Changeset 2620


Ignore:
Timestamp:
Feb 6, 2013, 5:03:20 PM (6 years ago)
Author:
campbell
Message:

Sufficient hacking to run the extracted Clight semantics.

Files:
7 added
4 edited

Legend:

Unmodified
Added
Removed
  • extracted/aSM.ml

    r2601 r2620  
    53795379| Mov (x, x0) -> Bool.False
    53805380
    5381 let subaddressing_modeel__o__mk_subaddressing_mode = assert false
     5381let subaddressing_modeel__o__mk_subaddressing_mode x = assert false
  • extracted/compiler.ml

    r2601 r2620  
    185185(** val back_end :
    186186    RTLabs_syntax.rTLabs_program -> ASM.pseudo_assembly_program **)
    187 let back_end =
     187let back_end x =
    188188  failwith "AXIOM TO BE REALIZED"
    189189
     
    195195    ASM.pseudo_assembly_program -> (object_code, costlabel_map) Types.prod
    196196    Errors.res **)
    197 let assembler =
     197let assembler x =
    198198  failwith "AXIOM TO BE REALIZED"
    199199
  • extracted/floats.ml

    r2601 r2620  
    4646
    4747type float (* AXIOM TO BE REALIZED *)
    48 
     48(*
    4949(** val fzero : float **)
    5050let fzero =
     
    106106let eq_dec0 =
    107107  failwith "AXIOM TO BE REALIZED"
    108 
     108*)
  • extracted/floats.mli

    r2601 r2620  
    4646
    4747type float
    48 
     48(*
    4949val fzero : float
    5050
     
    7676
    7777val eq_dec0 : float -> float -> (__, __) Types.sum
    78 
     78*)
Note: See TracChangeset for help on using the changeset viewer.