Library mcertikos.mm.MContainerCSource
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.
unsigned int get_nps()
{
return NPS_LOC;
}
Definition get_nps_body : statement :=
Sreturn (Some (Evar NPS_LOC tint)).
Definition f_get_nps := {|
fn_return := tint;
fn_callconv := cc_default;
fn_params := nil;
fn_vars := nil;
fn_temps := nil;
fn_body := get_nps_body
|}.
void set_nps(unsigned int newnps)
{
NPS_LOC = newnps;
}
Let tnewnps: ident := 1 % positive.
Definition set_nps_body : statement :=
Sassign (Evar NPS_LOC tint) (Etempvar tnewnps tint).
Definition f_set_nps := {|
fn_return := Tvoid;
fn_callconv := cc_default;
fn_params := ((tnewnps, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := set_nps_body
|}.
struct A {
unsigned int isnorm;
unsigned int allocated;
unsigned int c;
};
extern struct A AT_LOC[maxpage];
unsigned int is_norm (unsigned int is_norm_index)
{
unsigned int tisnorm;
tisnorm = AT_LOC[is_norm_index].isnorm;
if (tisnorm != 0)
{
if (tisnorm == 1)
tisnorm = 0;
else
tisnorm = 1;
}
return tisnorm;
}
Let tisnorm: ident := 2 % positive.
Let tis_norm_index: ident := 3 % positive.
Definition is_norm_body : statement :=
(Ssequence
(Sset tisnorm (Efield (Ederef
(Ebinop Oadd (Evar AT_LOC (tarray t_struct_A maxpage))
(Etempvar tis_norm_index tint) (tptr t_struct_A)) t_struct_A)
A_isnorm_ident tint)
)
(Ssequence
(Sifthenelse
(Ebinop One (Etempvar tisnorm tint) (Econst_int (Int.repr 0) tint) tint)
(Sifthenelse
(Ebinop Oeq (Etempvar tisnorm tint) (Econst_int (Int.repr 1) tint) tint)
(Sset tisnorm (Econst_int (Int.repr 0) tint))
(Sset tisnorm (Econst_int (Int.repr 1) tint))
)
Sskip
)
(Sreturn (Some (Etempvar tisnorm tint)))))
.
Definition f_is_norm := {|
fn_return := tint;
fn_callconv := cc_default;
fn_params := ((tis_norm_index, tint) :: nil);
fn_vars := nil;
fn_temps := ((tisnorm, tint) :: nil);
fn_body := is_norm_body
|}.
struct A {
unsigned int isnorm;
unsigned int allocated;
};
extern struct A AT_LOC[maxpage];
extern unsigned int ATC_LOC[maxpage];
void set_norm (unsigned int set_norm_index, unsigned int norm_val)
{
AT_LOC[set_norm_index].isnorm = norm_val;
AT_LOC[set_norm_index].allocated = 0;
ATC_LOC[set_norm_index] = 0;
}
Let tset_norm_index: ident := 4 % positive.
Let tnorm_val: ident := 5 % positive.
Definition set_norm_body: statement :=
(Ssequence
(Sassign (Efield (Ederef (Ebinop Oadd (Evar AT_LOC (tarray t_struct_A maxpage))
(Etempvar tset_norm_index tint) (tptr t_struct_A)) t_struct_A) A_isnorm_ident tint) (Etempvar tnorm_val tint))
(Ssequence
(Sassign (Efield (Ederef (Ebinop Oadd (Evar AT_LOC (tarray t_struct_A maxpage))
(Etempvar tset_norm_index tint) (tptr t_struct_A)) t_struct_A) A_allocated_ident tint) (Econst_int (Int.repr 0) tint))
(Sassign (Ederef (Ebinop Oadd (Evar ATC_LOC (tarray tuint maxpage))
(Etempvar tset_norm_index tint) (tptr tuint)) tuint) (Econst_int (Int.repr 0) tint))
)).
Definition f_set_norm := {|
fn_return := Tvoid;
fn_callconv := cc_default;
fn_params := ((tset_norm_index, tint) :: (tnorm_val, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := set_norm_body
|}.
struct A {
unsigned int isnorm;
unsigned int allocated;
};
extern struct A AT_LOC[maxpage];
unsigned int at_get (unsigned int at_get_index)
{
unsigned int allocated;
allocated = AT_LOC[at_get_index].allocated;
if (allocated != 0)
allocated = 1;
return allocated;
}
Let tallocated: ident := 6 % positive.
Let tat_get_index: ident := 7 % positive.
Definition at_get_body : statement :=
(Ssequence
(Sset tallocated (Efield (Ederef (Ebinop Oadd (Evar AT_LOC (tarray t_struct_A maxpage))
(Etempvar tat_get_index tint) (tptr t_struct_A)) t_struct_A) A_allocated_ident tint))
(Ssequence
(Sifthenelse
(Ebinop One (Etempvar tallocated tint) (Econst_int (Int.repr 0) tint) tint)
(Sset tallocated (Econst_int (Int.repr 1) tint))
Sskip)
(Sreturn (Some (Etempvar tallocated tint)))))
.
Definition f_at_get := {|
fn_return := tint;
fn_callconv := cc_default;
fn_params := ((tat_get_index, tint) :: nil);
fn_vars := nil;
fn_temps := ((tallocated, tint) :: nil);
fn_body := at_get_body
|}.
struct A {
int isnorm;
int allocated;
};
extern struct A AT_LOC[1048576];
void at_set (unsigned int at_set_index, unsigned int allocated_val)
{
AT_LOC[at_set_index].allocated = allocated_val;
}
Let tat_set_index: ident := 8 % positive.
Let tallocated_val: ident := 9 % positive.
Definition at_set_body: statement :=
(Sassign (Efield (Ederef (Ebinop Oadd (Evar AT_LOC (tarray t_struct_A maxpage))
(Etempvar tat_set_index tint) (tptr t_struct_A)) t_struct_A) A_allocated_ident tint) (Etempvar tallocated_val tint))
.
Definition f_at_set := {|
fn_return := Tvoid;
fn_callconv := cc_default;
fn_params := ((tat_set_index, tint) :: (tallocated_val, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := at_set_body
|}.
extern unsigned int ATC_LOC[maxpage];
unsigned int at_get_c (unsigned int at_get_c_index)
{
unsigned int c;
c = ATC_LOC[at_get_c_index];
return c;
}
Let tc: ident := 10 % positive.
Let tat_get_c_index: ident := 11 % positive.
Definition at_get_c_body : statement :=
(Ssequence
(Sset tc (Ederef (Ebinop Oadd (Evar ATC_LOC (tarray tuint maxpage))
(Etempvar tat_get_c_index tuint) (tptr tuint)) tuint))
(Sreturn (Some (Etempvar tc tint))))
.
Definition f_at_get_c := {|
fn_return := tint;
fn_callconv := cc_default;
fn_params := ((tat_get_c_index, tint) :: nil);
fn_vars := nil;
fn_temps := ((tc, tint) :: nil);
fn_body := at_get_c_body
|}.
extern unsigned int ATC_LOC[maxpage];
void at_set_c (unsigned int at_set_c_index, unsigned int c_val)
{
ATC_LOC[at_set_c_index] = c_val;
}
Let tat_set_c_index: ident := 12 % positive.
Let tc_val: ident := 13 % positive.
Definition at_set_c_body: statement :=
(Sassign (Ederef (Ebinop Oadd (Evar ATC_LOC (tarray tuint maxpage))
(Etempvar tat_set_c_index tint) (tptr tuint)) tuint) (Etempvar tc_val tint))
.
Definition f_at_set_c := {|
fn_return := Tvoid;
fn_callconv := cc_default;
fn_params := ((tat_set_c_index, tint) :: (tc_val, tint) :: nil);
fn_vars := nil;
fn_temps := nil;
fn_body := at_set_c_body
|}.