Changeset 2560


Ignore:
Timestamp:
Dec 18, 2012, 4:38:54 PM (7 years ago)
Author:
garnier
Message:

Fix in trace gen for CL

Location:
src/Clight
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r2468 r2560  
    246246  | Ecost l a ⇒
    247247      do 〈v,tr〉 ← exec_expr ge en m a;
    248       OK ? 〈v,tr⧺(Echarge l)
     248      OK ? 〈v,(Echarge l)⧺tr
    249249  ]
    250250]
  • src/Clight/Csem.ma

    r2468 r2560  
    592592  | eval_Ecost: ∀a,ty,v,l,tr.
    593593      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)
    595595
    596596(* * [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.