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/frontend_misc.ma

    r2588 r2608  
    345345
    346346definition block_DeqSet : DeqSet ≝ mk_DeqSet block eq_block ?.
    347 * #r1 #id1 * #r2 #id2 @(eqZb_elim … id1 id2)
    348 [ 1: #Heq >Heq cases r1 cases r2 normalize
     347* (*#r1*) #id1 * (*#r2*) #id2 @(eqZb_elim … id1 id2)
     348[ 1: #Heq >Heq (* cases r1 cases r2 * normalize *)
    349349     >eqZb_z_z normalize try // @conj #H destruct (H)
    350      try @refl
    351 | 2: #Hneq cases r1 cases r2 normalize
     350     try @refl @eqZb_z_z
     351| 2: #Hneq (* cases r1 cases r2 *) normalize
    352352     >(eqZb_false … Hneq) normalize @conj
    353353     #H destruct (H) elim Hneq #H @(False_ind … (H (refl ??)))
Note: See TracChangeset for help on using the changeset viewer.