Changeset 2763 for src


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
Files:
4 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
  • src/LIN/LINToASM.ma

    r2760 r2763  
    374374     (* atm no data identifier is used in the code, so preamble must be empty *)
    375375     return
    376       (mk_pseudo_assembly_program [ ] code symboltable exit_label ? ?)).
     376      (mk_pseudo_assembly_program [ ] code ? symboltable exit_label ? ?)).
    377377cases daemon
    378378qed.
  • src/compiler.ma

    r2762 r2763  
    5757  let pol ≝ λppc. \snd sigma_pol ppc in
    5858  OK ? (assembly p sigma pol).
    59   cases daemon
    60 qed.
    6159
    6260include "ASM/ASMCosts.ma".
Note: See TracChangeset for help on using the changeset viewer.