Changeset 1874 for src/Clight


Ignore:
Timestamp:
Apr 4, 2012, 6:48:25 PM (8 years ago)
Author:
campbell
Message:

First cut at using back-end memory model throughout.
Note the correction to BEValues.

Location:
src/Clight
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r1713 r1874  
    294294| cons h vars ⇒
    295295  let 〈id,ty〉 ≝ h in
    296   let 〈m1,b1〉 ≝ alloc m 0 (sizeof ty) Any in
     296  let 〈m1,b1〉 ≝ alloc becontentT m 0 (sizeof ty) Any in
    297297      exec_alloc_variables (add ?? en id b1) m1 vars
    298298].
     
    380380      | Kstop ⇒
    381381          match fn_return f with
    382           [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
     382          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list becontentT m (blocks_of_env e))〉
    383383          | _ ⇒ Wrong ??? (msg NonsenseState)
    384384          ]
    385385      | Kcall _ _ _ _ ⇒
    386386          match fn_return f with
    387           [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
     387          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list becontentT m (blocks_of_env e))〉
    388388          | _ ⇒ Wrong ??? (msg NonsenseState)
    389389          ]
     
    446446    match a_opt with
    447447    [ None ⇒ match fn_return f with
    448       [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉
     448      [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list becontentT m (blocks_of_env e))〉
    449449      | _ ⇒ Wrong ??? (msg ReturnMismatch)
    450450      ]
     
    454454        | inr _ ⇒
    455455          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    456           ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉
     456          ret ? 〈tr, Returnstate v (call_cont k) (free_list becontentT m (blocks_of_env e))〉
    457457        ]
    458458    ]
  • src/Clight/Csem.ma

    r1872 r1874  
    526526  | alloc_variables_cons:
    527527      ∀e,m,id,ty,vars,m1,b1,m2,e2.
    528       alloc m 0 (sizeof ty) Any = 〈m1, b1〉 →
    529       alloc_variables (add … e id b1) m1 vars e2 m2 →
     528      alloc becontentT m 0 (sizeof ty) Any = 〈m1, b1〉 →
     529      alloc_variables (add … e id (pi1 … b1)) m1 vars e2 m2 →
    530530      alloc_variables e m (〈id, ty〉 :: vars) e2 m2.
    531531
     
    11371137      fn_return f = Tvoid →
    11381138      step ge (State f (Sreturn (None ?)) k e m)
    1139            E0 (Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e)))
     1139           E0 (Returnstate Vundef (call_cont k) (free_list becontentT m (blocks_of_env e)))
    11401140  | step_return_1: ∀f,a,k,e,m,v,tr.
    11411141      fn_return f ≠ Tvoid →
    11421142      eval_expr ge e m a v tr →
    11431143      step ge (State f (Sreturn (Some ? a)) k e m)
    1144            tr (Returnstate v (call_cont k) (free_list m (blocks_of_env e)))
     1144           tr (Returnstate v (call_cont k) (free_list becontentT m (blocks_of_env e)))
    11451145  | step_skip_call: ∀f,k,e,m.
    11461146      is_call_cont k →
    11471147      fn_return f = Tvoid →
    11481148      step ge (State f Sskip k e m)
    1149            E0 (Returnstate Vundef k (free_list m (blocks_of_env e)))
     1149           E0 (Returnstate Vundef k (free_list becontentT m (blocks_of_env e)))
    11501150
    11511151  | step_switch: ∀f,a,sl,k,e,m,sz,n,tr.
Note: See TracChangeset for help on using the changeset viewer.