Changeset 175 for C-semantics/Csem.ma


Ignore:
Timestamp:
Oct 13, 2010, 12:19:22 PM (9 years ago)
Author:
campbell
Message:

Add cost labels, with the semantics that the label is added to the
event trace.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Csem.ma

    r155 r175  
    568568  [e] is the current environment and [m] is the current memory state. *)
    569569
    570 ninductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → Prop ≝
     570ninductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → trace → Prop ≝
    571571  | eval_Econst_int:   ∀i,ty.
    572       eval_expr ge e m (Expr (Econst_int i) ty) (Vint i)
     572      eval_expr ge e m (Expr (Econst_int i) ty) (Vint i) E0
    573573  | eval_Econst_float:   ∀f,ty.
    574       eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f)
    575   | eval_Elvalue: ∀a,ty,psp,loc,ofs,v.
    576       eval_lvalue ge e m (Expr a ty) psp loc ofs ->
    577       load_value_of_type ty m psp loc ofs = Some ? v ->
    578       eval_expr ge e m (Expr a ty) v
    579   | eval_Eaddrof: ∀a,ty,psp,loc,ofs.
    580       eval_lvalue ge e m a psp loc ofs ->
    581       eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr psp loc ofs)
     574      eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f) E0
     575  | eval_Elvalue: ∀a,ty,psp,loc,ofs,v,tr.
     576      eval_lvalue ge e m (Expr a ty) psp loc ofs tr →
     577      load_value_of_type ty m psp loc ofs = Some ? v
     578      eval_expr ge e m (Expr a ty) v tr
     579  | eval_Eaddrof: ∀a,ty,psp,loc,ofs,tr.
     580      eval_lvalue ge e m a psp loc ofs tr →
     581      eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr psp loc ofs) tr
    582582  | eval_Esizeof: ∀ty',ty.
    583       eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty')))
    584   | eval_Eunop:  ∀op,a,ty,v1,v.
    585       eval_expr ge e m a v1 ->
    586       sem_unary_operation op v1 (typeof a) = Some ? v ->
    587       eval_expr ge e m (Expr (Eunop op a) ty) v
    588   | eval_Ebinop: ∀op,a1,a2,ty,v1,v2,v.
    589       eval_expr ge e m a1 v1 ->
    590       eval_expr ge e m a2 v2 ->
    591       sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some ? v ->
    592       eval_expr ge e m (Expr (Ebinop op a1 a2) ty) v
    593   | eval_Econdition_true: ∀a1,a2,a3,ty,v1,v2.
    594       eval_expr ge e m a1 v1 ->
    595       is_true v1 (typeof a1) ->
    596       eval_expr ge e m a2 v2 ->
    597       eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v2
    598   | eval_Econdition_false: ∀a1,a2,a3,ty,v1,v3.
    599       eval_expr ge e m a1 v1 ->
    600       is_false v1 (typeof a1) ->
    601       eval_expr ge e m a3 v3 ->
    602       eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v3
    603   | eval_Eorbool_1: ∀a1,a2,ty,v1.
    604       eval_expr ge e m a1 v1 ->
    605       is_true v1 (typeof a1) ->
    606       eval_expr ge e m (Expr (Eorbool a1 a2) ty) Vtrue
    607   | eval_Eorbool_2: ∀a1,a2,ty,v1,v2,v.
    608       eval_expr ge e m a1 v1 ->
    609       is_false v1 (typeof a1) ->
    610       eval_expr ge e m a2 v2 ->
    611       bool_of_val v2 (typeof a2) v ->
    612       eval_expr ge e m (Expr (Eorbool a1 a2) ty) v
    613   | eval_Eandbool_1: ∀a1,a2,ty,v1.
    614       eval_expr ge e m a1 v1 ->
    615       is_false v1 (typeof a1) ->
    616       eval_expr ge e m (Expr (Eandbool a1 a2) ty) Vfalse
    617   | eval_Eandbool_2: ∀a1,a2,ty,v1,v2,v.
    618       eval_expr ge e m a1 v1 ->
    619       is_true v1 (typeof a1) ->
    620       eval_expr ge e m a2 v2 ->
    621       bool_of_val v2 (typeof a2) v ->
    622       eval_expr ge e m (Expr (Eandbool a1 a2) ty) v
    623   | eval_Ecast:   ∀a,ty,ty',v1,v.
    624       eval_expr ge e m a v1 ->
    625       cast m v1 (typeof a) ty v ->
    626       eval_expr ge e m (Expr (Ecast ty a) ty') v
     583      eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty'))) E0
     584  | eval_Eunop:  ∀op,a,ty,v1,v,tr.
     585      eval_expr ge e m a v1 tr →
     586      sem_unary_operation op v1 (typeof a) = Some ? v →
     587      eval_expr ge e m (Expr (Eunop op a) ty) v tr
     588  | eval_Ebinop: ∀op,a1,a2,ty,v1,v2,v,tr1,tr2.
     589      eval_expr ge e m a1 v1 tr1 →
     590      eval_expr ge e m a2 v2 tr2 →
     591      sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some ? v →
     592      eval_expr ge e m (Expr (Ebinop op a1 a2) ty) v (tr1⧺tr2)
     593  | eval_Econdition_true: ∀a1,a2,a3,ty,v1,v2,tr1,tr2.
     594      eval_expr ge e m a1 v1 tr1 →
     595      is_true v1 (typeof a1) →
     596      eval_expr ge e m a2 v2 tr2 →
     597      eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v2 (tr1⧺tr2)
     598  | eval_Econdition_false: ∀a1,a2,a3,ty,v1,v3,tr1,tr2.
     599      eval_expr ge e m a1 v1 tr1 →
     600      is_false v1 (typeof a1) →
     601      eval_expr ge e m a3 v3 tr2 →
     602      eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v3 (tr1⧺tr2)
     603  | eval_Eorbool_1: ∀a1,a2,ty,v1,tr.
     604      eval_expr ge e m a1 v1 tr →
     605      is_true v1 (typeof a1) →
     606      eval_expr ge e m (Expr (Eorbool a1 a2) ty) Vtrue tr
     607  | eval_Eorbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2.
     608      eval_expr ge e m a1 v1 tr1 →
     609      is_false v1 (typeof a1) →
     610      eval_expr ge e m a2 v2 tr2 →
     611      bool_of_val v2 (typeof a2) v →
     612      eval_expr ge e m (Expr (Eorbool a1 a2) ty) v (tr1⧺tr2)
     613  | eval_Eandbool_1: ∀a1,a2,ty,v1,tr.
     614      eval_expr ge e m a1 v1 tr →
     615      is_false v1 (typeof a1) →
     616      eval_expr ge e m (Expr (Eandbool a1 a2) ty) Vfalse tr
     617  | eval_Eandbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2.
     618      eval_expr ge e m a1 v1 tr1 →
     619      is_true v1 (typeof a1) →
     620      eval_expr ge e m a2 v2 tr2 →
     621      bool_of_val v2 (typeof a2) v →
     622      eval_expr ge e m (Expr (Eandbool a1 a2) ty) v (tr1⧺tr2)
     623  | eval_Ecast:   ∀a,ty,ty',v1,v,tr.
     624      eval_expr ge e m a v1 tr →
     625      cast m v1 (typeof a) ty v →
     626      eval_expr ge e m (Expr (Ecast ty a) ty') v tr
     627  | eval_Ecost: ∀a,ty,v,l,tr.
     628      eval_expr ge e m a v tr →
     629      eval_expr ge e m (Expr (Ecost l a) ty) v (tr⧺Echarge l)
    627630
    628631(* * [eval_lvalue ge e m a b ofs] defines the evaluation of expression [a]
     
    630633  that contains the value of the expression [a]. *)
    631634
    632 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → memory_space → block -> int -> Prop ≝
     635with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → memory_space → block → int → trace → Prop ≝
    633636  | eval_Evar_local:   ∀id,l,ty.
    634637      (* XXX notation? e!id*) get ??? id e = Some ? l →
    635       eval_lvalue ge e m (Expr (Evar id) ty) Any l zero
     638      eval_lvalue ge e m (Expr (Evar id) ty) Any l zero E0
    636639  | eval_Evar_global: ∀id,sp,l,ty.
    637       (* XXX e!id *) get ??? id e = None ? ->
    638       find_symbol ?? ge id = Some ? 〈sp,l〉 ->
    639       eval_lvalue ge e m (Expr (Evar id) ty) sp l zero
    640   | eval_Ederef: ∀a,ty,psp,l,ofs.
    641       eval_expr ge e m a (Vptr psp l ofs) ->
    642       eval_lvalue ge e m (Expr (Ederef a) ty) psp l ofs
    643  | eval_Efield_struct:   ∀a,i,ty,psp,l,ofs,id,fList,delta.
    644       eval_lvalue ge e m a psp l ofs ->
    645       typeof a = Tstruct id fList ->
    646       field_offset i fList = OK ? delta ->
    647       eval_lvalue ge e m (Expr (Efield a i) ty) psp l (add ofs (repr delta))
    648  | eval_Efield_union:   ∀a,i,ty,psp,l,ofs,id,fList.
    649       eval_lvalue ge e m a psp l ofs ->
    650       typeof a = Tunion id fList ->
    651       eval_lvalue ge e m (Expr (Efield a i) ty) psp l ofs.
     640      (* XXX e!id *) get ??? id e = None ?
     641      find_symbol ?? ge id = Some ? 〈sp,l〉
     642      eval_lvalue ge e m (Expr (Evar id) ty) sp l zero E0
     643  | eval_Ederef: ∀a,ty,psp,l,ofs,tr.
     644      eval_expr ge e m a (Vptr psp l ofs) tr →
     645      eval_lvalue ge e m (Expr (Ederef a) ty) psp l ofs tr
     646 | eval_Efield_struct:   ∀a,i,ty,psp,l,ofs,id,fList,delta,tr.
     647      eval_lvalue ge e m a psp l ofs tr →
     648      typeof a = Tstruct id fList
     649      field_offset i fList = OK ? delta
     650      eval_lvalue ge e m (Expr (Efield a i) ty) psp l (add ofs (repr delta)) tr
     651 | eval_Efield_union:   ∀a,i,ty,psp,l,ofs,id,fList,tr.
     652      eval_lvalue ge e m a psp l ofs tr →
     653      typeof a = Tunion id fList
     654      eval_lvalue ge e m (Expr (Efield a i) ty) psp l ofs tr.
    652655
    653656(*
     
    659662  expressions [al] to their values [vl]. *)
    660663
    661 ninductive eval_exprlist (ge:genv) (e:env) (m:mem) : list expr -> list val -> Prop :=
     664ninductive eval_exprlist (ge:genv) (e:env) (m:mem) : list expr → list val → trace → Prop ≝
    662665  | eval_Enil:
    663       eval_exprlist ge e m (nil ?) (nil ?)
    664   | eval_Econs:   ∀a,bl,v,vl.
    665       eval_expr ge e m a v ->
    666       eval_exprlist ge e m bl vl ->
    667       eval_exprlist ge e m (a :: bl) (v :: vl).
     666      eval_exprlist ge e m (nil ?) (nil ?) E0
     667  | eval_Econs:   ∀a,bl,v,vl,tr1,tr2.
     668      eval_expr ge e m a v tr1 →
     669      eval_exprlist ge e m bl vl tr2 →
     670      eval_exprlist ge e m (a :: bl) (v :: vl) (tr1⧺tr2).
    668671
    669672(*End EXPR.*)
     
    783786(* * Transition relation *)
    784787
    785 ninductive step (ge:genv) : state -> trace -> state -> Prop :=
    786 
    787   | step_assign:   ∀f,a1,a2,k,e,m,psp,loc,ofs,v2,m'.
    788       eval_lvalue ge e m a1 psp loc ofs ->
    789       eval_expr ge e m a2 v2 ->
    790       store_value_of_type (typeof a1) m psp loc ofs v2 = Some ? m' ->
     788(* XXX: note that cost labels in exprs expose a particular eval order. *)
     789
     790ninductive step (ge:genv) : state → trace → state → Prop ≝
     791
     792  | step_assign:   ∀f,a1,a2,k,e,m,psp,loc,ofs,v2,m',tr1,tr2.
     793      eval_lvalue ge e m a1 psp loc ofs tr1 →
     794      eval_expr ge e m a2 v2 tr2 →
     795      store_value_of_type (typeof a1) m psp loc ofs v2 = Some ? m' →
    791796      step ge (State f (Sassign a1 a2) k e m)
    792            E0 (State f Sskip k e m')
    793 
    794   | step_call_none:   ∀f,a,al,k,e,m,vf,vargs,fd.
    795       eval_expr ge e m a vf ->
    796       eval_exprlist ge e m al vargs ->
    797       find_funct ?? ge vf = Some ? fd ->
    798       type_of_fundef fd = typeof a ->
     797           (tr1⧺tr2) (State f Sskip k e m')
     798
     799  | step_call_none:   ∀f,a,al,k,e,m,vf,vargs,fd,tr1,tr2.
     800      eval_expr ge e m a vf tr1 →
     801      eval_exprlist ge e m al vargs tr2 →
     802      find_funct ?? ge vf = Some ? fd
     803      type_of_fundef fd = typeof a
    799804      step ge (State f (Scall (None ?) a al) k e m)
    800            E0 (Callstate fd vargs (Kcall (None ?) f e k) m)
    801 
    802   | step_call_some:   ∀f,lhs,a,al,k,e,m,psp,loc,ofs,vf,vargs,fd.
    803       eval_lvalue ge e m lhs psp loc ofs ->
    804       eval_expr ge e m a vf ->
    805       eval_exprlist ge e m al vargs ->
    806       find_funct ?? ge vf = Some ? fd ->
    807       type_of_fundef fd = typeof a ->
     805           (tr1⧺tr2) (Callstate fd vargs (Kcall (None ?) f e k) m)
     806
     807  | step_call_some:   ∀f,lhs,a,al,k,e,m,psp,loc,ofs,vf,vargs,fd,tr1,tr2,tr3.
     808      eval_lvalue ge e m lhs psp loc ofs tr1 →
     809      eval_expr ge e m a vf tr2 →
     810      eval_exprlist ge e m al vargs tr3 →
     811      find_funct ?? ge vf = Some ? fd
     812      type_of_fundef fd = typeof a
    808813      step ge (State f (Scall (Some ? lhs) a al) k e m)
    809            E0 (Callstate fd vargs (Kcall (Some ? 〈〈〈psp, loc〉, ofs〉, typeof lhs〉) f e k) m)
     814           (tr1⧺tr2⧺tr3) (Callstate fd vargs (Kcall (Some ? 〈〈〈psp, loc〉, ofs〉, typeof lhs〉) f e k) m)
    810815
    811816  | step_seq:  ∀f,s1,s2,k,e,m.
     
    822827           E0 (State f Sbreak k e m)
    823828
    824   | step_ifthenelse_true:  ∀f,a,s1,s2,k,e,m,v1.
    825       eval_expr ge e m a v1 ->
    826       is_true v1 (typeof a) ->
     829  | step_ifthenelse_true:  ∀f,a,s1,s2,k,e,m,v1,tr.
     830      eval_expr ge e m a v1 tr →
     831      is_true v1 (typeof a)
    827832      step ge (State f (Sifthenelse a s1 s2) k e m)
    828            E0 (State f s1 k e m)
    829   | step_ifthenelse_false: ∀f,a,s1,s2,k,e,m,v1.
    830       eval_expr ge e m a v1 ->
    831       is_false v1 (typeof a) ->
     833           tr (State f s1 k e m)
     834  | step_ifthenelse_false: ∀f,a,s1,s2,k,e,m,v1,tr.
     835      eval_expr ge e m a v1 tr →
     836      is_false v1 (typeof a)
    832837      step ge (State f (Sifthenelse a s1 s2) k e m)
    833            E0 (State f s2 k e m)
    834 
    835   | step_while_false: ∀f,a,s,k,e,m,v.
    836       eval_expr ge e m a v ->
    837       is_false v (typeof a) ->
     838           tr (State f s2 k e m)
     839
     840  | step_while_false: ∀f,a,s,k,e,m,v,tr.
     841      eval_expr ge e m a v tr →
     842      is_false v (typeof a)
    838843      step ge (State f (Swhile a s) k e m)
    839            E0 (State f Sskip k e m)
    840   | step_while_true: ∀f,a,s,k,e,m,v.
    841       eval_expr ge e m a v ->
    842       is_true v (typeof a) ->
     844           tr (State f Sskip k e m)
     845  | step_while_true: ∀f,a,s,k,e,m,v,tr.
     846      eval_expr ge e m a v tr →
     847      is_true v (typeof a)
    843848      step ge (State f (Swhile a s) k e m)
    844            E0 (State f s (Kwhile a s k) e m)
     849           tr (State f s (Kwhile a s k) e m)
    845850  | step_skip_or_continue_while: ∀f,x,a,s,k,e,m.
    846       x = Sskip ∨ x = Scontinue ->
     851      x = Sskip ∨ x = Scontinue
    847852      step ge (State f x (Kwhile a s k) e m)
    848853           E0 (State f (Swhile a s) k e m)
     
    854859      step ge (State f (Sdowhile a s) k e m)
    855860        E0 (State f s (Kdowhile a s k) e m)
    856   | step_skip_or_continue_dowhile_false: ∀f,x,a,s,k,e,m,v.
    857       x = Sskip ∨ x = Scontinue ->
    858       eval_expr ge e m a v ->
    859       is_false v (typeof a) ->
     861  | step_skip_or_continue_dowhile_false: ∀f,x,a,s,k,e,m,v,tr.
     862      x = Sskip ∨ x = Scontinue
     863      eval_expr ge e m a v tr →
     864      is_false v (typeof a)
    860865      step ge (State f x (Kdowhile a s k) e m)
    861            E0 (State f Sskip k e m)
    862   | step_skip_or_continue_dowhile_true: ∀f,x,a,s,k,e,m,v.
    863       x = Sskip ∨ x = Scontinue ->
    864       eval_expr ge e m a v ->
    865       is_true v (typeof a) ->
     866           tr (State f Sskip k e m)
     867  | step_skip_or_continue_dowhile_true: ∀f,x,a,s,k,e,m,v,tr.
     868      x = Sskip ∨ x = Scontinue
     869      eval_expr ge e m a v tr →
     870      is_true v (typeof a)
    866871      step ge (State f x (Kdowhile a s k) e m)
    867            E0 (State f (Sdowhile a s) k e m)
     872           tr (State f (Sdowhile a s) k e m)
    868873  | step_break_dowhile: ∀f,a,s,k,e,m.
    869874      step ge (State f Sbreak (Kdowhile a s k) e m)
     
    871876
    872877  | step_for_start: ∀f,a1,a2,a3,s,k,e,m.
    873       a1 ≠ Sskip ->
     878      a1 ≠ Sskip
    874879      step ge (State f (Sfor a1 a2 a3 s) k e m)
    875880           E0 (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m)
    876   | step_for_false: ∀f,a2,a3,s,k,e,m,v.
    877       eval_expr ge e m a2 v ->
    878       is_false v (typeof a2) ->
     881  | step_for_false: ∀f,a2,a3,s,k,e,m,v,tr.
     882      eval_expr ge e m a2 v tr →
     883      is_false v (typeof a2)
    879884      step ge (State f (Sfor Sskip a2 a3 s) k e m)
    880            E0 (State f Sskip k e m)
    881   | step_for_true: ∀f,a2,a3,s,k,e,m,v.
    882       eval_expr ge e m a2 v ->
    883       is_true v (typeof a2) ->
     885           tr (State f Sskip k e m)
     886  | step_for_true: ∀f,a2,a3,s,k,e,m,v,tr.
     887      eval_expr ge e m a2 v tr →
     888      is_true v (typeof a2)
    884889      step ge (State f (Sfor Sskip a2 a3 s) k e m)
    885            E0 (State f s (Kfor2 a2 a3 s k) e m)
     890           tr (State f s (Kfor2 a2 a3 s k) e m)
    886891  | step_skip_or_continue_for2: ∀f,x,a2,a3,s,k,e,m.
    887       x = Sskip ∨ x = Scontinue ->
     892      x = Sskip ∨ x = Scontinue
    888893      step ge (State f x (Kfor2 a2 a3 s k) e m)
    889894           E0 (State f a3 (Kfor3 a2 a3 s k) e m)
     
    896901
    897902  | step_return_0: ∀f,k,e,m.
    898       fn_return f = Tvoid ->
     903      fn_return f = Tvoid
    899904      step ge (State f (Sreturn (None ?)) k e m)
    900905           E0 (Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e)))
    901   | step_return_1: ∀f,a,k,e,m,v.
    902       fn_return f ≠ Tvoid ->
    903       eval_expr ge e m a v ->
     906  | step_return_1: ∀f,a,k,e,m,v,tr.
     907      fn_return f ≠ Tvoid
     908      eval_expr ge e m a v tr →
    904909      step ge (State f (Sreturn (Some ? a)) k e m)
    905            E0 (Returnstate v (call_cont k) (free_list m (blocks_of_env e)))
     910           tr (Returnstate v (call_cont k) (free_list m (blocks_of_env e)))
    906911  | step_skip_call: ∀f,k,e,m.
    907       is_call_cont k ->
    908       fn_return f = Tvoid ->
     912      is_call_cont k
     913      fn_return f = Tvoid
    909914      step ge (State f Sskip k e m)
    910915           E0 (Returnstate Vundef k (free_list m (blocks_of_env e)))
    911916
    912   | step_switch: ∀f,a,sl,k,e,m,n.
    913       eval_expr ge e m a (Vint n) ->
     917  | step_switch: ∀f,a,sl,k,e,m,n,tr.
     918      eval_expr ge e m a (Vint n) tr →
    914919      step ge (State f (Sswitch a sl) k e m)
    915            E0 (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m)
     920           tr (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m)
    916921  | step_skip_break_switch: ∀f,x,k,e,m.
    917       x = Sskip ∨ x = Sbreak ->
     922      x = Sskip ∨ x = Sbreak
    918923      step ge (State f x (Kswitch k) e m)
    919924           E0 (State f Sskip k e m)
     
    927932
    928933  | step_goto: ∀f,lbl,k,e,m,s',k'.
    929       find_label lbl (fn_body f) (call_cont k) = Some ? 〈s', k'〉 ->
     934      find_label lbl (fn_body f) (call_cont k) = Some ? 〈s', k'〉
    930935      step ge (State f (Sgoto lbl) k e m)
    931936           E0 (State f s' k' e m)
    932937
    933938  | step_internal_function: ∀f,vargs,k,m,e,m1,m2.
    934       alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) e m1 ->
    935       bind_parameters e m1 (fn_params f) vargs m2 ->
     939      alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) e m1
     940      bind_parameters e m1 (fn_params f) vargs m2
    936941      step ge (Callstate (Internal f) vargs k m)
    937942           E0 (State f (fn_body f) k e m2)
    938943
    939944  | step_external_function: ∀id,targs,tres,vargs,k,m,vres,t.
    940       event_match (external_function id targs tres) vargs t vres ->
     945      event_match (external_function id targs tres) vargs t vres
    941946      step ge (Callstate (External id targs tres) vargs k m)
    942947            t (Returnstate vres k m)
     
    947952
    948953  | step_returnstate_1: ∀v,f,e,k,m,m',psp,loc,ofs,ty.
    949       store_value_of_type ty m psp loc ofs v = Some ? m' ->
     954      store_value_of_type ty m psp loc ofs v = Some ? m'
    950955      step ge (Returnstate v (Kcall (Some ? 〈〈〈psp,loc〉, ofs〉, ty〉) f e k) m)
    951            E0 (State f Sskip k e m').
     956           E0 (State f Sskip k e m')
     957           
     958  | step_cost: ∀f,lbl,s,k,e,m.
     959      step ge (State f (Scost lbl s) k e m)
     960           (Echarge lbl) (State f s k e m).
    952961(*
    953962(** * Alternate big-step semantics *)
Note: See TracChangeset for help on using the changeset viewer.