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/RTLabs/RTLabs_traces.ma

    r2601 r2608  
    540540cases fd
    541541[ #fn whd in ⊢ (??%? → % → ?);
    542   @bind_res_value #lcl #Elcl cases (alloc m O (f_stacksize fn) XData)
     542  @bind_res_value #lcl #Elcl cases (alloc m O (f_stacksize fn) (*XData*))
    543543  #m' #b whd in ⊢ (??%? → ?); #E' destruct
    544544  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
Note: See TracChangeset for help on using the changeset viewer.