Library mcertikos.devdrivers.HandlerAsmGenLinkSource
*********************************************************************** * * * 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 LinkSourceTemplate.
Require Import DHandlerSw.
Require Import DHandlerSwAsmSource.
Require Import CDataTypes.
Require Import AST.
Require Import Integers.
Definition v_set_tf := {|
gvar_info := tuint;
gvar_init := (Init_int32 (Int.repr 0) :: nil);
gvar_readonly := false;
gvar_volatile := false
|}.
Definition DHandlerAsm_module: link_module :=
{|
lm_cfun :=
nil;
lm_asmfun :=
laf serial_intr_handler_asm serial_intr_handler_asm_function ::
nil;
lm_gvar :=
lgv set_tf v_set_tf ::
nil
|}.
Definition DHandlerAsm_impl `{CompCertiKOS} `{RealParams} :=
link_impl DHandlerAsm_module dhandlersw.