Library mcertikos.devdrivers.HandlerAsmGenLinkSource

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} `{MultiOracleProp} `{WaitTime} :=
  link_impl DHandlerAsm_module dhandlersw.