Changeset 2055 for src/ASM/Policy.ma


Ignore:
Timestamp:
Jun 13, 2012, 12:11:21 PM (8 years ago)
Author:
sacerdot
Message:

Warning: this commit adds an hypothesis that breaks all of assembly stuff.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2034 r2055  
    625625∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16).
    626626 option (Σsigma:Word → Word × bool.
    627    ∀ppc: Word.
     627   ∀ppc: Word. ∀ppc_ok.
    628628   let pc ≝ \fst (sigma ppc) in
    629629   let labels ≝ \fst (create_label_cost_map (\snd program)) in
    630630   let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def ?? labels x 0) in
    631    let instruction ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in
     631   let instruction ≝ \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
    632632   let next_pc ≝ \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in
    633633     And (nat_of_bitvector … ppc ≤ |\snd program| →
Note: See TracChangeset for help on using the changeset viewer.