Changeset 2608 for src/Cminor


Ignore:
Timestamp:
Feb 6, 2013, 1:01:34 PM (7 years ago)
Author:
garnier
Message:

Regions are no more stored in blocks. block_region now tests the id, it being below 0 implying Code region, XData otherwise.
Changes propagated through the front-end and common. Some more work might be required in the back-end, but it should be
trivial to fix related problems.

Motivation: no way to /elegantly/ prove that two blocks with the same id but different regions are non-sensical.
Prevented some proofs to go through in memory injections.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/Cminor_semantics.ma

    r2601 r2608  
    343343    match fd with
    344344    [ Internal f ⇒ err_to_io ?? (trace × state) (
    345         let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) XData in
     345        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) (* XData *) in
    346346        ! en ← bind_params args (f_params f);
    347347        return 〈E0, State f (f_body f) (init_locals en (f_vars f)) ? ? m' sp Kend ? st〉)
Note: See TracChangeset for help on using the changeset viewer.