Library mcertikos.proc.PKContextNewCSource
Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Cop.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Cop.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
#define num_proc 64 struct TCB { unsigned int state; unsigned int prev; unsigned int next; }; extern struct TCB TCBPool_LOC[num_proc]; unsigned int get_state(unsigned int proc_index) { return TCBPool_LOC[proc_index].state; }
Local Open Scope positive_scope.
Let tproc_index: ident := 1.
Local Open Scope Z_scope.
Definition get_state_body : statement :=
(Sreturn (Some (Efield
(Ederef
(Ebinop Oadd (Evar TCBPool_LOC (tarray t_struct_TCB num_proc))
(Etempvar tproc_index tint) (tptr t_struct_TCB))
t_struct_TCB) state tint))).
Definition f_get_state := {|
fn_return := tint;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tproc_index, tint) :: nil);
fn_temps := nil;
fn_body := get_state_body
|}.
Let tproc_index: ident := 1.
Local Open Scope Z_scope.
Definition get_state_body : statement :=
(Sreturn (Some (Efield
(Ederef
(Ebinop Oadd (Evar TCBPool_LOC (tarray t_struct_TCB num_proc))
(Etempvar tproc_index tint) (tptr t_struct_TCB))
t_struct_TCB) state tint))).
Definition f_get_state := {|
fn_return := tint;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tproc_index, tint) :: nil);
fn_temps := nil;
fn_body := get_state_body
|}.
#define num_proc 64 struct TCB { unsigned int state; unsigned int prev; unsigned int next; }; extern struct TCB TCBPool_LOC[num_proc]; unsigned int get_prev(unsigned int proc_index) { return TCBPool_LOC[proc_index].prev; }
Definition get_prev_body : statement :=
(Sreturn (Some (Efield
(Ederef
(Ebinop Oadd (Evar TCBPool_LOC (tarray t_struct_TCB num_proc))
(Etempvar tproc_index tint) (tptr t_struct_TCB))
t_struct_TCB) prev tint))).
Definition f_get_prev := {|
fn_return := tint;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tproc_index, tint) :: nil);
fn_temps := nil;
fn_body := get_prev_body
|}.
#define num_proc 64 struct TCB { unsigned int next; unsigned int prev; unsigned int next; }; extern struct TCB TCBPool_LOC[num_proc]; unsigned int get_next(unsigned int proc_index) { return TCBPool_LOC[proc_index].next; }
Definition get_next_body : statement :=
(Sreturn (Some (Efield
(Ederef
(Ebinop Oadd (Evar TCBPool_LOC (tarray t_struct_TCB num_proc))
(Etempvar tproc_index tint) (tptr t_struct_TCB))
t_struct_TCB) next tint))).
Definition f_get_next := {|
fn_return := tint;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tproc_index, tint) :: nil);
fn_temps := nil;
fn_body := get_next_body
|}.
#define num_proc 64 struct TCB { unsigned int state; unsigned int prev; unsigned int next; }; extern struct TCB TCBPool_LOC[num_proc]; void set_state(unsigned int proc_index, unsigned int state) { TCBPool_LOC[proc_index].state = state; }
Local Open Scope positive_scope.
Let tstate: ident := 2.
Local Open Scope Z_scope.
Definition set_state_body : statement :=
(Sassign (Efield(Ederef
(Ebinop Oadd (Evar TCBPool_LOC (tarray t_struct_TCB num_proc))
(Etempvar tproc_index tint) (tptr t_struct_TCB)) t_struct_TCB) state
tint) (Etempvar tstate tint)).
Definition f_set_state := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tproc_index, tint) :: (tstate, tint) :: nil);
fn_temps := nil;
fn_body := set_state_body
|}.
Let tstate: ident := 2.
Local Open Scope Z_scope.
Definition set_state_body : statement :=
(Sassign (Efield(Ederef
(Ebinop Oadd (Evar TCBPool_LOC (tarray t_struct_TCB num_proc))
(Etempvar tproc_index tint) (tptr t_struct_TCB)) t_struct_TCB) state
tint) (Etempvar tstate tint)).
Definition f_set_state := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tproc_index, tint) :: (tstate, tint) :: nil);
fn_temps := nil;
fn_body := set_state_body
|}.
#define num_proc 64 struct TCB { unsigned int prev; unsigned int prev; unsigned int next; }; extern struct TCB TCBPool_LOC[num_proc]; void set_prev(unsigned int proc_index, unsigned int prev) { TCBPool_LOC[proc_index].prev = prev; }
Local Open Scope positive_scope.
Let tprev: ident := 3.
Local Open Scope Z_scope.
Definition set_prev_body : statement :=
(Sassign (Efield(Ederef
(Ebinop Oadd (Evar TCBPool_LOC (tarray t_struct_TCB num_proc))
(Etempvar tproc_index tint) (tptr t_struct_TCB)) t_struct_TCB) prev
tint) (Etempvar tprev tint)).
Definition f_set_prev := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tproc_index, tint) :: (tprev, tint) :: nil);
fn_temps := nil;
fn_body := set_prev_body
|}.
Let tprev: ident := 3.
Local Open Scope Z_scope.
Definition set_prev_body : statement :=
(Sassign (Efield(Ederef
(Ebinop Oadd (Evar TCBPool_LOC (tarray t_struct_TCB num_proc))
(Etempvar tproc_index tint) (tptr t_struct_TCB)) t_struct_TCB) prev
tint) (Etempvar tprev tint)).
Definition f_set_prev := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tproc_index, tint) :: (tprev, tint) :: nil);
fn_temps := nil;
fn_body := set_prev_body
|}.
#define num_proc 64 struct TCB { unsigned int next; unsigned int next; unsigned int next; }; extern struct TCB TCBPool_LOC[num_proc]; void set_next(unsigned int proc_index, unsigned int next) { TCBPool_LOC[proc_index].next = next; }
Local Open Scope positive_scope.
Let tnext: ident := 4.
Local Open Scope Z_scope.
Definition set_next_body : statement :=
(Sassign (Efield(Ederef
(Ebinop Oadd (Evar TCBPool_LOC (tarray t_struct_TCB num_proc))
(Etempvar tproc_index tint) (tptr t_struct_TCB)) t_struct_TCB) next
tint) (Etempvar tnext tint)).
Definition f_set_next := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tproc_index, tint) :: (tnext, tint) :: nil);
fn_temps := nil;
fn_body := set_next_body
|}.
Let tnext: ident := 4.
Local Open Scope Z_scope.
Definition set_next_body : statement :=
(Sassign (Efield(Ederef
(Ebinop Oadd (Evar TCBPool_LOC (tarray t_struct_TCB num_proc))
(Etempvar tproc_index tint) (tptr t_struct_TCB)) t_struct_TCB) next
tint) (Etempvar tnext tint)).
Definition f_set_next := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tproc_index, tint) :: (tnext, tint) :: nil);
fn_temps := nil;
fn_body := set_next_body
|}.
#define num_proc 64 struct TCB { unsigned int prev; unsigned int prev; unsigned int next; }; extern struct TCB TCBPool_LOC[num_proc]; void tcb_init(unsigned int proc_index) { TCBPool_LOC[proc_index].state = 3; TCBPool_LOC[proc_index].prev = num_proc; TCBPool_LOC[proc_index].next = num_proc; }
Definition tcb_init_body : statement :=
(Ssequence
(Sassign (Efield (Ederef
(Ebinop Oadd (Evar TCBPool_LOC (tarray t_struct_TCB num_proc))
(Etempvar tproc_index tint) (tptr t_struct_TCB)) t_struct_TCB)
state tint) (Econst_int (Int.repr 3) tint))
(Ssequence
(Sassign (Efield (Ederef
(Ebinop Oadd (Evar TCBPool_LOC (tarray t_struct_TCB num_proc))
(Etempvar tproc_index tint) (tptr t_struct_TCB)) t_struct_TCB)
prev tint)
(Econst_int (Int.repr num_proc) tint))
(Sassign (Efield (Ederef
(Ebinop Oadd (Evar TCBPool_LOC (tarray t_struct_TCB num_proc))
(Etempvar tproc_index tint) (tptr t_struct_TCB)) t_struct_TCB)
next tint)
(Econst_int (Int.repr num_proc) tint)))).
Definition f_tcb_init := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tproc_index, tint) :: nil);
fn_temps := nil;
fn_body := tcb_init_body
|}.