From f780d788a70732f73d218833954050147a48b58c Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@cea.fr>
Date: Tue, 17 Aug 2021 16:41:23 +0200
Subject: [PATCH] [e-acsl] add test for issue eacsl!177
---
.../e-acsl/tests/bts/issue-eacsl-177.c | 16 ++
.../tests/bts/oracle/gen_issue-eacsl-177.c | 229 ++++++++++++++++++
.../bts/oracle/issue-eacsl-177.res.oracle | 20 ++
.../oracle_dev/issue-eacsl-177.e-acsl.err.log | 0
4 files changed, 265 insertions(+)
create mode 100644 src/plugins/e-acsl/tests/bts/issue-eacsl-177.c
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-177.c
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-177.res.oracle
create mode 100644 src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-177.e-acsl.err.log
diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-177.c b/src/plugins/e-acsl/tests/bts/issue-eacsl-177.c
new file mode 100644
index 00000000000..affaf754bb9
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-177.c
@@ -0,0 +1,16 @@
+/* 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); */
+
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-177.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-177.c
new file mode 100644
index 00000000000..edd1eec97bb
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-177.c
@@ -0,0 +1,229 @@
+/* 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;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-177.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-177.res.oracle
new file mode 100644
index 00000000000..dd6d9ea6b9d
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-177.res.oracle
@@ -0,0 +1,20 @@
+[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.
diff --git a/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-177.e-acsl.err.log b/src/plugins/e-acsl/tests/bts/oracle_dev/issue-eacsl-177.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
--
GitLab