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/common/extraGlobalenvs.ma

    r2590 r2608  
    219219** #x1 #x2 #x3 #tl whd in match add_globals;
    220220normalize nodelta #IND #m #ge #H whd in match (foldl ?????); normalize nodelta
    221 cases(alloc m ? ? x2) #m1 #bl1 normalize nodelta @IND whd in match add_symbol;
     221cases(alloc m ? ? (*x2*)) #m1 #bl1 normalize nodelta @IND whd in match add_symbol;
    222222normalize nodelta inversion(lookup_opt ? ? ?) [ #_ %]
    223223#f1 #H3 <(drop_fn_lfn … f1 H3) assumption
     
    227227lemma globalenv_no_minus_one :
    228228 ∀F,V,i,p.
    229   find_funct_ptr … (globalenv F V i p) (mk_block Code (-1)) = None ?.
     229  find_funct_ptr … (globalenv F V i p) (mk_block (*Code*) (-1)) = None ?.
    230230#F #V #i #p
    231231whd in match find_funct_ptr; normalize nodelta
     
    237237lemma globalenv_no_zero :
    238238 ∀F,V,i,p.
    239   find_funct_ptr … (globalenv F V i p) (mk_block Code OZ) = None ?. //
    240 qed.
    241 
     239  find_funct_ptr … (globalenv F V i p) (mk_block (*Code*) OZ) = None ?. //
     240qed.
     241
Note: See TracChangeset for help on using the changeset viewer.