Changeset 2560 for src/Clight/Csem.ma


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

Fix in trace gen for CL

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.