Library mcertikos.devdrivers.DAbsConsoleBuffIntroCSource

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 get_serial_exists_body :=
  (Sreturn (Some (Evar serial_exists_LOC tuint))).

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

Notation _ex := 1 % positive.

Definition set_serial_exists_body :=
  (Sifthenelse (Ebinop Ogt (Etempvar _ex tuint) (Econst_int (Int.repr 0) tint)
               tint)
  (Sassign (Evar serial_exists_LOC tuint) (Econst_int (Int.repr 1) tint))
  (Sassign (Evar serial_exists_LOC tuint) (Econst_int (Int.repr 0) tint))).

Definition f_set_serial_exists := {|
  fn_return := tvoid;
  fn_callconv := cc_default;
  fn_params := ((_ex, tuint) :: nil);
  fn_vars := nil;
  fn_temps := nil;
  fn_body := set_serial_exists_body
|}.