Library mcertikos.devdrivers.DHandlerOpCSource
*********************************************************************** * * * 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 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
|}.