Skip to content

Commit

Permalink
Fixed incorrect variable renaming in bcccc88
Browse files Browse the repository at this point in the history
This issue caused the step counter to not be introduced when
the history constructor was used in a contract.
  • Loading branch information
daniel-larraz committed Oct 3, 2024
1 parent 59c9a53 commit 439da03
Show file tree
Hide file tree
Showing 2 changed files with 14 additions and 6 deletions.
12 changes: 6 additions & 6 deletions src/lustre/lustreAstNormalizer.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1155,25 +1155,25 @@ and normalize_node info map
in
(* Normalize equations and the contract *)
let nitems, gids8, warnings5 = normalize_list (normalize_item info node_id map) items in
let gids7' = union gids7 gids8 in
let gids8' =
let gids6_8 = union gids6 gids8 in
let gids9 =
if exists_reachability_prop_with_bounds ||
not (StringMap.is_empty gids7'.history_vars) then (
not (StringMap.is_empty gids6_8.history_vars) then (
add_step_counter info
)
else
empty ()
in
let gids9 =
let gids10 =
StringMap.fold
(fun id h_id acc ->
union acc (add_history_var_and_equation info id h_id)
)
gids7'.history_vars
gids6_8.history_vars
(empty ())
in
let new_gids = union_list [union_list gids1; union_list gids2; union_list gids3;
gids4; gids5; gids6; gids7'; gids8'; gids9] in
gids4; gids5; gids7; gids6_8; gids9; gids10] in
let old_gids, warnings6 = normalize_gid_equations info map node_id in
let map = StringMap.add node_id (union old_gids new_gids) map in
(node_id, is_extern, params, inputs, outputs, locals, List.flatten nitems, ncontracts),
Expand Down
8 changes: 8 additions & 0 deletions tests/regression/success/history1.lus
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@

node N(x: int) returns (y: int);
(*@contract
guarantee "G1" exists (z: history(x)) y = z + 1;
*)
let
y = x + 1 -> if any bool then x + 1 else pre y;
tel

0 comments on commit 439da03

Please sign in to comment.