Changeset 2763 for src/ASM


Ignore:
Timestamp:
Mar 2, 2013, 11:42:16 AM (7 years ago)
Author:
sacerdot
Message:

All daemons in compiler.ma closed (i.e. proof obligations added
to the sigma type of compiled programs).

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2760 r2763  
    11011101{ preamble : list (Identifier × Word)
    11021102; code : list labelled_instruction
     1103; code_size_ok: S (|code|) < 2^16
    11031104; renamed_symbols : list (Identifier × ident)
    11041105; final_label : Identifier
  • src/ASM/Policy.ma

    r2762 r2763  
    658658(* The glue between Policy and Assembly. *)
    659659definition jump_expansion':
    660 ∀program:(Σp:pseudo_assembly_program.S (|code p|) < 2^16).
     660∀program:pseudo_assembly_program.
    661661 option (Σsigma_policy:(Word → Word) × (Word → bool).
    662662   let 〈sigma,policy〉≝ sigma_policy in
     
    674674          jmpeqb jl long_jump)〉,?»
    675675  ] (refl ? f).
    676 [2: % [@(pi2 … program) | @well_labelled_p ]]
     676[2: % [@code_size_ok | @well_labelled_p ]]
    677677normalize nodelta in p; whd in match sigma_policy_specification; normalize nodelta
    678678lapply (pi2 ?? (je_fixpoint «code program,?»)) [2: >p | skip] normalize nodelta cases x
Note: See TracChangeset for help on using the changeset viewer.