Library mcertikos.devdrivers.DHandlerIntroCSource

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_handler_sw_body :=
  (Ssequence
  (Scall None
    (Evar ioapic_mask (Tfunction (Tcons tuint Tnil) tvoid cc_default))
    ((Econst_int (Int.repr 4) tint) :: nil))
  (Ssequence
    (Scall None (Evar sti (Tfunction Tnil tvoid cc_default)) nil)
    (Ssequence
      (Scall None (Evar cons_intr (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_handler_sw := {|
  fn_return := tvoid;
  fn_callconv := cc_default;
  fn_params := nil;
  fn_vars := nil;
  fn_temps := nil;
  fn_body := serial_intr_handler_sw_body
|}.