Changeset 2608 for src/RTLabs


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.

Location:
src/RTLabs
Files:
2 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
  • 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.