diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
new file mode 100644
index 0000000000000000000000000000000000000000..51dac6a97767622f11be304e0b7f9dd1ed7d37c1
--- /dev/null
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -0,0 +1,24 @@
+###############################################################################
+# Preliminary notes: #
+# ------------------ #
+# Mark "-": change with an impact for users (and possibly developers). #
+# Mark "o": change with an impact for developers only. #
+# Mark "+": change for Frama-C-commits audience (not in html version) #
+# Mark "*": bug fixed. #
+# Mark "!": change that can break compatibility with existing development. #
+# '#nnn' : BTS entry #nnn #
+# '#!nnn' : BTS private entry #nnn #
+# For compatibility with old change log formats: #
+# '#?nnn' : OLD-BTS entry #nnn #
+###############################################################################
+# Categories:
+# E-ACSL: the Whole E-ACSL plug-in
+###############################################################################
+
+###################################
+Plugin E-ACSL 0.1 Nitrogen_20111001
+###################################
+
+- E-ACSL [2012/01/06] First release for the Hi-Lite FUI9 project.
+
+###################################
diff --git a/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf b/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..447ccfb91c42bdd5a019a53ce0884f9888d8a5db
Binary files /dev/null and b/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf differ
diff --git a/src/plugins/e-acsl/doc/manuals/e-acsl.pdf b/src/plugins/e-acsl/doc/manuals/e-acsl.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..5e822451678b8dd6503341568926a3a87a91a384
Binary files /dev/null and b/src/plugins/e-acsl/doc/manuals/e-acsl.pdf differ
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/labeled_stmt.i b/src/plugins/e-acsl/tests/e-acsl-runtime/labeled_stmt.i
new file mode 100644
index 0000000000000000000000000000000000000000..eb72ec82c74102bb20ce4d9c88d9394e9dceb465
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/labeled_stmt.i
@@ -0,0 +1,16 @@
+/* run.config
+ COMMENT: labeled stmt and gotos
+ EXECNOW: LOG gen_labeled_stmt.c BIN gen_labeled_stmt.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/labeled_stmt.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_labeled_stmt.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_labeled_stmt.out ./tests/e-acsl-runtime/result/gen_labeled_stmt.c -lgmp && ./tests/e-acsl-runtime/result/gen_labeled_stmt.out
+*/
+
+int X = 0;
+
+/*@ ensures X == 3; */
+int main(void) {
+ goto L1;
+ L1: /*@ assert X == 0; */ X = 1;
+ goto L2;
+ L2: /*@ requires X == 1; ensures X == 2; */ X = 2;
+ if (X) { X = 3; return 0; }
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/linear_search.i b/src/plugins/e-acsl/tests/e-acsl-runtime/linear_search.i
new file mode 100644
index 0000000000000000000000000000000000000000..211224922611a18472237b12a5228eb4ac8052c9
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/linear_search.i
@@ -0,0 +1,36 @@
+/* run.config
+ COMMENT: linear search (example of the TAP'12 article)
+ EXECNOW: LOG gen_linear_search.c BIN gen_linear_search.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/linear_search.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_linear_search.c > /dev/null && gcc -pedantic -o ./tests/e-acsl-runtime/result/gen_linear_search.out ./tests/e-acsl-runtime/result/gen_linear_search.c -lgmp && ./tests/e-acsl-runtime/result/gen_linear_search.out
+*/
+
+int A[10];
+
+/*@ requires \forall integer i; 0 <= i < 9 ==> A[i] <= A[i+1];
+ behavior exists:
+ assumes \exists integer j; 0 <= j < 10 && A[j] == elt;
+ ensures \result == 1;
+ behavior not_exists:
+ assumes \forall integer j; 0 <= j < 10 ==> A[j] != elt;
+ ensures \result == 0; */
+int search(int elt){
+ int k;
+ // linear search in a sorted array
+ for(k = 0; k < 10; k++)
+ if(A[k] == elt) return 1; // element found
+ else if(A[k] > elt) return 0; // element not found (sorted array)
+ return 0; // element not found
+}
+
+int main(void) {
+
+ int found;
+ for(int i = 0; i < 10; i++) A[i] = i * i;
+
+ found = search(36);
+ /*@ assert found == 1; */
+
+ found = search(5);
+ /*@ assert found == 0; */
+
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
new file mode 100644
index 0000000000000000000000000000000000000000..7032d842cfa0c3ab90768989a074e1c878b89066
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
@@ -0,0 +1,116 @@
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct mpz_t[1];
+/*@ ensures \valid(\old(z));
+ assigns *z;
+ assigns *z \from n; */
+extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
+/*@ requires \valid(x);
+ assigns *x; */
+extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns \nothing; */
+extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2);
+/*@ terminates \false;
+ ensures \false;
+ assigns \nothing; */
+extern void exit(int status);
+/*@ assigns \nothing; */
+extern int printf(char const * , ...);
+void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
+{
+ if (predicate) {
+ printf("%s failed at line %d.\nThe failing predicate is:\n%s.\n",kind,
+ line,pred_txt);
+ exit(1);
+ }
+ return;
+}
+
+int X = 0;
+/*@ ensures X ≡ 3; */
+int main(void)
+{
+ int __retres;
+ goto L1;
+ L1:
+ /*@ assert X ≡ 0; */ ;
+ {
+ mpz_t e_acsl_1;
+ mpz_t e_acsl_2;
+ int e_acsl_3;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)X);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)0);
+ e_acsl_3 = __gmpz_cmp((__mpz_struct const *)(e_acsl_1),
+ (__mpz_struct const *)(e_acsl_2));
+ e_acsl_assert(! (e_acsl_3 == 0),(char *)"Assertion",(char *)"(X == 0)",
+ 11);
+ __gmpz_clear((__mpz_struct *)(e_acsl_1));
+ __gmpz_clear((__mpz_struct *)(e_acsl_2));
+ }
+
+ X = 1;
+ goto L2;
+ L2:
+ /*@ requires X ≡ 1;
+ ensures X ≡ 2; */
+ {
+ mpz_t e_acsl_7;
+ mpz_t e_acsl_8;
+ int e_acsl_9;
+ {
+ mpz_t e_acsl_4;
+ mpz_t e_acsl_5;
+ int e_acsl_6;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_4),(long)X);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_5),(long)1);
+ e_acsl_6 = __gmpz_cmp((__mpz_struct const *)(e_acsl_4),
+ (__mpz_struct const *)(e_acsl_5));
+ e_acsl_assert(! (e_acsl_6 == 0),(char *)"Precondition",
+ (char *)"(X == 1)",13);
+ __gmpz_clear((__mpz_struct *)(e_acsl_4));
+ __gmpz_clear((__mpz_struct *)(e_acsl_5));
+ X = 2;
+ }
+
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_7),(long)X);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_8),(long)2);
+ e_acsl_9 = __gmpz_cmp((__mpz_struct const *)(e_acsl_7),
+ (__mpz_struct const *)(e_acsl_8));
+ e_acsl_assert(! (e_acsl_9 == 0),(char *)"Postcondition",
+ (char *)"(X == 2)",13);
+ __gmpz_clear((__mpz_struct *)(e_acsl_7));
+ __gmpz_clear((__mpz_struct *)(e_acsl_8));
+ }
+
+ if (X) {
+ X = 3;
+ __retres = 0;
+ goto return_label; }
+ __retres = 0;
+ return_label:
+ {
+ mpz_t e_acsl_10;
+ mpz_t e_acsl_11;
+ int e_acsl_12;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_10),(long)X);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_11),(long)3);
+ e_acsl_12 = __gmpz_cmp((__mpz_struct const *)(e_acsl_10),
+ (__mpz_struct const *)(e_acsl_11));
+ e_acsl_assert(! (e_acsl_12 == 0),(char *)"Postcondition",
+ (char *)"(X == 3)",8);
+ __gmpz_clear((__mpz_struct *)(e_acsl_10));
+ __gmpz_clear((__mpz_struct *)(e_acsl_11));
+ return (__retres);
+ }
+
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
new file mode 100644
index 0000000000000000000000000000000000000000..e467aa549cd3fb469ba37f766cd36ca1f156ac43
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
@@ -0,0 +1,346 @@
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct mpz_t[1];
+/*@ ensures \valid(\old(x));
+ assigns *x; */
+extern void __gmpz_init(__mpz_struct * /*[1]*/ x);
+/*@ ensures \valid(\old(z));
+ assigns *z;
+ assigns *z \from n; */
+extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
+/*@ requires \valid(z_orig);
+ requires \valid(z);
+ assigns *z; */
+extern void __gmpz_set(__mpz_struct * /*[1]*/ z,
+ __mpz_struct const * /*[1]*/ z_orig);
+/*@ requires \valid(x);
+ assigns *x; */
+extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns \nothing; */
+extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ requires \valid(z3);
+ assigns *z1;
+*/
+extern void __gmpz_add(__mpz_struct * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2,
+ __mpz_struct const * /*[1]*/ z3);
+/*@ requires \valid(z);
+ assigns \nothing; */
+extern long __gmpz_get_si(__mpz_struct const * /*[1]*/ z);
+/*@ terminates \false;
+ ensures \false;
+ assigns \nothing; */
+extern void exit(int status);
+/*@ assigns \nothing; */
+extern int printf(char const * , ...);
+void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
+{
+ if (predicate) {
+ printf("%s failed at line %d.\nThe failing predicate is:\n%s.\n",kind,
+ line,pred_txt);
+ exit(1);
+ }
+ return;
+}
+
+int A[10];
+/*@ requires ∀ ℤ i; 0 ≤ i ∧ i < 9 ⇒ A[i] ≤ A[i+1];
+ behavior exists:
+ assumes ∃ ℤ j; (0 ≤ j ∧ j < 10) ∧ A[j] ≡ elt;
+ ensures \result ≡ 1;
+
+ behavior not_exists:
+ assumes ∀ ℤ j; 0 ≤ j ∧ j < 10 ⇒ A[j] ≢ elt;
+ ensures \result ≡ 0;
+
+
+*/
+int search(int elt)
+{
+ int __retres;
+ int k;
+ int e_acsl_20;
+ int e_acsl_33;
+ {
+ mpz_t e_acsl_1;
+ int e_acsl_2;
+ e_acsl_2 = 1;
+ __gmpz_init((__mpz_struct *)(e_acsl_1));
+ {
+ mpz_t e_acsl_7;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_7),(long)0);
+ __gmpz_set((__mpz_struct *)(e_acsl_1),(__mpz_struct const *)(e_acsl_7));
+ __gmpz_clear((__mpz_struct *)(e_acsl_7));
+ }
+
+ while (1) {
+ {
+ mpz_t e_acsl_8;
+ int e_acsl_9;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_8),(long)9);
+ e_acsl_9 = __gmpz_cmp((__mpz_struct const *)(e_acsl_1),
+ (__mpz_struct const *)(e_acsl_8));
+ if (! (e_acsl_9 < 0)) { break; }
+ __gmpz_clear((__mpz_struct *)(e_acsl_8));
+ }
+
+ {
+ int e_acsl_3;
+ mpz_t e_acsl_4;
+ mpz_t e_acsl_5;
+ int e_acsl_6;
+ e_acsl_3 = (int)__gmpz_get_si((__mpz_struct const *)(e_acsl_1));
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_4),(long)1);
+ __gmpz_init((__mpz_struct *)(e_acsl_5));
+ __gmpz_add((__mpz_struct *)(e_acsl_5),
+ (__mpz_struct const *)(e_acsl_1),
+ (__mpz_struct const *)(e_acsl_4));
+ e_acsl_6 = (int)__gmpz_get_si((__mpz_struct const *)(e_acsl_5));
+ __gmpz_clear((__mpz_struct *)(e_acsl_4));
+ __gmpz_clear((__mpz_struct *)(e_acsl_5));
+ if (! (A[e_acsl_3] <= A[e_acsl_6])) {
+ e_acsl_2 = 0;
+ goto e_acsl_end_loop1;
+ }
+ }
+
+ {
+ mpz_t e_acsl_10;
+ mpz_t e_acsl_11;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_10),(long)((char)1));
+ __gmpz_init((__mpz_struct *)(e_acsl_11));
+ __gmpz_add((__mpz_struct *)(e_acsl_11),
+ (__mpz_struct const *)(e_acsl_1),
+ (__mpz_struct const *)(e_acsl_10));
+ __gmpz_set((__mpz_struct *)(e_acsl_1),
+ (__mpz_struct const *)(e_acsl_11));
+ __gmpz_clear((__mpz_struct *)(e_acsl_10));
+ __gmpz_clear((__mpz_struct *)(e_acsl_11));
+ }
+
+ }
+ e_acsl_end_loop1: ;
+ e_acsl_assert(! e_acsl_2,(char *)"Precondition",
+ (char *)"(\\forall integer i; 0 <= i && i < 9 ==> A[i] <= A[i+1])",
+ 8);
+ __gmpz_clear((__mpz_struct *)(e_acsl_1));
+ {
+ mpz_t e_acsl_25;
+ int e_acsl_26;
+ e_acsl_26 = 1;
+ __gmpz_init((__mpz_struct *)(e_acsl_25));
+ {
+ mpz_t e_acsl_28;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_28),(long)0);
+ __gmpz_set((__mpz_struct *)(e_acsl_25),
+ (__mpz_struct const *)(e_acsl_28));
+ __gmpz_clear((__mpz_struct *)(e_acsl_28));
+ }
+
+ while (1) {
+ {
+ mpz_t e_acsl_29;
+ int e_acsl_30;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_29),(long)10);
+ e_acsl_30 = __gmpz_cmp((__mpz_struct const *)(e_acsl_25),
+ (__mpz_struct const *)(e_acsl_29));
+ if (! (e_acsl_30 < 0)) { break; }
+ __gmpz_clear((__mpz_struct *)(e_acsl_29));
+ }
+
+ {
+ int e_acsl_27;
+ e_acsl_27 = (int)__gmpz_get_si((__mpz_struct const *)(e_acsl_25));
+ if (! (A[e_acsl_27] != elt)) {
+ e_acsl_26 = 0;
+ goto e_acsl_end_loop3;
+ }
+ }
+
+ {
+ mpz_t e_acsl_31;
+ mpz_t e_acsl_32;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_31),(long)((char)1));
+ __gmpz_init((__mpz_struct *)(e_acsl_32));
+ __gmpz_add((__mpz_struct *)(e_acsl_32),
+ (__mpz_struct const *)(e_acsl_25),
+ (__mpz_struct const *)(e_acsl_31));
+ __gmpz_set((__mpz_struct *)(e_acsl_25),
+ (__mpz_struct const *)(e_acsl_32));
+ __gmpz_clear((__mpz_struct *)(e_acsl_31));
+ __gmpz_clear((__mpz_struct *)(e_acsl_32));
+ }
+
+ }
+ e_acsl_end_loop3: ;
+ e_acsl_33 = e_acsl_26;
+ __gmpz_clear((__mpz_struct *)(e_acsl_25));
+ }
+
+ {
+ mpz_t e_acsl_12;
+ int e_acsl_13;
+ e_acsl_13 = 0;
+ __gmpz_init((__mpz_struct *)(e_acsl_12));
+ {
+ mpz_t e_acsl_15;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_15),(long)0);
+ __gmpz_set((__mpz_struct *)(e_acsl_12),
+ (__mpz_struct const *)(e_acsl_15));
+ __gmpz_clear((__mpz_struct *)(e_acsl_15));
+ }
+
+ while (1) {
+ {
+ mpz_t e_acsl_16;
+ int e_acsl_17;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_16),(long)10);
+ e_acsl_17 = __gmpz_cmp((__mpz_struct const *)(e_acsl_12),
+ (__mpz_struct const *)(e_acsl_16));
+ if (! (e_acsl_17 < 0)) { break; }
+ __gmpz_clear((__mpz_struct *)(e_acsl_16));
+ }
+
+ {
+ int e_acsl_14;
+ e_acsl_14 = (int)__gmpz_get_si((__mpz_struct const *)(e_acsl_12));
+ if (! (! (A[e_acsl_14] == elt))) {
+ e_acsl_13 = 1;
+ goto e_acsl_end_loop2;
+ }
+ }
+
+ {
+ mpz_t e_acsl_18;
+ mpz_t e_acsl_19;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_18),(long)((char)1));
+ __gmpz_init((__mpz_struct *)(e_acsl_19));
+ __gmpz_add((__mpz_struct *)(e_acsl_19),
+ (__mpz_struct const *)(e_acsl_12),
+ (__mpz_struct const *)(e_acsl_18));
+ __gmpz_set((__mpz_struct *)(e_acsl_12),
+ (__mpz_struct const *)(e_acsl_19));
+ __gmpz_clear((__mpz_struct *)(e_acsl_18));
+ __gmpz_clear((__mpz_struct *)(e_acsl_19));
+ }
+
+ }
+ e_acsl_end_loop2: ;
+ e_acsl_20 = e_acsl_13;
+ __gmpz_clear((__mpz_struct *)(e_acsl_12));
+ }
+
+ k = 0;
+ }
+
+ while (1) {
+ if (! (k < 10)) { break; }
+ if (A[k] == elt) {
+ __retres = 1;
+ goto return_label; }
+ else {
+ if (A[k] > elt) {
+ __retres = 0;
+ goto return_label; } }
+ k ++;
+ }
+ __retres = 0;
+ return_label:
+ {
+ int e_acsl_24;
+ int e_acsl_37;
+ if (! e_acsl_20) { e_acsl_24 = 1; }
+ else {
+ mpz_t e_acsl_21;
+ mpz_t e_acsl_22;
+ int e_acsl_23;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_21),(long)__retres);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_22),(long)1);
+ e_acsl_23 = __gmpz_cmp((__mpz_struct const *)(e_acsl_21),
+ (__mpz_struct const *)(e_acsl_22));
+ e_acsl_24 = e_acsl_23 == 0;
+ __gmpz_clear((__mpz_struct *)(e_acsl_21));
+ __gmpz_clear((__mpz_struct *)(e_acsl_22));
+ }
+ e_acsl_assert(! e_acsl_24,(char *)"Postcondition",
+ (char *)"(\\old(\\exists integer j; (0 <= j && j < 10) && A[j] == elt) ==> \\result == 1)",
+ 11);
+ if (! e_acsl_33) { e_acsl_37 = 1; }
+ else {
+ mpz_t e_acsl_34;
+ mpz_t e_acsl_35;
+ int e_acsl_36;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_34),(long)__retres);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_35),(long)0);
+ e_acsl_36 = __gmpz_cmp((__mpz_struct const *)(e_acsl_34),
+ (__mpz_struct const *)(e_acsl_35));
+ e_acsl_37 = e_acsl_36 == 0;
+ __gmpz_clear((__mpz_struct *)(e_acsl_34));
+ __gmpz_clear((__mpz_struct *)(e_acsl_35));
+ }
+ e_acsl_assert(! e_acsl_37,(char *)"Postcondition",
+ (char *)"(\\old(\\forall integer j; 0 <= j && j < 10 ==> A[j] != elt) ==> \\result == 0)",
+ 14);
+ return (__retres);
+ }
+
+}
+
+int main(void)
+{
+ int __retres;
+ int found;
+ { int i;
+ i = 0;
+ while (1) {
+ if (! (i < 10)) { break; }
+ A[i] = i * i;
+ i ++; } }
+
+ found = search(36);
+ /*@ assert found ≡ 1; */ ;
+ {
+ mpz_t e_acsl_1;
+ mpz_t e_acsl_2;
+ int e_acsl_3;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)found);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)1);
+ e_acsl_3 = __gmpz_cmp((__mpz_struct const *)(e_acsl_1),
+ (__mpz_struct const *)(e_acsl_2));
+ e_acsl_assert(! (e_acsl_3 == 0),(char *)"Assertion",
+ (char *)"(found == 1)",30);
+ __gmpz_clear((__mpz_struct *)(e_acsl_1));
+ __gmpz_clear((__mpz_struct *)(e_acsl_2));
+ }
+
+ found = search(5);
+ /*@ assert found ≡ 0; */ ;
+ {
+ mpz_t e_acsl_4;
+ mpz_t e_acsl_5;
+ int e_acsl_6;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_4),(long)found);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_5),(long)0);
+ e_acsl_6 = __gmpz_cmp((__mpz_struct const *)(e_acsl_4),
+ (__mpz_struct const *)(e_acsl_5));
+ e_acsl_assert(! (e_acsl_6 == 0),(char *)"Assertion",
+ (char *)"(found == 0)",33);
+ __gmpz_clear((__mpz_struct *)(e_acsl_4));
+ __gmpz_clear((__mpz_struct *)(e_acsl_5));
+ }
+
+ __retres = 0;
+ return (__retres);
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..14c65ead652f0edf145aa28470e92d13ebe2ee49
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle
@@ -0,0 +1,235 @@
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ X ∈ {0}
+PROJECT_FILE.i:232:[value] Assertion got status valid.
+[value] computing for function __gmpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:237.
+PROJECT_FILE.i:82:[value] Function __gmpz_init_set_si: postcondition got status valid.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:238.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_cmp <- main.
+ Called from PROJECT_FILE.i:239.
+PROJECT_FILE.i:119:[value] Function __gmpz_cmp: precondition got status valid.
+PROJECT_FILE.i:120:[value] Function __gmpz_cmp: precondition got status valid.
+[value] Done for function __gmpz_cmp
+[value] computing for function e_acsl_assert <- main.
+ Called from PROJECT_FILE.i:240.
+[value] computing for function printf <- e_acsl_assert <- main.
+ Called from PROJECT_FILE.i:219.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_assert <- main.
+ Called from PROJECT_FILE.i:221.
+PROJECT_FILE.i:207:[value] Function exit: postcondition got status invalid.
+[value] Done for function exit
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+[value] computing for function __gmpz_clear <- main.
+ Called from PROJECT_FILE.i:241.
+PROJECT_FILE.i:111:[value] Function __gmpz_clear: precondition got status valid.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- main.
+ Called from PROJECT_FILE.i:242.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:259.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:260.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_cmp <- main.
+ Called from PROJECT_FILE.i:261.
+[value] Done for function __gmpz_cmp
+[value] computing for function e_acsl_assert <- main.
+ Called from PROJECT_FILE.i:262.
+[value] computing for function printf <- e_acsl_assert <- main.
+ Called from PROJECT_FILE.i:219.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_assert <- main.
+ Called from PROJECT_FILE.i:221.
+[value] Done for function exit
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+[value] computing for function __gmpz_clear <- main.
+ Called from PROJECT_FILE.i:263.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- main.
+ Called from PROJECT_FILE.i:264.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:268.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:269.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_cmp <- main.
+ Called from PROJECT_FILE.i:270.
+[value] Done for function __gmpz_cmp
+[value] computing for function e_acsl_assert <- main.
+ Called from PROJECT_FILE.i:271.
+[value] computing for function printf <- e_acsl_assert <- main.
+ Called from PROJECT_FILE.i:219.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_assert <- main.
+ Called from PROJECT_FILE.i:221.
+[value] Done for function exit
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+[value] computing for function __gmpz_clear <- main.
+ Called from PROJECT_FILE.i:272.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- main.
+ Called from PROJECT_FILE.i:273.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:286.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:287.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_cmp <- main.
+ Called from PROJECT_FILE.i:288.
+[value] Done for function __gmpz_cmp
+[value] computing for function e_acsl_assert <- main.
+ Called from PROJECT_FILE.i:289.
+[value] computing for function printf <- e_acsl_assert <- main.
+ Called from PROJECT_FILE.i:219.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_assert <- main.
+ Called from PROJECT_FILE.i:221.
+[value] Done for function exit
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+[value] computing for function __gmpz_clear <- main.
+ Called from PROJECT_FILE.i:290.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- main.
+ Called from PROJECT_FILE.i:291.
+[value] Done for function __gmpz_clear
+PROJECT_FILE.i:226:[value] Function main: postcondition got status valid.
+[value] Recording results for main
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values at end of function e_acsl_assert:
+[value] Values at end of function main:
+ X ∈ {3}
+ __retres ∈ {0}
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct mpz_t[1];
+/*@ ensures \valid(\old(z));
+ assigns *z;
+ assigns *z \from n; */
+extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
+/*@ requires \valid(x);
+ assigns *x; */
+extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns \nothing; */
+extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2);
+/*@ terminates \false;
+ ensures \false;
+ assigns \nothing; */
+extern void exit(int status);
+/*@ assigns \nothing; */
+extern int printf(char const * , ...);
+void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
+{
+ if (predicate) {
+ printf("%s failed at line %d.\nThe failing predicate is:\n%s.\n",kind,
+ line,pred_txt);
+ exit(1);
+ }
+ return;
+}
+
+int X = 0;
+/*@ ensures X ≡ 3; */
+int main(void)
+{
+ int __retres;
+ goto L1;
+ L1:
+ /*@ assert X ≡ 0; */ ;
+ {
+ mpz_t e_acsl_1;
+ mpz_t e_acsl_2;
+ int e_acsl_3;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)X);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)0);
+ e_acsl_3 = __gmpz_cmp((__mpz_struct const *)(e_acsl_1),
+ (__mpz_struct const *)(e_acsl_2));
+ e_acsl_assert(! (e_acsl_3 == 0),(char *)"Assertion",(char *)"(X == 0)",
+ 11);
+ __gmpz_clear((__mpz_struct *)(e_acsl_1));
+ __gmpz_clear((__mpz_struct *)(e_acsl_2));
+ }
+
+ X = 1;
+ goto L2;
+ L2:
+ /*@ requires X ≡ 1;
+ ensures X ≡ 2; */
+ {
+ mpz_t e_acsl_7;
+ mpz_t e_acsl_8;
+ int e_acsl_9;
+ {
+ mpz_t e_acsl_4;
+ mpz_t e_acsl_5;
+ int e_acsl_6;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_4),(long)X);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_5),(long)1);
+ e_acsl_6 = __gmpz_cmp((__mpz_struct const *)(e_acsl_4),
+ (__mpz_struct const *)(e_acsl_5));
+ e_acsl_assert(! (e_acsl_6 == 0),(char *)"Precondition",
+ (char *)"(X == 1)",13);
+ __gmpz_clear((__mpz_struct *)(e_acsl_4));
+ __gmpz_clear((__mpz_struct *)(e_acsl_5));
+ X = 2;
+ }
+
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_7),(long)X);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_8),(long)2);
+ e_acsl_9 = __gmpz_cmp((__mpz_struct const *)(e_acsl_7),
+ (__mpz_struct const *)(e_acsl_8));
+ e_acsl_assert(! (e_acsl_9 == 0),(char *)"Postcondition",
+ (char *)"(X == 2)",13);
+ __gmpz_clear((__mpz_struct *)(e_acsl_7));
+ __gmpz_clear((__mpz_struct *)(e_acsl_8));
+ }
+
+ if (X) {
+ X = 3;
+ __retres = 0;
+ goto return_label; }
+ __retres = 0;
+ return_label:
+ {
+ mpz_t e_acsl_10;
+ mpz_t e_acsl_11;
+ int e_acsl_12;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_10),(long)X);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_11),(long)3);
+ e_acsl_12 = __gmpz_cmp((__mpz_struct const *)(e_acsl_10),
+ (__mpz_struct const *)(e_acsl_11));
+ e_acsl_assert(! (e_acsl_12 == 0),(char *)"Postcondition",
+ (char *)"(X == 3)",8);
+ __gmpz_clear((__mpz_struct *)(e_acsl_10));
+ __gmpz_clear((__mpz_struct *)(e_acsl_11));
+ return (__retres);
+ }
+
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c91f6fcda29240328ff5af707d9577b5257877c9
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
@@ -0,0 +1,903 @@
+tests/e-acsl-runtime/linear_search.i:8:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
+:0:[e-acsl] warning: missing guard for ensuring that i is a valid array index
+tests/e-acsl-runtime/linear_search.i:8:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
+:0:[e-acsl] warning: missing guard for ensuring that i+1 is a valid array index
+tests/e-acsl-runtime/linear_search.i:10:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
+:0:[e-acsl] warning: missing guard for ensuring that j is a valid array index
+tests/e-acsl-runtime/linear_search.i:13:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ A[0..9] ∈ {0}
+PROJECT_FILE.i:457:[value] entering loop for the first time
+PROJECT_FILE.i:460:[value] assigning non deterministic value for the first time
+[value] computing for function search <- main.
+ Called from PROJECT_FILE.i:463.
+PROJECT_FILE.i:226:[value] Function search: precondition got status unknown.
+[value] computing for function __gmpz_init <- search <- main.
+ Called from PROJECT_FILE.i:247.
+PROJECT_FILE.i:69:[value] Function __gmpz_init: postcondition got status valid.
+[value] Done for function __gmpz_init
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:250.
+PROJECT_FILE.i:82:[value] Function __gmpz_init_set_si: postcondition got status valid.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_set <- search <- main.
+ Called from PROJECT_FILE.i:251.
+PROJECT_FILE.i:94:[value] Function __gmpz_set: precondition got status valid.
+PROJECT_FILE.i:95:[value] Function __gmpz_set: precondition got status valid.
+[value] Done for function __gmpz_set
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:252.
+PROJECT_FILE.i:111:[value] Function __gmpz_clear: precondition got status valid.
+[value] Done for function __gmpz_clear
+PROJECT_FILE.i:255:[value] entering loop for the first time
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:259.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_cmp <- search <- main.
+ Called from PROJECT_FILE.i:260.
+PROJECT_FILE.i:119:[value] Function __gmpz_cmp: precondition got status valid.
+PROJECT_FILE.i:120:[value] Function __gmpz_cmp: precondition got status valid.
+[value] Done for function __gmpz_cmp
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:262.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_get_si <- search <- main.
+ Called from PROJECT_FILE.i:270.
+PROJECT_FILE.i:172:[value] Function __gmpz_get_si: precondition got status valid.
+[value] Done for function __gmpz_get_si
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:271.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init <- search <- main.
+ Called from PROJECT_FILE.i:272.
+[value] Done for function __gmpz_init
+[value] computing for function __gmpz_add <- search <- main.
+ Called from PROJECT_FILE.i:273.
+PROJECT_FILE.i:138:[value] Function __gmpz_add: precondition got status valid.
+PROJECT_FILE.i:139:[value] Function __gmpz_add: precondition got status valid.
+PROJECT_FILE.i:140:[value] Function __gmpz_add: precondition got status valid.
+[value] Done for function __gmpz_add
+[value] computing for function __gmpz_get_si <- search <- main.
+ Called from PROJECT_FILE.i:274.
+[value] Done for function __gmpz_get_si
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:275.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:276.
+[value] Done for function __gmpz_clear
+PROJECT_FILE.i:277:[kernel] warning: accessing out of bounds index [-2147483648..2147483647].
+ assert 0 ≤ e_acsl_3 ∧ e_acsl_3 < 10;
+PROJECT_FILE.i:277:[kernel] warning: accessing out of bounds index [-2147483648..2147483647].
+ assert 0 ≤ e_acsl_6 ∧ e_acsl_6 < 10;
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:286.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init <- search <- main.
+ Called from PROJECT_FILE.i:287.
+[value] Done for function __gmpz_init
+[value] computing for function __gmpz_add <- search <- main.
+ Called from PROJECT_FILE.i:288.
+[value] Done for function __gmpz_add
+[value] computing for function __gmpz_set <- search <- main.
+ Called from PROJECT_FILE.i:289.
+[value] Done for function __gmpz_set
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:290.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:291.
+[value] Done for function __gmpz_clear
+[value] computing for function e_acsl_assert <- search <- main.
+ Called from PROJECT_FILE.i:296.
+[value] computing for function printf <- e_acsl_assert <- search <- main.
+ Called from PROJECT_FILE.i:219.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_assert <- search <- main.
+ Called from PROJECT_FILE.i:221.
+PROJECT_FILE.i:207:[value] Function exit: postcondition got status invalid.
+[value] Done for function exit
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:299.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_init <- search <- main.
+ Called from PROJECT_FILE.i:304.
+[value] Done for function __gmpz_init
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:307.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_set <- search <- main.
+ Called from PROJECT_FILE.i:308.
+[value] Done for function __gmpz_set
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:309.
+[value] Done for function __gmpz_clear
+PROJECT_FILE.i:312:[value] entering loop for the first time
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:316.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_cmp <- search <- main.
+ Called from PROJECT_FILE.i:317.
+[value] Done for function __gmpz_cmp
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:319.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_get_si <- search <- main.
+ Called from PROJECT_FILE.i:324.
+[value] Done for function __gmpz_get_si
+PROJECT_FILE.i:325:[kernel] warning: accessing out of bounds index [-2147483648..2147483647].
+ assert 0 ≤ e_acsl_27 ∧ e_acsl_27 < 10;
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:334.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init <- search <- main.
+ Called from PROJECT_FILE.i:335.
+[value] Done for function __gmpz_init
+[value] computing for function __gmpz_add <- search <- main.
+ Called from PROJECT_FILE.i:336.
+[value] Done for function __gmpz_add
+[value] computing for function __gmpz_set <- search <- main.
+ Called from PROJECT_FILE.i:337.
+[value] Done for function __gmpz_set
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:338.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:339.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:345.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_init <- search <- main.
+ Called from PROJECT_FILE.i:352.
+[value] Done for function __gmpz_init
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:355.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_set <- search <- main.
+ Called from PROJECT_FILE.i:356.
+[value] Done for function __gmpz_set
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:357.
+[value] Done for function __gmpz_clear
+PROJECT_FILE.i:360:[value] entering loop for the first time
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:364.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_cmp <- search <- main.
+ Called from PROJECT_FILE.i:365.
+[value] Done for function __gmpz_cmp
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:367.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_get_si <- search <- main.
+ Called from PROJECT_FILE.i:372.
+[value] Done for function __gmpz_get_si
+PROJECT_FILE.i:373:[kernel] warning: accessing out of bounds index [-2147483648..2147483647].
+ assert 0 ≤ e_acsl_14 ∧ e_acsl_14 < 10;
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:382.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init <- search <- main.
+ Called from PROJECT_FILE.i:383.
+[value] Done for function __gmpz_init
+[value] computing for function __gmpz_add <- search <- main.
+ Called from PROJECT_FILE.i:384.
+[value] Done for function __gmpz_add
+[value] computing for function __gmpz_set <- search <- main.
+ Called from PROJECT_FILE.i:385.
+[value] Done for function __gmpz_set
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:386.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:387.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:393.
+[value] Done for function __gmpz_clear
+PROJECT_FILE.i:399:[value] entering loop for the first time
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:421.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:422.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_cmp <- search <- main.
+ Called from PROJECT_FILE.i:423.
+[value] Done for function __gmpz_cmp
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:425.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:426.
+[value] Done for function __gmpz_clear
+[value] computing for function e_acsl_assert <- search <- main.
+ Called from PROJECT_FILE.i:428.
+[value] computing for function printf <- e_acsl_assert <- search <- main.
+ Called from PROJECT_FILE.i:219.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_assert <- search <- main.
+ Called from PROJECT_FILE.i:221.
+[value] Done for function exit
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:436.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:437.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_cmp <- search <- main.
+ Called from PROJECT_FILE.i:438.
+[value] Done for function __gmpz_cmp
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:440.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:441.
+[value] Done for function __gmpz_clear
+[value] computing for function e_acsl_assert <- search <- main.
+ Called from PROJECT_FILE.i:443.
+[value] computing for function printf <- e_acsl_assert <- search <- main.
+ Called from PROJECT_FILE.i:219.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_assert <- search <- main.
+ Called from PROJECT_FILE.i:221.
+[value] Done for function exit
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+PROJECT_FILE.i:229:[value] Function search, behavior exists: postcondition got status unknown.
+PROJECT_FILE.i:229:[value] Function search, behavior exists: postcondition got status unknown, but it is unknown if the behavior is active.
+PROJECT_FILE.i:233:[value] Function search, behavior not_exists: postcondition got status unknown.
+PROJECT_FILE.i:233:[value] Function search, behavior not_exists: postcondition got status unknown, but it is unknown if the behavior is active.
+[value] Recording results for search
+[value] Done for function search
+PROJECT_FILE.i:464:[value] Assertion got status unknown.
+[value] computing for function __gmpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:469.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:470.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_cmp <- main.
+ Called from PROJECT_FILE.i:471.
+[value] Done for function __gmpz_cmp
+[value] computing for function e_acsl_assert <- main.
+ Called from PROJECT_FILE.i:472.
+[value] computing for function printf <- e_acsl_assert <- main.
+ Called from PROJECT_FILE.i:219.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_assert <- main.
+ Called from PROJECT_FILE.i:221.
+[value] Done for function exit
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+[value] computing for function __gmpz_clear <- main.
+ Called from PROJECT_FILE.i:473.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- main.
+ Called from PROJECT_FILE.i:474.
+[value] Done for function __gmpz_clear
+[value] computing for function search <- main.
+ Called from PROJECT_FILE.i:478.
+[value] computing for function __gmpz_init <- search <- main.
+ Called from PROJECT_FILE.i:247.
+[value] Done for function __gmpz_init
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:250.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_set <- search <- main.
+ Called from PROJECT_FILE.i:251.
+[value] Done for function __gmpz_set
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:252.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:259.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_cmp <- search <- main.
+ Called from PROJECT_FILE.i:260.
+[value] Done for function __gmpz_cmp
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:262.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_get_si <- search <- main.
+ Called from PROJECT_FILE.i:270.
+[value] Done for function __gmpz_get_si
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:271.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init <- search <- main.
+ Called from PROJECT_FILE.i:272.
+[value] Done for function __gmpz_init
+[value] computing for function __gmpz_add <- search <- main.
+ Called from PROJECT_FILE.i:273.
+[value] Done for function __gmpz_add
+[value] computing for function __gmpz_get_si <- search <- main.
+ Called from PROJECT_FILE.i:274.
+[value] Done for function __gmpz_get_si
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:275.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:276.
+[value] Done for function __gmpz_clear
+PROJECT_FILE.i:277:[value] Assertion got status unknown.
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:286.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init <- search <- main.
+ Called from PROJECT_FILE.i:287.
+[value] Done for function __gmpz_init
+[value] computing for function __gmpz_add <- search <- main.
+ Called from PROJECT_FILE.i:288.
+[value] Done for function __gmpz_add
+[value] computing for function __gmpz_set <- search <- main.
+ Called from PROJECT_FILE.i:289.
+[value] Done for function __gmpz_set
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:290.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:291.
+[value] Done for function __gmpz_clear
+[value] computing for function e_acsl_assert <- search <- main.
+ Called from PROJECT_FILE.i:296.
+[value] computing for function printf <- e_acsl_assert <- search <- main.
+ Called from PROJECT_FILE.i:219.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_assert <- search <- main.
+ Called from PROJECT_FILE.i:221.
+[value] Done for function exit
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:299.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_init <- search <- main.
+ Called from PROJECT_FILE.i:304.
+[value] Done for function __gmpz_init
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:307.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_set <- search <- main.
+ Called from PROJECT_FILE.i:308.
+[value] Done for function __gmpz_set
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:309.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:316.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_cmp <- search <- main.
+ Called from PROJECT_FILE.i:317.
+[value] Done for function __gmpz_cmp
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:319.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_get_si <- search <- main.
+ Called from PROJECT_FILE.i:324.
+[value] Done for function __gmpz_get_si
+PROJECT_FILE.i:325:[value] Assertion got status unknown.
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:334.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init <- search <- main.
+ Called from PROJECT_FILE.i:335.
+[value] Done for function __gmpz_init
+[value] computing for function __gmpz_add <- search <- main.
+ Called from PROJECT_FILE.i:336.
+[value] Done for function __gmpz_add
+[value] computing for function __gmpz_set <- search <- main.
+ Called from PROJECT_FILE.i:337.
+[value] Done for function __gmpz_set
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:338.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:339.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:345.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_init <- search <- main.
+ Called from PROJECT_FILE.i:352.
+[value] Done for function __gmpz_init
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:355.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_set <- search <- main.
+ Called from PROJECT_FILE.i:356.
+[value] Done for function __gmpz_set
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:357.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:364.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_cmp <- search <- main.
+ Called from PROJECT_FILE.i:365.
+[value] Done for function __gmpz_cmp
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:367.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_get_si <- search <- main.
+ Called from PROJECT_FILE.i:372.
+[value] Done for function __gmpz_get_si
+PROJECT_FILE.i:373:[value] Assertion got status unknown.
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:382.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init <- search <- main.
+ Called from PROJECT_FILE.i:383.
+[value] Done for function __gmpz_init
+[value] computing for function __gmpz_add <- search <- main.
+ Called from PROJECT_FILE.i:384.
+[value] Done for function __gmpz_add
+[value] computing for function __gmpz_set <- search <- main.
+ Called from PROJECT_FILE.i:385.
+[value] Done for function __gmpz_set
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:386.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:387.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:393.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:421.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:422.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_cmp <- search <- main.
+ Called from PROJECT_FILE.i:423.
+[value] Done for function __gmpz_cmp
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:425.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:426.
+[value] Done for function __gmpz_clear
+[value] computing for function e_acsl_assert <- search <- main.
+ Called from PROJECT_FILE.i:428.
+[value] computing for function printf <- e_acsl_assert <- search <- main.
+ Called from PROJECT_FILE.i:219.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_assert <- search <- main.
+ Called from PROJECT_FILE.i:221.
+[value] Done for function exit
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:436.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init_set_si <- search <- main.
+ Called from PROJECT_FILE.i:437.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_cmp <- search <- main.
+ Called from PROJECT_FILE.i:438.
+[value] Done for function __gmpz_cmp
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:440.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- search <- main.
+ Called from PROJECT_FILE.i:441.
+[value] Done for function __gmpz_clear
+[value] computing for function e_acsl_assert <- search <- main.
+ Called from PROJECT_FILE.i:443.
+[value] computing for function printf <- e_acsl_assert <- search <- main.
+ Called from PROJECT_FILE.i:219.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_assert <- search <- main.
+ Called from PROJECT_FILE.i:221.
+[value] Done for function exit
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+[value] Recording results for search
+[value] Done for function search
+PROJECT_FILE.i:479:[value] Assertion got status unknown.
+[value] computing for function __gmpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:484.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_init_set_si <- main.
+ Called from PROJECT_FILE.i:485.
+[value] Done for function __gmpz_init_set_si
+[value] computing for function __gmpz_cmp <- main.
+ Called from PROJECT_FILE.i:486.
+[value] Done for function __gmpz_cmp
+[value] computing for function e_acsl_assert <- main.
+ Called from PROJECT_FILE.i:487.
+[value] computing for function printf <- e_acsl_assert <- main.
+ Called from PROJECT_FILE.i:219.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_assert <- main.
+ Called from PROJECT_FILE.i:221.
+[value] Done for function exit
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+[value] computing for function __gmpz_clear <- main.
+ Called from PROJECT_FILE.i:488.
+[value] Done for function __gmpz_clear
+[value] computing for function __gmpz_clear <- main.
+ Called from PROJECT_FILE.i:489.
+[value] Done for function __gmpz_clear
+[value] Recording results for main
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values at end of function e_acsl_assert:
+[value] Values at end of function search:
+ __retres ∈ {0; 1}
+ k ∈ [0..10]
+ e_acsl_20 ∈ {0; 1}
+ e_acsl_33 ∈ {0; 1}
+[value] Values at end of function main:
+ A[0..9] ∈ [0..81]
+ __retres ∈ {0}
+ found ∈ {0}
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct mpz_t[1];
+/*@ ensures \valid(\old(x));
+ assigns *x; */
+extern void __gmpz_init(__mpz_struct * /*[1]*/ x);
+/*@ ensures \valid(\old(z));
+ assigns *z;
+ assigns *z \from n; */
+extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
+/*@ requires \valid(z_orig);
+ requires \valid(z);
+ assigns *z; */
+extern void __gmpz_set(__mpz_struct * /*[1]*/ z,
+ __mpz_struct const * /*[1]*/ z_orig);
+/*@ requires \valid(x);
+ assigns *x; */
+extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns \nothing; */
+extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2);
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ requires \valid(z3);
+ assigns *z1;
+*/
+extern void __gmpz_add(__mpz_struct * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2,
+ __mpz_struct const * /*[1]*/ z3);
+/*@ requires \valid(z);
+ assigns \nothing; */
+extern long __gmpz_get_si(__mpz_struct const * /*[1]*/ z);
+/*@ terminates \false;
+ ensures \false;
+ assigns \nothing; */
+extern void exit(int status);
+/*@ assigns \nothing; */
+extern int printf(char const * , ...);
+void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
+{
+ if (predicate) {
+ printf("%s failed at line %d.\nThe failing predicate is:\n%s.\n",kind,
+ line,pred_txt);
+ exit(1);
+ }
+ return;
+}
+
+int A[10];
+/*@ requires ∀ ℤ i; 0 ≤ i ∧ i < 9 ⇒ A[i] ≤ A[i+1];
+ behavior exists:
+ assumes ∃ ℤ j; (0 ≤ j ∧ j < 10) ∧ A[j] ≡ elt;
+ ensures \result ≡ 1;
+
+ behavior not_exists:
+ assumes ∀ ℤ j; 0 ≤ j ∧ j < 10 ⇒ A[j] ≢ elt;
+ ensures \result ≡ 0;
+
+
+*/
+int search(int elt)
+{
+ int __retres;
+ int k;
+ int e_acsl_20;
+ int e_acsl_33;
+ {
+ mpz_t e_acsl_1;
+ int e_acsl_2;
+ e_acsl_2 = 1;
+ __gmpz_init((__mpz_struct *)(e_acsl_1));
+ {
+ mpz_t e_acsl_7;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_7),(long)0);
+ __gmpz_set((__mpz_struct *)(e_acsl_1),(__mpz_struct const *)(e_acsl_7));
+ __gmpz_clear((__mpz_struct *)(e_acsl_7));
+ }
+
+ while (1) {
+ {
+ mpz_t e_acsl_8;
+ int e_acsl_9;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_8),(long)9);
+ e_acsl_9 = __gmpz_cmp((__mpz_struct const *)(e_acsl_1),
+ (__mpz_struct const *)(e_acsl_8));
+ if (! (e_acsl_9 < 0)) { break; }
+ __gmpz_clear((__mpz_struct *)(e_acsl_8));
+ }
+
+ {
+ int e_acsl_3;
+ mpz_t e_acsl_4;
+ mpz_t e_acsl_5;
+ int e_acsl_6;
+ e_acsl_3 = (int)__gmpz_get_si((__mpz_struct const *)(e_acsl_1));
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_4),(long)1);
+ __gmpz_init((__mpz_struct *)(e_acsl_5));
+ __gmpz_add((__mpz_struct *)(e_acsl_5),
+ (__mpz_struct const *)(e_acsl_1),
+ (__mpz_struct const *)(e_acsl_4));
+ e_acsl_6 = (int)__gmpz_get_si((__mpz_struct const *)(e_acsl_5));
+ __gmpz_clear((__mpz_struct *)(e_acsl_4));
+ __gmpz_clear((__mpz_struct *)(e_acsl_5));
+ /*@ assert 0 ≤ e_acsl_3 ∧ e_acsl_3 < 10;
+ // synthesized
+ */
+ /*@ assert 0 ≤ e_acsl_6 ∧ e_acsl_6 < 10;
+ // synthesized
+ */
+ if (! (A[e_acsl_3] <= A[e_acsl_6])) {
+ e_acsl_2 = 0;
+ goto e_acsl_end_loop1;
+ }
+ }
+
+ {
+ mpz_t e_acsl_10;
+ mpz_t e_acsl_11;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_10),(long)((char)1));
+ __gmpz_init((__mpz_struct *)(e_acsl_11));
+ __gmpz_add((__mpz_struct *)(e_acsl_11),
+ (__mpz_struct const *)(e_acsl_1),
+ (__mpz_struct const *)(e_acsl_10));
+ __gmpz_set((__mpz_struct *)(e_acsl_1),
+ (__mpz_struct const *)(e_acsl_11));
+ __gmpz_clear((__mpz_struct *)(e_acsl_10));
+ __gmpz_clear((__mpz_struct *)(e_acsl_11));
+ }
+
+ }
+ e_acsl_end_loop1: ;
+ e_acsl_assert(! e_acsl_2,(char *)"Precondition",
+ (char *)"(\\forall integer i; 0 <= i && i < 9 ==> A[i] <= A[i+1])",
+ 8);
+ __gmpz_clear((__mpz_struct *)(e_acsl_1));
+ {
+ mpz_t e_acsl_25;
+ int e_acsl_26;
+ e_acsl_26 = 1;
+ __gmpz_init((__mpz_struct *)(e_acsl_25));
+ {
+ mpz_t e_acsl_28;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_28),(long)0);
+ __gmpz_set((__mpz_struct *)(e_acsl_25),
+ (__mpz_struct const *)(e_acsl_28));
+ __gmpz_clear((__mpz_struct *)(e_acsl_28));
+ }
+
+ while (1) {
+ {
+ mpz_t e_acsl_29;
+ int e_acsl_30;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_29),(long)10);
+ e_acsl_30 = __gmpz_cmp((__mpz_struct const *)(e_acsl_25),
+ (__mpz_struct const *)(e_acsl_29));
+ if (! (e_acsl_30 < 0)) { break; }
+ __gmpz_clear((__mpz_struct *)(e_acsl_29));
+ }
+
+ {
+ int e_acsl_27;
+ e_acsl_27 = (int)__gmpz_get_si((__mpz_struct const *)(e_acsl_25));
+ /*@ assert 0 ≤ e_acsl_27 ∧ e_acsl_27 < 10;
+ // synthesized
+ */
+ if (! (A[e_acsl_27] != elt)) {
+ e_acsl_26 = 0;
+ goto e_acsl_end_loop3;
+ }
+ }
+
+ {
+ mpz_t e_acsl_31;
+ mpz_t e_acsl_32;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_31),(long)((char)1));
+ __gmpz_init((__mpz_struct *)(e_acsl_32));
+ __gmpz_add((__mpz_struct *)(e_acsl_32),
+ (__mpz_struct const *)(e_acsl_25),
+ (__mpz_struct const *)(e_acsl_31));
+ __gmpz_set((__mpz_struct *)(e_acsl_25),
+ (__mpz_struct const *)(e_acsl_32));
+ __gmpz_clear((__mpz_struct *)(e_acsl_31));
+ __gmpz_clear((__mpz_struct *)(e_acsl_32));
+ }
+
+ }
+ e_acsl_end_loop3: ;
+ e_acsl_33 = e_acsl_26;
+ __gmpz_clear((__mpz_struct *)(e_acsl_25));
+ }
+
+ {
+ mpz_t e_acsl_12;
+ int e_acsl_13;
+ e_acsl_13 = 0;
+ __gmpz_init((__mpz_struct *)(e_acsl_12));
+ {
+ mpz_t e_acsl_15;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_15),(long)0);
+ __gmpz_set((__mpz_struct *)(e_acsl_12),
+ (__mpz_struct const *)(e_acsl_15));
+ __gmpz_clear((__mpz_struct *)(e_acsl_15));
+ }
+
+ while (1) {
+ {
+ mpz_t e_acsl_16;
+ int e_acsl_17;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_16),(long)10);
+ e_acsl_17 = __gmpz_cmp((__mpz_struct const *)(e_acsl_12),
+ (__mpz_struct const *)(e_acsl_16));
+ if (! (e_acsl_17 < 0)) { break; }
+ __gmpz_clear((__mpz_struct *)(e_acsl_16));
+ }
+
+ {
+ int e_acsl_14;
+ e_acsl_14 = (int)__gmpz_get_si((__mpz_struct const *)(e_acsl_12));
+ /*@ assert 0 ≤ e_acsl_14 ∧ e_acsl_14 < 10;
+ // synthesized
+ */
+ if (! (! (A[e_acsl_14] == elt))) {
+ e_acsl_13 = 1;
+ goto e_acsl_end_loop2;
+ }
+ }
+
+ {
+ mpz_t e_acsl_18;
+ mpz_t e_acsl_19;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_18),(long)((char)1));
+ __gmpz_init((__mpz_struct *)(e_acsl_19));
+ __gmpz_add((__mpz_struct *)(e_acsl_19),
+ (__mpz_struct const *)(e_acsl_12),
+ (__mpz_struct const *)(e_acsl_18));
+ __gmpz_set((__mpz_struct *)(e_acsl_12),
+ (__mpz_struct const *)(e_acsl_19));
+ __gmpz_clear((__mpz_struct *)(e_acsl_18));
+ __gmpz_clear((__mpz_struct *)(e_acsl_19));
+ }
+
+ }
+ e_acsl_end_loop2: ;
+ e_acsl_20 = e_acsl_13;
+ __gmpz_clear((__mpz_struct *)(e_acsl_12));
+ }
+
+ k = 0;
+ }
+
+ while (1) {
+ if (! (k < 10)) { break; }
+ if (A[k] == elt) {
+ __retres = 1;
+ goto return_label; }
+ else {
+ if (A[k] > elt) {
+ __retres = 0;
+ goto return_label; } }
+ k ++;
+ }
+ __retres = 0;
+ return_label:
+ {
+ int e_acsl_24;
+ int e_acsl_37;
+ if (! e_acsl_20) { e_acsl_24 = 1; }
+ else {
+ mpz_t e_acsl_21;
+ mpz_t e_acsl_22;
+ int e_acsl_23;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_21),(long)__retres);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_22),(long)1);
+ e_acsl_23 = __gmpz_cmp((__mpz_struct const *)(e_acsl_21),
+ (__mpz_struct const *)(e_acsl_22));
+ e_acsl_24 = e_acsl_23 == 0;
+ __gmpz_clear((__mpz_struct *)(e_acsl_21));
+ __gmpz_clear((__mpz_struct *)(e_acsl_22));
+ }
+ e_acsl_assert(! e_acsl_24,(char *)"Postcondition",
+ (char *)"(\\old(\\exists integer j; (0 <= j && j < 10) && A[j] == elt) ==> \\result == 1)",
+ 11);
+ if (! e_acsl_33) { e_acsl_37 = 1; }
+ else {
+ mpz_t e_acsl_34;
+ mpz_t e_acsl_35;
+ int e_acsl_36;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_34),(long)__retres);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_35),(long)0);
+ e_acsl_36 = __gmpz_cmp((__mpz_struct const *)(e_acsl_34),
+ (__mpz_struct const *)(e_acsl_35));
+ e_acsl_37 = e_acsl_36 == 0;
+ __gmpz_clear((__mpz_struct *)(e_acsl_34));
+ __gmpz_clear((__mpz_struct *)(e_acsl_35));
+ }
+ e_acsl_assert(! e_acsl_37,(char *)"Postcondition",
+ (char *)"(\\old(\\forall integer j; 0 <= j && j < 10 ==> A[j] != elt) ==> \\result == 0)",
+ 14);
+ return (__retres);
+ }
+
+}
+
+int main(void)
+{
+ int __retres;
+ int found;
+ { int i;
+ i = 0;
+ while (1) {
+ if (! (i < 10)) { break; }
+ A[i] = i * i;
+ i ++; } }
+
+ found = search(36);
+ /*@ assert found ≡ 1; */ ;
+ {
+ mpz_t e_acsl_1;
+ mpz_t e_acsl_2;
+ int e_acsl_3;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_1),(long)found);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)1);
+ e_acsl_3 = __gmpz_cmp((__mpz_struct const *)(e_acsl_1),
+ (__mpz_struct const *)(e_acsl_2));
+ e_acsl_assert(! (e_acsl_3 == 0),(char *)"Assertion",
+ (char *)"(found == 1)",30);
+ __gmpz_clear((__mpz_struct *)(e_acsl_1));
+ __gmpz_clear((__mpz_struct *)(e_acsl_2));
+ }
+
+ found = search(5);
+ /*@ assert found ≡ 0; */ ;
+ {
+ mpz_t e_acsl_4;
+ mpz_t e_acsl_5;
+ int e_acsl_6;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_4),(long)found);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_5),(long)0);
+ e_acsl_6 = __gmpz_cmp((__mpz_struct const *)(e_acsl_4),
+ (__mpz_struct const *)(e_acsl_5));
+ e_acsl_assert(! (e_acsl_6 == 0),(char *)"Assertion",
+ (char *)"(found == 0)",33);
+ __gmpz_clear((__mpz_struct *)(e_acsl_4));
+ __gmpz_clear((__mpz_struct *)(e_acsl_5));
+ }
+
+ __retres = 0;
+ return (__retres);
+}
+
+
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 184c183d6af469c2a1945fa51a5ca88894e46ddb..4f131e9563a56405650a74444ae7f460cde94b15 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -110,6 +110,13 @@ let principal_type_from_term t1 t2 =
in
principal_type (typ t1) (typ t2)
+let is_representable _n k _s = match k with
+ | IBool | IChar | IUChar | IUInt | IUShort | IULong | ISChar | IShort | IInt
+ | ILong ->
+ true
+ | ILongLong | IULongLong ->
+ false
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index fa5269c9293f073709413a7ddfa45b386c4b5aaf..cbfa80a6b37a56f26b60f80034e0ebee9a66911c 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -24,6 +24,8 @@ open Cil_types
(** Typing rules. *)
+(* TODO: to be improved *)
+
val principal_type: logic_type -> logic_type -> logic_type
val principal_type_from_term: term -> term -> logic_type
@@ -31,6 +33,10 @@ val context_sensitive:
?loc:location -> Env.t -> logic_type -> bool -> term option -> exp ->
exp * Env.t
+val is_representable: My_bigint.t -> ikind -> string option -> bool
+(** Is the given constant representable?
+ (See [Cil_types.CInt64] for details about arguments *)
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 59b78bb42fa31769b9a5a77f67420560b066c7c4..faa1d7d2d00cf339651c4e0002a030bc4be417f9 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -45,16 +45,9 @@ let name_of_mpz_arith_bop = function
| Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr
| Shiftlt | Shiftrt | PlusPI | IndexPI | MinusPI | MinusPP -> assert false
-let is_representable _n k _s = match k with
- | IBool | IChar | IUChar | IUInt | IUShort | IULong | ISChar | IShort | IInt
- | ILong ->
- true
- | ILongLong | IULongLong ->
- false
-
let constant_to_exp ?(loc=Location.unknown) = function
| CInt64(n, k, s) ->
- if is_representable n k s then kinteger64_repr ?loc k n s, false
+ if Typing.is_representable n k s then kinteger64_repr ?loc k n s, false
else mkString ?loc (My_bigint.to_string n), true
| CStr _ | CWStr _ | CChr _ | CReal _ | CEnum _ as c ->
new_exp ?loc (Const c), false
@@ -662,7 +655,7 @@ class e_acsl_visitor prj generate = object (self)
let mk_block stmt =
(* be careful: as this function is called in a post action, [env] has
been modified since pre actions have been executed.
- Use [function_env] to store it. *)
+ Use [function_env] to get it back. *)
let env = !function_env in
let mk_block b = mkStmt ~valid_sid:true (Block b) in
let mk_post_env env =
@@ -683,7 +676,39 @@ class e_acsl_visitor prj generate = object (self)
(* also handle the postcondition of the function and clear the env *)
let env = Project.on prj (convert_post_spec env) !funspec in
let b, env = Env.pop_and_get env stmt ~global_clear:true Env.After in
- mk_block b, env
+ let new_stmt = mk_block b in
+ let labels = stmt.labels in
+ (match labels with
+ | [] -> ()
+ | _ :: _ ->
+ (* move the labels of the return to the new block in order to
+ evaluate the postcondition when jumping to them. *)
+ stmt.labels <- [];
+ new_stmt.labels <- labels @ new_stmt.labels;
+ (* update the gotos of the function jumping to one of the labels *)
+ let o = object
+ inherit Visitor.frama_c_inplace
+ method vstmt_aux s = match s.skind with
+ | Goto(s_ref, _) ->
+ (* [!s_ref] and [stmt] are not part of the same project, thus it
+ is safer to compare the ids than to use Stmt.equal *)
+ if !s_ref.sid = stmt.sid then s_ref := new_stmt;
+ SkipChildren
+ | _ -> DoChildren
+ (* improve efficiency: skip childrens of vstmt which cannot
+ contain any stmt *)
+ method vinst _ = SkipChildren
+ method vexpr _ = SkipChildren
+ method vcode_annot _ = SkipChildren
+ method vlval _ = SkipChildren
+ end in
+ let vis = Env.get_visitor env in
+ let f = Extlib.the vis#current_func in
+ let mv_label s =
+ ignore (Visitor.visitFramacStmt o (get_stmt vis#behavior s))
+ in
+ List.iter mv_label f.sallstmts);
+ new_stmt, env
else
(* must generate [pre_block] which includes [stmt] before generating
[post_block] *)