Ignore:
Timestamp:
Mar 19, 2013, 8:42:43 AM (7 years ago)
Author:
sacerdot
Message:

Semantics of ASM in place (up to return values and function call names).
The test example badly diverges in ASM after being ok in LIN.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/abstractStatus.ml

    r2773 r2905  
    190190      Nat.O)))))))))))))))))
    191191
    192 (** val aSM_classify :
     192(** val oC_classify :
    193193    BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
    194194    StructuredTraces.status_class **)
    195 let aSM_classify code_memory s =
     195let oC_classify code_memory s =
    196196  aSM_classify0 (current_instruction code_memory s)
    197197
Note: See TracChangeset for help on using the changeset viewer.