[e-acsl] add pathological typing example

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);
+}

src/plugins/e-acsl/tests/constructs/oracle/axiomatic.res.oracle

+[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'

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)
 {