Library mcertikos.proc.PAbQueueCSource
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.
extern unsigned int CURID_LOC; unsigned int get_curid() { return CURID_LOC; }
Definition get_curid_body : statement :=
Sreturn (Some (Evar CURID_LOC tint)).
Definition f_get_curid := {|
fn_return := tint;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := nil;
fn_temps := nil;
fn_body := get_curid_body
|}.
extern unsigned int CURID_LOC; void set_curid(unsigned int curid) { CURID_LOC = curid; }
Let tcurid: ident := 1 % positive.
Definition set_curid_body : statement :=
Sassign (Evar CURID_LOC tint) (Etempvar tcurid tint).
Definition f_set_curid := {|
fn_return := Tvoid;
fn_callconv := cc_default;
fn_vars := nil;
fn_params := ((tcurid, tint) :: nil);
fn_temps := nil;
fn_body := set_curid_body
|}.