Library mcertikos.devdrivers.DLApicCSource

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_init_body :=
(Ssequence
  (Scall None (Evar cons_buf_init (Tfunction Tnil tvoid cc_default)) nil)
  (Scall None (Evar serial_init (Tfunction Tnil tvoid cc_default)) nil)).

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

Definition _hasMore := 1%positive.
Definition _t := 2%positive.

Definition cons_intr_loop_condition :=
  Ebinop Oand
  (Ebinop Oeq (Etempvar _hasMore tuint) (Econst_int (Int.repr 1) tuint) tint)
  (Ebinop Olt (Etempvar _t tint) (Econst_int (Int.repr 512) tint) tint)
  tint.

Definition cons_intr_loop_body :=
  (Ssequence
    (Scall (Some _hasMore) (Evar serial_getc (Tfunction Tnil tuint cc_default)) nil)
    (Sset _t (Ebinop Oadd (Etempvar _t tint) (Econst_int (Int.repr 1) tint) tint))).

Notation cons_intr_real_body :=
      (Ssequence
     (Scall (Some _hasMore)
      (Evar serial_getc (Tfunction Tnil tuint cc_default)) nil)
  (Sifthenelse (Ebinop Oeq (Etempvar _hasMore tuint)
                 (Econst_int (Int.repr 1) tuint) tint)
    (Ssequence
      (Sset _t (Econst_int (Int.repr 0) tint))
      (Swhile cons_intr_loop_condition cons_intr_loop_body))
    Sskip)).

Definition cons_intr_body :=
(Ssequence
   (Scall None (Evar lapic_eoi (Tfunction Tnil tvoid cc_default)) nil)
   cons_intr_real_body).

Definition f_cons_intr := {|
  fn_return := tvoid;
  fn_callconv := cc_default;
  fn_params := nil;
  fn_vars := nil;
  fn_temps := ((_hasMore, tuint) :: (_t, tint) :: nil);
  fn_body := cons_intr_body
|}.