Library mcertikos.mm.MPTKernCSource

***********************************************************************
*                                                                     *
*            The CertiKOS Certified Kit Operating System              *
*                                                                     *
*                   The FLINT Group, Yale University                  *
*                                                                     *
*  Copyright The FLINT Group, Yale University.  All rights reserved.  *
*  This file is distributed under the terms of the Yale University    *
*  Non-Commercial License Agreement.                                  *
*                                                                     *
***********************************************************************

Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Cop.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.

      extern void pt_init_kern(unsigned int);
      extern void set_pg(void);
      extern void set_pt(unsigned int);

      void pt_init(unsigned int mbi_adr)
      {
          pt_init_kern(mbi_adr);
          set_pt(0);
          set_pg();
      }

Let tmbi_adr: ident := 1 % positive.

Definition pt_init_body : statement :=
  (Ssequence
     (Scall None (Evar pt_init_kern (Tfunction (Tcons tint Tnil) Tvoid cc_default)) ((Etempvar tmbi_adr tint)::nil))
     (Ssequence
        (Scall None (Evar set_pt (Tfunction (Tcons tint Tnil) Tvoid cc_default))
               ((Econst_int (Int.repr 0) tint) :: nil))
        (Scall None (Evar set_pg (Tfunction Tnil Tvoid cc_default)) nil)))
.

Definition f_pt_init := {|
                         fn_return := tvoid;
                         fn_callconv := cc_default;
                         fn_vars := nil;
                         fn_params := ((tmbi_adr, tint)::nil);
                         fn_temps := nil;
                         fn_body := pt_init_body
                       |}.