Library mcertikos.devdrivers.DConsoleCSource

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

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

Definition intr_default_handler_body :=
  (Scall None (Evar lapic_eoi (Tfunction Tnil tvoid cc_default)) nil).

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