diff --git a/CHANGELOG.md b/CHANGELOG.md index 33bab107e..f266d8838 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -33,6 +33,10 @@ ([PR #227](https://github.com/jasmin-lang/jasmin/pull/227); fixes [#190](https://github.com/jasmin-lang/jasmin/issues/190)). +- Fix a failing assertion in extraction to EasyCrypt for constant-time + ([PR #229](https://github.com/jasmin-lang/jasmin/pull/229); + fixes [#202](https://github.com/jasmin-lang/jasmin/issues/202)). + ## New features - Fill an array with “random” data using `p = #randombytes(p);` diff --git a/compiler/src/toEC.ml b/compiler/src/toEC.ml index d1e8b304e..ae4e867b0 100644 --- a/compiler/src/toEC.ml +++ b/compiler/src/toEC.ml @@ -1086,7 +1086,7 @@ module Leak = struct let rec init_aux_i env i = match i.i_desc with - | Cassgn (lv, _, _, _) -> add_aux env [ty_lval lv] + | Cassgn (lv, _, _, e) -> add_aux (add_aux env [ty_lval lv]) [ty_expr e] | Copn (lvs, _, _, _) -> add_aux env (List.map ty_lval lvs) | Ccall(_, lvs, _, _) | Csyscall(lvs, _, _)-> if lvs = [] then env