- Timestamp:
- Dec 18, 2012, 4:38:54 PM (8 years ago)
- Location:
- src/Clight
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/Cexec.ma
r2468 r2560 246 246 | Ecost l a ⇒ 247 247 do 〈v,tr〉 ← exec_expr ge en m a; 248 OK ? 〈v, tr⧺(Echarge l)〉248 OK ? 〈v,(Echarge l)⧺tr〉 249 249 ] 250 250 ] -
src/Clight/Csem.ma
r2468 r2560 592 592 | eval_Ecost: ∀a,ty,v,l,tr. 593 593 eval_expr ge e m a v tr → 594 eval_expr ge e m (Expr (Ecost l a) ty) v ( tr⧺Echarge l)594 eval_expr ge e m (Expr (Ecost l a) ty) v ((Echarge l)⧺tr) 595 595 596 596 (* * [eval_lvalue ge e m a r b ofs] defines the evaluation of expression [a]
Note: See TracChangeset
for help on using the changeset viewer.