[e-acsl] add test for issue eacsl!177

src/plugins/e-acsl/tests/bts/issue-eacsl-177.c

+/* run.config
+   COMMENT: test for issue e-acsl 177
+   STDOPT: +"-eva-unroll-recursive-calls 100"
+*/
+
+#include<limits.h>
+
+/*@ logic integer f(integer n) =
+    n <= INT_MAX+1 || n >= LONG_MAX+1 ? 0 : f(n + 1) + n; */
+
+int main (void) {
+  /*@ assert f(0) == 0; */ ;
+
+  /*@ assert (\let n = (0 == 0) ? LONG_MAX : -1; f(n) != 0); */
+
+}

src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-177.c

+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
+/*@
+logic ℤ f(ℤ n) =
+  n ≤ 2147483647 + 1 ∨ n ≥ 9223372036854775807L + 1? 0: f(n + 1) + n;
+
+*/
+void __gen_e_acsl_f(__e_acsl_mpz_t *__retres_arg, int n);
+
+void __gen_e_acsl_f_2(__e_acsl_mpz_t *__retres_arg, long n);
+
+void __gen_e_acsl_f_3(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
+
+int main(void)
+{
+  int __retres;
+  {
+    __e_acsl_mpz_t __gen_e_acsl_f_8;
+    __e_acsl_mpz_t __gen_e_acsl__10;
+    int __gen_e_acsl_eq;
+    __gen_e_acsl_f(& __gen_e_acsl_f_8,0);
+    __gmpz_init_set_si(__gen_e_acsl__10,0L);
+    __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f_8),
+                                 (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
+    __e_acsl_assert(__gen_e_acsl_eq == 0,1,"Assertion","main","f(0) == 0",
+                    "tests/bts/issue-eacsl-177.c",12);
+    __gmpz_clear(__gen_e_acsl_f_8);
+    __gmpz_clear(__gen_e_acsl__10);
+  }
+  /*@ assert f(0) ≡ 0; */ ;
+  {
+    long __gen_e_acsl_n_5;
+    __e_acsl_mpz_t __gen_e_acsl_f_10;
+    __e_acsl_mpz_t __gen_e_acsl__11;
+    int __gen_e_acsl_ne;
+    __gen_e_acsl_n_5 = 9223372036854775807L;
+    __gen_e_acsl_f_2(& __gen_e_acsl_f_10,__gen_e_acsl_n_5);
+    __gmpz_init_set_si(__gen_e_acsl__11,0L);
+    __gen_e_acsl_ne = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f_10),
+                                 (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
+    __e_acsl_assert(__gen_e_acsl_ne != 0,1,"Assertion","main",
+                    "\\let n = 0 == 0? 9223372036854775807L: -1; f(n) != 0",
+                    "tests/bts/issue-eacsl-177.c",14);
+    __gmpz_clear(__gen_e_acsl_f_10);
+    __gmpz_clear(__gen_e_acsl__11);
+  }
+  /*@ assert \let n = 0 ≡ 0? 9223372036854775807L: -1; f(n) ≢ 0; */ ;
+  __retres = 0;
+  return __retres;
+}
+
+/*@ assigns *((__e_acsl_mpz_struct *)*__retres_arg);
+    assigns *((__e_acsl_mpz_struct *)*__retres_arg) \from n;
+ */
+void __gen_e_acsl_f(__e_acsl_mpz_t *__retres_arg, int n)
+{
+  int __gen_e_acsl_or;
+  __e_acsl_mpz_t __gen_e_acsl_if_3;
+  if ((long)n <= 2147483648L) __gen_e_acsl_or = 1;
+  else {
+    __e_acsl_mpz_t __gen_e_acsl_n;
+    __e_acsl_mpz_t __gen_e_acsl_;
+    int __gen_e_acsl_ge;
+    __gmpz_init_set_si(__gen_e_acsl_n,(long)n);
+    __gmpz_init_set_ui(__gen_e_acsl_,9223372036854775807UL + 1UL);
+    __gen_e_acsl_ge = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
+                                 (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+    __gen_e_acsl_or = __gen_e_acsl_ge >= 0;
+    __gmpz_clear(__gen_e_acsl_n);
+    __gmpz_clear(__gen_e_acsl_);
+  }
+  if (__gen_e_acsl_or) {
+    __e_acsl_mpz_t __gen_e_acsl__2;
+    __gmpz_init_set_si(__gen_e_acsl__2,0L);
+    __gmpz_init_set(__gen_e_acsl_if_3,
+                    (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+    __gmpz_clear(__gen_e_acsl__2);
+  }
+  else {
+    __e_acsl_mpz_t __gen_e_acsl_f_7;
+    __e_acsl_mpz_t __gen_e_acsl_n_4;
+    __e_acsl_mpz_t __gen_e_acsl_add_5;
+    __gen_e_acsl_f_2(& __gen_e_acsl_f_7,n + 1L);
+    __gmpz_init_set_si(__gen_e_acsl_n_4,(long)n);
+    __gmpz_init(__gen_e_acsl_add_5);
+    __gmpz_add(__gen_e_acsl_add_5,
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl_f_7),
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_4));
+    __gmpz_init_set(__gen_e_acsl_if_3,
+                    (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5));
+    __gmpz_clear(__gen_e_acsl_f_7);
+    __gmpz_clear(__gen_e_acsl_n_4);
+    __gmpz_clear(__gen_e_acsl_add_5);
+  }
+  __gmpz_init_set(*__retres_arg,
+                  (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_3));
+  __gmpz_clear(__gen_e_acsl_if_3);
+  return;
+}
+
+/*@ assigns *((__e_acsl_mpz_struct *)*__retres_arg);
+    assigns *((__e_acsl_mpz_struct *)*__retres_arg) \from n;
+ */
+void __gen_e_acsl_f_2(__e_acsl_mpz_t *__retres_arg, long n)
+{
+  int __gen_e_acsl_or_2;
+  __e_acsl_mpz_t __gen_e_acsl_if_2;
+  if (n <= 2147483648L) __gen_e_acsl_or_2 = 1;
+  else {
+    __e_acsl_mpz_t __gen_e_acsl_n_2;
+    __e_acsl_mpz_t __gen_e_acsl__3;
+    int __gen_e_acsl_ge_2;
+    __gmpz_init_set_si(__gen_e_acsl_n_2,n);
+    __gmpz_init_set_ui(__gen_e_acsl__3,9223372036854775807UL + 1UL);
+    __gen_e_acsl_ge_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
+                                   (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
+    __gen_e_acsl_or_2 = __gen_e_acsl_ge_2 >= 0;
+    __gmpz_clear(__gen_e_acsl_n_2);
+    __gmpz_clear(__gen_e_acsl__3);
+  }
+  if (__gen_e_acsl_or_2) {
+    __e_acsl_mpz_t __gen_e_acsl__4;
+    __gmpz_init_set_si(__gen_e_acsl__4,0L);
+    __gmpz_init_set(__gen_e_acsl_if_2,
+                    (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+    __gmpz_clear(__gen_e_acsl__4);
+  }
+  else {
+    __e_acsl_mpz_t __gen_e_acsl_n_3;
+    __e_acsl_mpz_t __gen_e_acsl__5;
+    __e_acsl_mpz_t __gen_e_acsl_add;
+    __e_acsl_mpz_t __gen_e_acsl_f_6;
+    __e_acsl_mpz_t __gen_e_acsl_add_4;
+    __gmpz_init_set_si(__gen_e_acsl_n_3,n);
+    __gmpz_init_set_si(__gen_e_acsl__5,1L);
+    __gmpz_init(__gen_e_acsl_add);
+    __gmpz_add(__gen_e_acsl_add,
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_3),
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
+    /*@ assert
+        Eva: initialization:
+          \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add);
+    */
+    __gen_e_acsl_f_3(& __gen_e_acsl_f_6,
+                     (__e_acsl_mpz_struct *)__gen_e_acsl_add);
+    __gmpz_init(__gen_e_acsl_add_4);
+    __gmpz_add(__gen_e_acsl_add_4,
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl_f_6),
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_3));
+    __gmpz_init_set(__gen_e_acsl_if_2,
+                    (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
+    __gmpz_clear(__gen_e_acsl_n_3);
+    __gmpz_clear(__gen_e_acsl__5);
+    __gmpz_clear(__gen_e_acsl_add);
+    __gmpz_clear(__gen_e_acsl_f_6);
+    __gmpz_clear(__gen_e_acsl_add_4);
+  }
+  __gmpz_init_set(*__retres_arg,
+                  (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2));
+  __gmpz_clear(__gen_e_acsl_if_2);
+  return;
+}
+
+/*@ assigns *((__e_acsl_mpz_struct *)*__retres_arg);
+    assigns *((__e_acsl_mpz_struct *)*__retres_arg) \from *n, n;
+ */
+void __gen_e_acsl_f_3(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
+{
+  __e_acsl_mpz_t __gen_e_acsl__6;
+  int __gen_e_acsl_le;
+  int __gen_e_acsl_or_3;
+  __e_acsl_mpz_t __gen_e_acsl_if;
+  __gmpz_init_set_ui(__gen_e_acsl__6,(unsigned long)(2147483647U + 1U));
+  __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
+                               (__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
+  if (__gen_e_acsl_le <= 0) __gen_e_acsl_or_3 = 1;
+  else {
+    __e_acsl_mpz_t __gen_e_acsl__7;
+    int __gen_e_acsl_ge_3;
+    __gmpz_init_set_ui(__gen_e_acsl__7,9223372036854775807UL + 1UL);
+    __gen_e_acsl_ge_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
+                                   (__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
+    __gen_e_acsl_or_3 = __gen_e_acsl_ge_3 >= 0;
+    __gmpz_clear(__gen_e_acsl__7);
+  }
+  if (__gen_e_acsl_or_3) {
+    __e_acsl_mpz_t __gen_e_acsl__8;
+    __gmpz_init_set_si(__gen_e_acsl__8,0L);
+    __gmpz_init_set(__gen_e_acsl_if,
+                    (__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
+    __gmpz_clear(__gen_e_acsl__8);
+  }
+  else {
+    __e_acsl_mpz_t __gen_e_acsl__9;
+    __e_acsl_mpz_t __gen_e_acsl_add_2;
+    __e_acsl_mpz_t __gen_e_acsl_f_5;
+    __e_acsl_mpz_t __gen_e_acsl_add_3;
+    __gmpz_init_set_si(__gen_e_acsl__9,1L);
+    __gmpz_init(__gen_e_acsl_add_2);
+    __gmpz_add(__gen_e_acsl_add_2,(__e_acsl_mpz_struct const *)(n),
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
+    /*@ assert
+        Eva: initialization:
+          \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_2);
+    */
+    __gen_e_acsl_f_3(& __gen_e_acsl_f_5,
+                     (__e_acsl_mpz_struct *)__gen_e_acsl_add_2);
+    __gmpz_init(__gen_e_acsl_add_3);
+    __gmpz_add(__gen_e_acsl_add_3,
+               (__e_acsl_mpz_struct const *)(__gen_e_acsl_f_5),
+               (__e_acsl_mpz_struct const *)(n));
+    __gmpz_init_set(__gen_e_acsl_if,
+                    (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
+    __gmpz_clear(__gen_e_acsl__9);
+    __gmpz_clear(__gen_e_acsl_add_2);
+    __gmpz_clear(__gen_e_acsl_f_5);
+    __gmpz_clear(__gen_e_acsl_add_3);
+  }
+  __gmpz_init_set(*__retres_arg,
+                  (__e_acsl_mpz_struct const *)(__gen_e_acsl_if));
+  __gmpz_clear(__gen_e_acsl__6);
+  __gmpz_clear(__gen_e_acsl_if);
+  return;
+}
+
+

src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-177.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/bts/issue-eacsl-177.c:12: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/bts/issue-eacsl-177.c:12: Warning: 
+  assertion got status unknown.
+[eva:alarm] tests/bts/issue-eacsl-177.c:9: Warning: 
+  accessing uninitialized left-value.
+  assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add);
+[eva:alarm] tests/bts/issue-eacsl-177.c:9: Warning: 
+  accessing uninitialized left-value.
+  assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_2);
+[eva] tests/bts/issue-eacsl-177.c:9: Warning: 
+  Using specification of function __gen_e_acsl_f_3
+  for recursive calls of depth 100. Analysis of function __gen_e_acsl_f_3
+  is thus incomplete and its soundness relies on the written specification.
+[eva:alarm] tests/bts/issue-eacsl-177.c:14: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/bts/issue-eacsl-177.c:14: Warning: 
+  assertion got status unknown.