From 3d7726544b245580d11f2d027324d2636a5a9e7e Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Sun, 25 Aug 2024 00:16:35 +0200
Subject: [PATCH] [e-acsl] add pathological typing example

---
 .../e-acsl/tests/constructs/axiomatic.c       | 18 ++++++
 .../constructs/oracle/axiomatic.res.oracle    |  8 +++
 .../tests/constructs/oracle/gen_axiomatic.c   | 59 +++++++++++++++++++
 3 files changed, 85 insertions(+)

diff --git a/src/plugins/e-acsl/tests/constructs/axiomatic.c b/src/plugins/e-acsl/tests/constructs/axiomatic.c
index 699ce476bb9..19e5dd287f1 100644
--- a/src/plugins/e-acsl/tests/constructs/axiomatic.c
+++ b/src/plugins/e-acsl/tests/constructs/axiomatic.c
@@ -16,3 +16,21 @@ void f(int s) {
 int main() {
   f(2);
 }
+
+/*@
+
+axiomatic g {
+  logic ℤ g(int c)
+    reads c;
+}
+
+@*/
+
+/*@ ensures g(t) == 0; */
+int h(const int t) {
+  return 0;
+}
+
+int i() {
+  h(1);
+}
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/axiomatic.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/axiomatic.res.oracle
index f716c7a89ac..ebbe084569c 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/axiomatic.res.oracle
+++ b/src/plugins/e-acsl/tests/constructs/oracle/axiomatic.res.oracle
@@ -1,4 +1,12 @@
+[kernel:CERT:MSC:37] axiomatic.c:29: Warning: 
+  Body of function h falls-through. Adding a return statement
+[kernel:CERT:MSC:37] axiomatic.c:33: Warning: 
+  Body of function i falls-through. Adding a return statement
 [e-acsl] beginning translation.
+[e-acsl] axiomatic.c:28: Warning: 
+  E-ACSL construct `logic functions or predicates performing read accesses'
+  is not yet supported.
+  Ignoring annotation.
 [e-acsl] axiomatic.c:11: Warning: 
   E-ACSL construct
   `logic functions or predicates with no definition nor reads clause'
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_axiomatic.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_axiomatic.c
index 2c280d59d83..c43f0f87008 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_axiomatic.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_axiomatic.c
@@ -32,6 +32,65 @@ int main(void)
   return __retres;
 }
 
+/*@ axiomatic g {
+      logic integer g(char c) 
+        reads c;
+      
+      }
+
+*/
+/*@ ensures g(\old(s)) == 0; */
+char __gen_e_acsl_h(char const s);
+
+char h(char const s)
+{
+  char __retres;
+  {
+    __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+    __gen_e_acsl_assert_data.blocking = 1;
+    __gen_e_acsl_assert_data.kind = "Assertion";
+    __gen_e_acsl_assert_data.pred_txt = "\\false";
+    __gen_e_acsl_assert_data.file = "axiomatic.c";
+    __gen_e_acsl_assert_data.fct = "h";
+    __gen_e_acsl_assert_data.line = 29;
+    __gen_e_acsl_assert_data.name = "missing_return";
+    __e_acsl_assert(0,& __gen_e_acsl_assert_data);
+  }
+  /*@ assert missing_return: \false; */ ;
+  __retres = (char)0;
+  return __retres;
+}
+
+int i(void)
+{
+  int __retres;
+  __gen_e_acsl_h((char)'c');
+  {
+    __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+    __gen_e_acsl_assert_data.blocking = 1;
+    __gen_e_acsl_assert_data.kind = "Assertion";
+    __gen_e_acsl_assert_data.pred_txt = "\\false";
+    __gen_e_acsl_assert_data.file = "axiomatic.c";
+    __gen_e_acsl_assert_data.fct = "i";
+    __gen_e_acsl_assert_data.line = 33;
+    __gen_e_acsl_assert_data.name = "missing_return";
+    __e_acsl_assert(0,& __gen_e_acsl_assert_data);
+  }
+  /*@ assert missing_return: \false; */ ;
+  __retres = 0;
+  return __retres;
+}
+
+/*@ ensures g(\old(s)) == 0; */
+char __gen_e_acsl_h(char const s)
+{
+  char __gen_e_acsl_at;
+  char __retres;
+  __gen_e_acsl_at = s;
+  __retres = h(s);
+  return __retres;
+}
+
 /*@ ensures p(\old(s)); */
 void __gen_e_acsl_f(int s)
 {
-- 
GitLab