From a95f7cc9eb63f4cd9803e401671b07f5abdcfd3b Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Thu, 26 Sep 2024 14:42:30 +0200
Subject: [PATCH] [e-acsl] add changelog entry for physical term equality
also: add clarifying comment to the Labels module
---
src/plugins/e-acsl/doc/Changelog | 3 +++
src/plugins/e-acsl/src/analyses/labels.ml | 3 +++
2 files changed, 6 insertions(+)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index f5f780dd7d0..ab6ca4885ad 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 adc84060c75..9fc9626a842 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
--
GitLab