Library mcertikos.mm.MPTInitCSource

***********************************************************************
*                                                                     *
*            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 unsigned int PTP_LOC[num_proc];
      
      void set_bit(unsigned int proc_index, unsigned int val)
      {
          PTP_LOC[proc_index] = val;
      }
Local temporaries used in the function
Local Open Scope positive.
Let tproc_index: ident := 1.
Let tval: ident:= 2.

Local Open Scope Z_scope.

Definition set_bit_body : statement :=
  (Sassign (Ederef
              (Ebinop Oadd (Evar PTP_LOC (tarray tint num_proc)) (Etempvar tproc_index tint)
                      (tptr tint)) tint) (Etempvar tval tint)).

Definition f_set_bit := {|
                         fn_return := tvoid;
                         fn_callconv := cc_default;
                         fn_vars := nil;
                         fn_params := ((tproc_index, tint) :: (tval, tint) :: nil);
                         fn_temps := nil;
                         fn_body := set_bit_body
                       |}.

      extern unsigned int PTP_LOC[num_proc];
      
      unsigned int is_used(unsigned int proc_index)
      {
          unsigned int val;
          val = PTP_LOC[proc_index];
          return val;
      }

Local Open Scope Z_scope.

Definition is_used_body : statement :=
  (Ssequence (Sset tval (Ederef
                           (Ebinop Oadd (Evar PTP_LOC (tarray tint 64))
                                   (Etempvar tproc_index tint) (tptr tint)) tint))
             (Sreturn (Some (Etempvar tval tint)))).

Definition f_is_used := {|
                         fn_return := tint;
                         fn_callconv := cc_default;
                         fn_vars := nil;
                         fn_params := ((tproc_index, tint) :: nil);
                         fn_temps := ((tval, tint) :: nil);
                         fn_body := is_used_body
                       |}.