Changeset 2608 for src/Clight/Csem.ma


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/Clight/Csem.ma

    r2588 r2608  
    512512  | alloc_variables_cons:
    513513      ∀e,m,id,ty,vars,m1,b1,m2,e2.
    514       alloc m 0 (sizeof ty) XData = 〈m1, b1〉 →
    515       alloc_variables (add … e id (pi1 … b1)) m1 vars e2 m2 →
     514      alloc m 0 (sizeof ty) (* XData *) = 〈m1, b1〉 →
     515      alloc_variables (add … e id b1) m1 vars e2 m2 →
    516516      alloc_variables e m (〈id, ty〉 :: vars) e2 m2.
    517517
Note: See TracChangeset for help on using the changeset viewer.