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/interpret2.mli

    r2880 r2905  
    138138  ASM.labelled_object_code -> Measurable.preclassified_system
    139139
     140open Assembly
     141
     142val execute_1_pseudo_instruction' :
     143  ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
     144  (BitVector.word -> Bool.bool) -> Status.pseudoStatus -> Status.pseudoStatus
     145
     146val classify_pseudo_instruction :
     147  ASM.pseudo_instruction -> StructuredTraces.status_class
     148
     149val aSM_classify :
     150  ASM.pseudo_assembly_program -> Status.pseudoStatus ->
     151  StructuredTraces.status_class
     152
     153val aSM_as_label_of_pc :
     154  ASM.pseudo_assembly_program -> BitVector.word -> CostLabel.costlabel
     155  Types.option
     156
     157val aSM_abstract_status :
     158  ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
     159  (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status
     160
     161val aSM_preclassified_system :
     162  ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
     163  (BitVector.word -> Bool.bool) -> Measurable.preclassified_system
     164
Note: See TracChangeset for help on using the changeset viewer.