Library mcertikos.trap.TTrapArgCSource2

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

void
sys_getc()
{
	int x;

	serial_intr_disable();
	x = cons_buf_read();
	serial_intr_enable();

	uctx_set_retval1(x);
	uctx_set_errno(E_SUCC);
}

Notation _x := 1 % positive.

Definition sys_getc_body :=
(Ssequence
  (Scall None (Evar serial_intr_disable (Tfunction Tnil tvoid cc_default))
    nil)
  (Ssequence
      (Scall (Some _x)
        (Evar cons_buf_read (Tfunction Tnil tuint cc_default)) nil)
    (Ssequence
      (Scall None
        (Evar serial_intr_enable (Tfunction Tnil tvoid cc_default)) nil)
      (Ssequence
        (Scall None
          (Evar uctx_set_retval1 (Tfunction (Tcons tuint Tnil) tvoid
                                    cc_default)) ((Etempvar _x tint) :: nil))
        (Scall None
          (Evar uctx_set_errno (Tfunction (Tcons tuint Tnil) tvoid
                                  cc_default))
          ((Econst_int (Int.repr 0) tint) :: nil)))))).

Definition f_sys_getc := {|
  fn_return := tvoid;
  fn_callconv := cc_default;
  fn_params := nil;
  fn_vars := nil;
  fn_temps := ((_x, tint) :: nil);
  fn_body := sys_getc_body
|}.

void
sys_putc (void)
{
	unsigned int c;

	c = uctx_arg2 ();

	serial_intr_disable();
	serial_putc(c);
	serial_intr_enable();

	uctx_set_errno (E_SUCC);
}

Notation _c := 2 % positive.

Definition sys_putc_body :=
(Ssequence
    (Scall (Some _c) (Evar uctx_arg2 (Tfunction Tnil tuint cc_default))
      nil)
  (Ssequence
    (Scall None (Evar serial_intr_disable (Tfunction Tnil tvoid cc_default))
      nil)
    (Ssequence
      (Scall None
        (Evar serial_putc (Tfunction (Tcons tuint Tnil) tvoid cc_default))
        ((Etempvar _c tuint) :: nil))
      (Ssequence
        (Scall None
          (Evar serial_intr_enable (Tfunction Tnil tvoid cc_default)) nil)
        (Scall None
          (Evar uctx_set_errno (Tfunction (Tcons tuint Tnil) tvoid
                                  cc_default))
          ((Econst_int (Int.repr 0) tint) :: nil)))))).

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