diff --git a/src/plugins/e-acsl/tests/constructs/axiomatic.c b/src/plugins/e-acsl/tests/constructs/axiomatic.c
index 699ce476bb9afe309d9d9d7b3fe29353a91b5fe7..19e5dd287f1aee58ea852f185b6087d792e31904 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 f716c7a89ac0efe6e774df6c2e8aacf4864d1c66..ebbe084569ccc9a1ce67c2624868252d0dae5c32 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 2c280d59d83026b8e9b8da4725c49f1ec35f3e17..c43f0f870083ffa54f24598ca6d1d791d3be94fc 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)
 {