From 2491fba9f905e2e38e3a0577347d96712ea3ab63 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 26 Sep 2024 14:49:43 +0200
Subject: [PATCH] [e-acsl] update error message in oracle - these tests do not
 use anymore datacons, another error is thus triggered

---
 src/plugins/e-acsl/tests/format/oracle/printf.res.oracle  | 8 ++++++--
 src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle       | 4 +++-
 .../e-acsl/tests/temporal/oracle/t_memcpy.res.oracle      | 4 +++-
 3 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
index 6ea6f74635e..61c1a73899c 100644
--- a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
@@ -46,9 +46,13 @@
   is not yet supported.
   Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:196: Warning: 
-  E-ACSL construct `datacons' is not yet supported. Ignoring annotation.
+  E-ACSL construct `logic functions or predicates performing read accesses'
+  is not yet supported.
+  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:204: Warning: 
-  E-ACSL construct `datacons' is not yet supported. Ignoring annotation.
+  E-ACSL construct `logic functions or predicates performing read accesses'
+  is not yet supported.
+  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:192: Warning: 
   Some assumes clauses could not be translated.
   Ignoring complete and disjoint behaviors annotations.
diff --git a/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle
index d6ab15b134f..66d16674c03 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle
+++ b/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle
@@ -7,7 +7,9 @@
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:151: Warning: 
-  E-ACSL construct `datacons' is not yet supported. Ignoring annotation.
+  E-ACSL construct `logic functions or predicates performing read accesses'
+  is not yet supported.
+  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:138: Warning: 
   no assigns clause generated for function valid_read_or_empty because pointers as arguments is not yet supported
 [e-acsl] FRAMAC_SHARE/libc/string.h:137: Warning: 
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
index c9851298903..4e14e33da38 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
@@ -7,7 +7,9 @@
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:151: Warning: 
-  E-ACSL construct `datacons' is not yet supported. Ignoring annotation.
+  E-ACSL construct `logic functions or predicates performing read accesses'
+  is not yet supported.
+  Ignoring annotation.
 [e-acsl] FRAMAC_SHARE/libc/string.h:113: Warning: 
   no assigns clause generated for function valid_read_or_empty because pointers as arguments is not yet supported
 [e-acsl] FRAMAC_SHARE/libc/string.h:112: Warning: 
-- 
GitLab