diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog index f5f780dd7d02bf57a3c44434d4fb7f2e60cd61f2..ab6ca4885ad499bb3af93b8159fdb54860fc428d 100644 --- a/src/plugins/e-acsl/doc/Changelog +++ b/src/plugins/e-acsl/doc/Changelog @@ -25,6 +25,9 @@ Plugin E-ACSL <next-release> ############################################################################### +-* E-ACSL [2024-09-26] fix usage of structural equality of terms; + By using physical equality we ensure that structurally + identical terms are translated according to their context. -* E-ACSL [2024-09-16] fix logic variable escaping its scope -* E-ACSL [2024-09-03] handle negative integers generated by RTE - E-ACSL [2024-09-03] add support for labelled logic functions in case diff --git a/src/plugins/e-acsl/src/analyses/labels.ml b/src/plugins/e-acsl/src/analyses/labels.ml index adc84060c757cbc13e40932b813a3cf9276a4f00..9fc9626a8429ee408b64305c23afcdcba6483389 100644 --- a/src/plugins/e-acsl/src/analyses/labels.ml +++ b/src/plugins/e-acsl/src/analyses/labels.ml @@ -65,6 +65,9 @@ let at_data_for_stmts: At_data.t list ref Stmt.Hashtbl.t = statement [stmt]. *) let add_at_for_stmt data stmt = let stmt = get_first_inner_stmt stmt in + (* Note that the error field is not taken into account in At_data.equal. + Therefore we cannot just write: + At_data.Hashtbl.replace ats_tbl data data; let old_data = data in *) let ats_ref = try Stmt.Hashtbl.find at_data_for_stmts stmt