Library mcertikos.devdrivers.DConsoleCSource

***********************************************************************
*                                                                     *
*            The CertiKOS Certified Kit Operating System              *
*                                                                     *
*                   The FLINT Group, Yale University                  *
*                                                                     *
*  Copyright The FLINT Group, Yale University.  All rights reserved.  *
*  This file is distributed under the terms of the Yale University    *
*  Non-Commercial License Agreement.                                  *
*                                                                     *
***********************************************************************

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
|}.