Library mcertikos.devdrivers.DIoApicCSource

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 lapic_init_body :=
(Ssequence
  (Scall None
    (Evar lapic_write (Tfunction (Tcons tint (Tcons tint Tnil)) tvoid
                         cc_default))
    ((Ebinop Odiv (Econst_int (Int.repr 240) tint)
       (Econst_int (Int.repr 4) tint) tint) ::
     (Ebinop Oadd
       (Ebinop Oadd (Econst_int (Int.repr 256) tint)
         (Econst_int (Int.repr 32) tint) tint) (Econst_int (Int.repr 7) tint)
       tint) :: nil))
  (Ssequence
    (Scall None
      (Evar lapic_write (Tfunction (Tcons tint (Tcons tint Tnil)) tvoid
                           cc_default))
      ((Ebinop Odiv (Econst_int (Int.repr 848) tint)
         (Econst_int (Int.repr 4) tint) tint) ::
       (Econst_int (Int.repr 65536) tint) :: nil))
    (Ssequence
      (Scall None
        (Evar lapic_write (Tfunction (Tcons tint (Tcons tint Tnil)) tvoid
                             cc_default))
        ((Ebinop Odiv (Econst_int (Int.repr 864) tint)
           (Econst_int (Int.repr 4) tint) tint) ::
         (Econst_int (Int.repr 65536) tint) :: nil))
      (Ssequence
        (Scall None
          (Evar lapic_write (Tfunction (Tcons tint (Tcons tint Tnil)) tvoid
                               cc_default))
          ((Ebinop Odiv (Econst_int (Int.repr 832) tint)
             (Econst_int (Int.repr 4) tint) tint) ::
           (Econst_int (Int.repr 65536) tint) :: nil))
        (Ssequence
          (Scall None
            (Evar lapic_write (Tfunction (Tcons tint (Tcons tint Tnil))
                                 tvoid cc_default))
            ((Ebinop Odiv (Econst_int (Int.repr 208) tint)
               (Econst_int (Int.repr 4) tint) tint) ::
             (Econst_int (Int.repr 0) tint) :: nil))
          (Ssequence
            (Scall None
              (Evar lapic_write (Tfunction (Tcons tint (Tcons tint Tnil))
                                   tvoid cc_default))
              ((Ebinop Odiv (Econst_int (Int.repr 880) tint)
                 (Econst_int (Int.repr 4) tint) tint) ::
               (Econst_int (Int.repr 50) tint) :: nil))
            (Ssequence
              (Scall None
                (Evar lapic_write (Tfunction (Tcons tint (Tcons tint Tnil))
                                     tvoid cc_default))
                ((Ebinop Odiv (Econst_int (Int.repr 640) tint)
                   (Econst_int (Int.repr 4) tint) tint) ::
                 (Econst_int (Int.repr 0) tint) :: nil))
              (Ssequence
                (Scall None
                  (Evar lapic_write (Tfunction
                                       (Tcons tint (Tcons tint Tnil)) tvoid
                                       cc_default))
                  ((Ebinop Odiv (Econst_int (Int.repr 640) tint)
                     (Econst_int (Int.repr 4) tint) tint) ::
                   (Econst_int (Int.repr 0) tint) :: nil))
                (Ssequence
                  (Scall None
                    (Evar lapic_write (Tfunction
                                         (Tcons tint (Tcons tint Tnil)) tvoid
                                         cc_default))
                    ((Ebinop Odiv (Econst_int (Int.repr 176) tint)
                       (Econst_int (Int.repr 4) tint) tint) ::
                     (Econst_int (Int.repr 0) tint) :: nil))
                  (Scall None
                    (Evar lapic_write (Tfunction
                                         (Tcons tint (Tcons tint Tnil)) tvoid
                                         cc_default))
                    ((Ebinop Odiv (Econst_int (Int.repr 128) tint)
                       (Econst_int (Int.repr 4) tint) tint) ::
                     (Econst_int (Int.repr 0) tint) :: nil))))))))))).

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

Definition lapic_eoi_body :=
(Scall None
  (Evar lapic_write (Tfunction (Tcons tint (Tcons tint Tnil)) tvoid
                       cc_default))
  ((Ebinop Odiv (Econst_int (Int.repr 176) tint)
     (Econst_int (Int.repr 4) tint) tint) ::
   (Econst_int (Int.repr 0) tint) :: nil)).

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