Changeset 1988 for src/Clight/Csem.ma


Ignore:
Timestamp:
May 24, 2012, 11:39:27 AM (6 years ago)
Author:
campbell
Message:

Abstraction of the memory contents in the memory models is no longer
necessary.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r1986 r1988  
    526526  | alloc_variables_cons:
    527527      ∀e,m,id,ty,vars,m1,b1,m2,e2.
    528       alloc becontentT m 0 (sizeof ty) Any = 〈m1, b1〉 →
     528      alloc m 0 (sizeof ty) Any = 〈m1, b1〉 →
    529529      alloc_variables (add … e id (pi1 … b1)) m1 vars e2 m2 →
    530530      alloc_variables e m (〈id, ty〉 :: vars) e2 m2.
     
    11391139      fn_return f = Tvoid →
    11401140      step ge (State f (Sreturn (None ?)) k e m)
    1141            E0 (Returnstate Vundef (call_cont k) (free_list becontentT m (blocks_of_env e)))
     1141           E0 (Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e)))
    11421142  | step_return_1: ∀f,a,k,e,m,v,tr.
    11431143      fn_return f ≠ Tvoid →
    11441144      eval_expr ge e m a v tr →
    11451145      step ge (State f (Sreturn (Some ? a)) k e m)
    1146            tr (Returnstate v (call_cont k) (free_list becontentT m (blocks_of_env e)))
     1146           tr (Returnstate v (call_cont k) (free_list m (blocks_of_env e)))
    11471147  | step_skip_call: ∀f,k,e,m.
    11481148      is_call_cont k →
    11491149      fn_return f = Tvoid →
    11501150      step ge (State f Sskip k e m)
    1151            E0 (Returnstate Vundef k (free_list becontentT m (blocks_of_env e)))
     1151           E0 (Returnstate Vundef k (free_list m (blocks_of_env e)))
    11521152
    11531153  | step_switch: ∀f,a,sl,k,e,m,sz,n,tr.
Note: See TracChangeset for help on using the changeset viewer.