Changeset 2560 for src

Timestamp:

Dec 18, 2012, 4:38:54 PM (8 years ago)

Author:

garnier

Message:

Fix in trace gen for CL

Location:

src/Clight

Files:

• Cexec.ma (modified) (1 diff)
• Csem.ma (modified) (1 diff)

src/Clight/Cexec.ma

@@ -246 +246 @@
   | Ecost l a ⇒
       do 〈v,tr〉 ← exec_expr ge en m a;
-      OK ? 〈v,tr⧺(Echarge l)〉
+      OK ? 〈v,(Echarge l)⧺tr〉
   ]
 ]

src/Clight/Csem.ma

@@ -592 +592 @@
   | eval_Ecost: ∀a,ty,v,l,tr.
       eval_expr ge e m a v tr →
-      eval_expr ge e m (Expr (Ecost l a) ty) v (tr⧺Echarge l)
+      eval_expr ge e m (Expr (Ecost l a) ty) v ((Echarge l)⧺tr)
 
 (* * [eval_lvalue ge e m a r b ofs] defines the evaluation of expression [a]