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.

extern void acquire_lock_TCB (int n);
extern void enqueue(unsigned int chan_index, unsigned int proc_index);
extern void release_lock_TCB (int n);

void enqueue_atomic (int n, int i)
{
	acquire_lock_TCB (n);
	enqueue (n, i);
	release_lock_TCB (n);
}

Function parameters and local temporaries used in the function

Local Open Scope positive_scope.

Definition _n := 1.
Definition _i := 2.

Definition enqueue_atomic_body :=
  (Ssequence
  (Scall None
    (Evar acquire_lock_TCB (Tfunction (Tcons tint Tnil) tvoid cc_default))
    ((Etempvar _n tint ) :: nil))
  (Ssequence
    (Scall None
      (Evar enqueue (Tfunction (Tcons tuint (Tcons tuint Tnil)) tvoid
                       cc_default))
      ((Etempvar _n tint ) :: (Etempvar _i tint ) :: nil))
    (Scall None
      (Evar release_lock_TCB (Tfunction (Tcons tint Tnil) tvoid cc_default))
      ((Etempvar _n tint ) :: nil)))).

Definition f_enqueue_atomic :=
  {|
    fn_return := tvoid;
    fn_callconv := cc_default;
    fn_params := ((_n, tint) :: (_i, tint) :: nil);
    fn_vars := nil;
    fn_temps := nil;
    fn_body := enqueue_atomic_body
  |}.

extern void acquire_lock_TCB (int n);
extern unsigned int dequeue(unsigned int chan_index);
extern void release_lock_TCB (int n);

unsigned int dequeue_atomic (int n)
{
	unsigned int i;
	acquire_lock_TCB (n);
	i = dequeue (n);
	release_lock_TCB (n);
	return i;
}

Definition dequeue_atomic_body :=
  (Ssequence
  (Scall None
    (Evar acquire_lock_TCB (Tfunction (Tcons tint Tnil) tvoid cc_default))
    ((Etempvar _n tint ) :: nil))
  (Ssequence
      (Scall (Some _i)
        (Evar dequeue (Tfunction (Tcons tuint Tnil) tuint cc_default))
        ((Etempvar _n tint ) :: nil))
    (Ssequence
      (Scall None
        (Evar release_lock_TCB (Tfunction (Tcons tint Tnil) tvoid
                                  cc_default)) ((Etempvar _n tint ) :: nil))
      (Sreturn (Some (Etempvar _i tuint)))))).

Definition f_dequeue_atomic := {|
  fn_return := tuint;
  fn_callconv := cc_default;
  fn_params := ((_n, tint) :: nil);
  fn_vars := nil;
  fn_temps := ((_i, tuint) :: nil);
  fn_body := dequeue_atomic_body
|}.