Library mcertikos.devdrivers.DHandlerOpCSource

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 serial_intr_enable_concrete_body :=
  (Ssequence
     (Scall None (Evar serial_intr_enable_handler (Tfunction Tnil tvoid cc_default)) nil)
     (Scall None (Evar ioapic_unmask (Tfunction (Tcons tuint Tnil) tvoid cc_default))
         ((Econst_int (Int.repr 4) tint) :: nil))).

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

Definition serial_intr_disable_concrete_body :=
  (Ssequence
     (Scall None (Evar serial_intr_disable_handler (Tfunction Tnil tvoid cc_default)) nil)
     (Scall None (Evar ioapic_mask (Tfunction (Tcons tuint Tnil) tvoid cc_default))
         ((Econst_int (Int.repr 4) tint) :: nil))).

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