Library mcertikos.devdrivers.MQTicketLockCSource

Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Cop.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.

Definition cons_buf_init_body :=
  (Ssequence
  (Sassign (Efield (Evar cons_buf_LOC t_struct_cons_buf) rpos tuint)
    (Econst_int (Int.repr 0) tint))
  (Sassign (Efield (Evar cons_buf_LOC t_struct_cons_buf) wpos tuint)
    (Econst_int (Int.repr 0) tint))).

Definition f_cons_buf_init := {|
  fn_return := tvoid;
  fn_callconv := cc_default;
  fn_params := nil;
  fn_vars := nil;
  fn_temps := nil;
  fn_body := cons_buf_init_body
|}.

Definition cons_buf_wpos_body :=
  (Sreturn (Some (Efield (Evar cons_buf_LOC t_struct_cons_buf) wpos tuint))).

Definition f_cons_buf_wpos := {|
  fn_return := tuint;
  fn_callconv := cc_default;
  fn_params := nil;
  fn_vars := nil;
  fn_temps := nil;
  fn_body := cons_buf_wpos_body
|}.

Notation _rv := 1%positive.

Definition cons_buf_read_body :=
(Ssequence
  (Sset _rv (Econst_int (Int.repr 0) tint))
  (Ssequence
    (Sifthenelse (Ebinop One
                   (Efield (Evar cons_buf_LOC t_struct_cons_buf) rpos tuint)
                   (Efield (Evar cons_buf_LOC t_struct_cons_buf) wpos tuint) tint)
      (Ssequence
        (Sset _rv
          (Ederef
            (Ebinop Oadd
              (Efield (Evar cons_buf_LOC t_struct_cons_buf) buffer
                (tarray tuint 512))
              (Efield (Evar cons_buf_LOC t_struct_cons_buf) rpos tuint)
              (tptr tuint)) tuint))
        (Sassign (Efield (Evar cons_buf_LOC t_struct_cons_buf) rpos tuint)
          (Ebinop Omod
            (Ebinop Oadd (Efield (Evar cons_buf_LOC t_struct_cons_buf) rpos tuint)
              (Econst_int (Int.repr 1) tint) tuint)
            (Econst_int (Int.repr 512) tint) tuint)))
      Sskip)
    (Sreturn (Some (Etempvar _rv tuint))))).

Definition f_cons_buf_read := {|
  fn_return := tuint;
  fn_callconv := cc_default;
  fn_params := nil;
  fn_vars := nil;
  fn_temps := ((_rv, tuint) :: nil);
  fn_body := cons_buf_read_body
|}.

Notation _c := 2%positive.

Definition cons_buf_write_body :=
  (Ssequence
  (Sassign
    (Ederef
      (Ebinop Oadd
        (Efield (Evar cons_buf_LOC t_struct_cons_buf) buffer (tarray tuint 512))
        (Efield (Evar cons_buf_LOC t_struct_cons_buf) wpos tuint) (tptr tuint))
      tuint) (Etempvar _c tuint))
  (Ssequence
    (Sassign (Efield (Evar cons_buf_LOC t_struct_cons_buf) wpos tuint)
      (Ebinop Omod
        (Ebinop Oadd (Efield (Evar cons_buf_LOC t_struct_cons_buf) wpos tuint)
          (Econst_int (Int.repr 1) tint) tuint)
        (Econst_int (Int.repr 512) tint) tuint))
    (Sifthenelse (Ebinop Oeq
                   (Efield (Evar cons_buf_LOC t_struct_cons_buf) rpos tuint)
                   (Efield (Evar cons_buf_LOC t_struct_cons_buf) wpos tuint) tint)
      (Sassign (Efield (Evar cons_buf_LOC t_struct_cons_buf) rpos tuint)
        (Ebinop Omod
          (Ebinop Oadd (Efield (Evar cons_buf_LOC t_struct_cons_buf) rpos tuint)
            (Econst_int (Int.repr 1) tint) tuint)
          (Econst_int (Int.repr 512) tint) tuint))
      Sskip))).

Definition f_cons_buf_write := {|
  fn_return := tvoid;
  fn_callconv := cc_default;
  fn_params := ((_c, tuint) :: nil);
  fn_vars := nil;
  fn_temps := nil;
  fn_body := cons_buf_write_body
|}.