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_semantics.ma

    r2601 r2608  
    175175        (* CSC: XXX alignment call (concrete_stacksize in OCaml) is missing
    176176           here *)
    177         let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) XData in
     177        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) (* XData *) in
    178178        return 〈E0, State (mk_frame fn locals (f_entry fn) ? sp dst) fs m'〉
    179179    | External fn ⇒
     
    294294| * #fn #args #retdst #stk #m #tr #s'
    295295  whd in ⊢ (??%? → ?);
    296   [ @bind_res_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?);
     296  [ @bind_res_value #loc #Eloc cases (alloc m O ? (*?*)) #m' #b whd in ⊢ (??%? → ?);
    297297    #E destruct %3
    298298  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
     
    342342| * #fn #args #retdst #stk #m #tr #fd' #args' #dst' #fs' #m'
    343343  whd in ⊢ (??%? → ?);
    344   [ @bind_res_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?);
     344  [ @bind_res_value #loc #Eloc cases (alloc m O ?(*?*)) #m' #b whd in ⊢ (??%? → ?);
    345345    #E destruct
    346346  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
Note: See TracChangeset for help on using the changeset viewer.