Ignore:
Timestamp:
Apr 6, 2013, 7:35:25 PM (7 years ago)
Author:
sacerdot
Message:

New extraction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • driver/extracted/interpret2.ml

    r3080 r3106  
    468468        policy (Obj.magic st))) (Obj.magic (Status.initialise_status c))
    469469
     470(** val aSM_status :
     471    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
     472    (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status **)
     473let aSM_status c sigma policy =
     474  let label_map = (Fetch.create_label_cost_map c.ASM.code).Types.fst in
     475  let symbol_map = Status.construct_datalabels c.ASM.preamble in
     476  let addr_of_label = fun x ->
     477    Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     478      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     479      Nat.O))))))))))))))))
     480      (Identifiers.lookup_def PreIdentifiers.ASMTag label_map x Nat.O)
     481  in
     482  let addr_of_symbol = fun x ->
     483    Identifiers.lookup_def PreIdentifiers.ASMTag symbol_map x
     484      (addr_of_label x)
     485  in
     486  aSM_abstract_status c addr_of_label addr_of_symbol sigma policy
     487
Note: See TracChangeset for help on using the changeset viewer.