diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/at.i b/src/plugins/e-acsl/tests/e-acsl-runtime/at.i
index 5e7a85ac143a64f88c31d1626073cd2cad3a89e6..9ca397f65f6927364e962f610b0f1b674a6e8d60 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/at.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/at.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: \at
- EXECNOW: LOG gen_at.c BIN gen_at.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/at.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_at.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_at.out ./tests/e-acsl-runtime/result/gen_at.c -lgmp
+ EXECNOW: LOG gen_at.c BIN gen_at.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/at.i -e-acsl-project p -e-acsl-include-headers -then-on p -print -ocode ./tests/e-acsl-runtime/result/gen_at.c > /dev/null && gcc -o ./tests/e-acsl-runtime/result/gen_at.out ./tests/e-acsl-runtime/result/gen_at.c -lgmp && ./tests/e-acsl-runtime/result/gen_at.out
*/
int A = 0;
@@ -16,6 +16,26 @@ void f(void) {
A = 3;
}
+/* /\*@ requires \valid(p); */
+/* @ requires \valid(p+1); */
+/* @ requires \valid(q); */
+/* @*\/ */
+void g(int *p, int *q) {
+ *p = 0;
+ *(p+1) = 1;
+ *q = 0;
+ L1: *p = 2;
+ *(p+1) = 3;
+ *q = 1;
+ L2: A = 4;
+ /*@ assert (\at(*(p+\at(*q,L1)),L2) == 2); */
+ L3:
+ /*@ assert (\at(*(p+\at(*q,L1)),Here) == 2); */
+ // /*@ assert (\at(*(p+\at(*q,L1)),L3) == 2); */ // doesn't work yet
+ // /*@ assert (\at(*(p+\at(*q,L2)),L1)) == 1; */
+ return ;
+}
+
int main(void) {
int x;
@@ -30,5 +50,8 @@ int main(void) {
/*@ assert \at(x+1,L) == 1; */
/*@ assert \at(x,L)+1 == 1; */
+ int t[2];
+ g(t,&x);
+
return 0;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
index c369b56ec411fffba0a3bdf432fada0e75ed511b..a167a416e324980c98d827d341d2a2f8ad615d2f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
@@ -1,53 +1,59 @@
+tests/e-acsl-runtime/at.i:31:[e-acsl] warning: missing guard for ensuring that q is a valid memory access
+tests/e-acsl-runtime/at.i:31:[e-acsl] warning: missing guard for ensuring that p+\at(*q,L1) is a valid pointer
+tests/e-acsl-runtime/at.i:31:[e-acsl] warning: missing guard for ensuring that p+\at(*q,L1) is a valid memory access
+tests/e-acsl-runtime/at.i:33:[e-acsl] warning: missing guard for ensuring that q is a valid memory access
+tests/e-acsl-runtime/at.i:33:[e-acsl] warning: missing guard for ensuring that p+\at(*q,L1) is a valid pointer
+tests/e-acsl-runtime/at.i:33:[e-acsl] warning: missing guard for ensuring that p+\at(*q,L1) is a valid memory access
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
A ∈ {0}
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:236.
+ Called from PROJECT_FILE.i:291.
PROJECT_FILE.i:33:[value] Function mpz_init_set_si: postcondition got status valid.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:237.
+ Called from PROJECT_FILE.i:292.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:238.
+ Called from PROJECT_FILE.i:293.
PROJECT_FILE.i:21:[value] Function mpz_init: postcondition got status valid.
[value] Done for function mpz_init
[value] computing for function mpz_add <- main.
- Called from PROJECT_FILE.i:239.
+ Called from PROJECT_FILE.i:294.
PROJECT_FILE.i:64:[value] Function mpz_add: precondition got status valid.
PROJECT_FILE.i:65:[value] Function mpz_add: precondition got status valid.
PROJECT_FILE.i:66:[value] Function mpz_add: precondition got status valid.
[value] Done for function mpz_add
[value] computing for function mpz_init_set <- main.
- Called from PROJECT_FILE.i:240.
+ Called from PROJECT_FILE.i:295.
PROJECT_FILE.i:25:[value] Function mpz_init_set: postcondition got status valid.
[value] Done for function mpz_init_set
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:241.
+ Called from PROJECT_FILE.i:296.
PROJECT_FILE.i:43:[value] Function mpz_clear: precondition got status valid.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:242.
+ Called from PROJECT_FILE.i:297.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:243.
+ Called from PROJECT_FILE.i:298.
[value] Done for function mpz_clear
-PROJECT_FILE.i:247:[value] Assertion got status valid.
+PROJECT_FILE.i:302:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:252.
+ Called from PROJECT_FILE.i:307.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:253.
+ Called from PROJECT_FILE.i:308.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:254.
+ Called from PROJECT_FILE.i:309.
PROJECT_FILE.i:49:[value] Function mpz_cmp: precondition got status valid.
PROJECT_FILE.i:50:[value] Function mpz_cmp: precondition got status valid.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:255.
+ Called from PROJECT_FILE.i:310.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
[value] Done for function printf
@@ -58,13 +64,13 @@ PROJECT_FILE.i:119:[value] Function exit: postcondition got status invalid.
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:256.
+ Called from PROJECT_FILE.i:311.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:257.
+ Called from PROJECT_FILE.i:312.
[value] Done for function mpz_clear
[value] computing for function f <- main.
- Called from PROJECT_FILE.i:263.
+ Called from PROJECT_FILE.i:318.
PROJECT_FILE.i:148:[value] Assertion got status valid.
[value] computing for function mpz_init_set_si <- f <- main.
Called from PROJECT_FILE.i:153.
@@ -197,18 +203,18 @@ PROJECT_FILE.i:191:[value] Assertion got status unknown.
PROJECT_FILE.i:132:[value] Function f: postcondition got status valid.
[value] Recording results for f
[value] Done for function f
-PROJECT_FILE.i:264:[value] Assertion got status unknown.
+PROJECT_FILE.i:319:[value] Assertion got status unknown.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:269.
+ Called from PROJECT_FILE.i:324.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:270.
+ Called from PROJECT_FILE.i:325.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:271.
+ Called from PROJECT_FILE.i:326.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:272.
+ Called from PROJECT_FILE.i:327.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
[value] Done for function printf
@@ -218,20 +224,20 @@ PROJECT_FILE.i:264:[value] Assertion got status unknown.
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:273.
+ Called from PROJECT_FILE.i:328.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:274.
+ Called from PROJECT_FILE.i:329.
[value] Done for function mpz_clear
-PROJECT_FILE.i:278:[value] Assertion got status unknown.
+PROJECT_FILE.i:333:[value] Assertion got status unknown.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:282.
+ Called from PROJECT_FILE.i:337.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:283.
+ Called from PROJECT_FILE.i:338.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:284.
+ Called from PROJECT_FILE.i:339.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
[value] Done for function printf
@@ -241,26 +247,26 @@ PROJECT_FILE.i:278:[value] Assertion got status unknown.
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:285.
+ Called from PROJECT_FILE.i:340.
[value] Done for function mpz_clear
-PROJECT_FILE.i:289:[value] Assertion got status unknown.
+PROJECT_FILE.i:344:[value] Assertion got status unknown.
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:295.
+ Called from PROJECT_FILE.i:350.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init_set_si <- main.
- Called from PROJECT_FILE.i:296.
+ Called from PROJECT_FILE.i:351.
[value] Done for function mpz_init_set_si
[value] computing for function mpz_init <- main.
- Called from PROJECT_FILE.i:297.
+ Called from PROJECT_FILE.i:352.
[value] Done for function mpz_init
[value] computing for function mpz_add <- main.
- Called from PROJECT_FILE.i:298.
+ Called from PROJECT_FILE.i:353.
[value] Done for function mpz_add
[value] computing for function mpz_cmp <- main.
- Called from PROJECT_FILE.i:299.
+ Called from PROJECT_FILE.i:354.
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <- main.
- Called from PROJECT_FILE.i:300.
+ Called from PROJECT_FILE.i:355.
[value] computing for function printf <- e_acsl_fail <- main.
Called from PROJECT_FILE.i:129.
[value] Done for function printf
@@ -270,16 +276,72 @@ PROJECT_FILE.i:289:[value] Assertion got status unknown.
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:301.
+ Called from PROJECT_FILE.i:356.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:302.
+ Called from PROJECT_FILE.i:357.
[value] Done for function mpz_clear
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:303.
+ Called from PROJECT_FILE.i:358.
[value] Done for function mpz_clear
+[value] computing for function g <- main.
+ Called from PROJECT_FILE.i:362.
+PROJECT_FILE.i:240:[value] Assertion got status unknown.
+[value] computing for function mpz_init_set_si <- g <- main.
+ Called from PROJECT_FILE.i:245.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- g <- main.
+ Called from PROJECT_FILE.i:246.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_cmp <- g <- main.
+ Called from PROJECT_FILE.i:247.
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <- g <- main.
+ Called from PROJECT_FILE.i:248.
+[value] computing for function printf <- e_acsl_fail <- g <- main.
+ Called from PROJECT_FILE.i:129.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_fail <- g <- main.
+ Called from PROJECT_FILE.i:129.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <- g <- main.
+ Called from PROJECT_FILE.i:250.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- g <- main.
+ Called from PROJECT_FILE.i:251.
+[value] Done for function mpz_clear
+PROJECT_FILE.i:256:[value] Assertion got status unknown.
+[value] computing for function mpz_init_set_si <- g <- main.
+ Called from PROJECT_FILE.i:262.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_init_set_si <- g <- main.
+ Called from PROJECT_FILE.i:263.
+[value] Done for function mpz_init_set_si
+[value] computing for function mpz_cmp <- g <- main.
+ Called from PROJECT_FILE.i:264.
+[value] Done for function mpz_cmp
+[value] computing for function e_acsl_fail <- g <- main.
+ Called from PROJECT_FILE.i:266.
+[value] computing for function printf <- e_acsl_fail <- g <- main.
+ Called from PROJECT_FILE.i:129.
+[value] Done for function printf
+[value] computing for function exit <- e_acsl_fail <- g <- main.
+ Called from PROJECT_FILE.i:129.
+[value] Done for function exit
+[value] Recording results for e_acsl_fail
+[value] Done for function e_acsl_fail
+[value] computing for function mpz_clear <- g <- main.
+ Called from PROJECT_FILE.i:268.
+[value] Done for function mpz_clear
+[value] computing for function mpz_clear <- g <- main.
+ Called from PROJECT_FILE.i:269.
+[value] Done for function mpz_clear
+[value] Recording results for g
+[value] Done for function g
[value] computing for function mpz_clear <- main.
- Called from PROJECT_FILE.i:308.
+ Called from PROJECT_FILE.i:364.
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
@@ -294,10 +356,21 @@ PROJECT_FILE.i:289:[value] Assertion got status unknown.
e_acsl_13 ∈ {0}
e_acsl_14 ∈ {0}
e_acsl_18 ∈ {3}
+[value] Values for function g:
+ A ∈ {4}
+ e_acsl_1 ∈ {0}
+ e_acsl_2 ∈ {2}
+ e_acsl_6 ∈ {0}
+ e_acsl_7 ∈ {2}
+ x ∈ {1}
+ t[0] ∈ {2}
+ [1] ∈ {3}
[value] Values for function main:
- A ∈ {3}
+ A ∈ {4}
__retres ∈ {0}
- x ∈ {2}
+ x ∈ {1}
+ t[0] ∈ {2}
+ [1] ∈ {3}
e_acsl_4 ∈ {0}
e_acsl_11[0] ∈ [--..--] or UNINITIALIZED
e_acsl_14 ∈ {0}
@@ -442,10 +515,64 @@ void f(void)
}
+void g(int *p, int *q)
+{
+ int e_acsl_1;
+ int e_acsl_2;
+ int e_acsl_6;
+ int e_acsl_7;
+ *p = 0;
+ *(p + 1) = 1;
+ *q = 0;
+ L1: e_acsl_6 = *q;
+ e_acsl_1 = *q;
+ *p = 2;
+ *(p + 1) = 3;
+ *q = 1;
+ L2: e_acsl_2 = *(p + e_acsl_1);
+ A = 4;
+ /*@ assert \at(*(p+\at(*q,L1)),L2) ≡ 2; */ ;
+ {
+ mpz_t e_acsl_3;
+ mpz_t e_acsl_4;
+ int e_acsl_5;
+ mpz_init_set_si((__mpz_struct *)(e_acsl_3),(long)e_acsl_2);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_4),(long)2);
+ e_acsl_5 = mpz_cmp((__mpz_struct const *)(e_acsl_3),
+ (__mpz_struct const *)(e_acsl_4));
+ if (! (e_acsl_5 == 0)) {
+ e_acsl_fail((char *)"(\\at(*(p+\\at(*q,L1)),L2) == 2)");
+ }
+ mpz_clear((__mpz_struct *)(e_acsl_3));
+ mpz_clear((__mpz_struct *)(e_acsl_4));
+ }
+
+ L3:
+ /*@ assert \at(*(p+\at(*q,L1)),Here) ≡ 2; */ ;
+ {
+ mpz_t e_acsl_8;
+ mpz_t e_acsl_9;
+ int e_acsl_10;
+ e_acsl_7 = *(p + e_acsl_6);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_8),(long)e_acsl_7);
+ mpz_init_set_si((__mpz_struct *)(e_acsl_9),(long)2);
+ e_acsl_10 = mpz_cmp((__mpz_struct const *)(e_acsl_8),
+ (__mpz_struct const *)(e_acsl_9));
+ if (! (e_acsl_10 == 0)) {
+ e_acsl_fail((char *)"(\\at(*(p+\\at(*q,L1)),Here) == 2)");
+ }
+ mpz_clear((__mpz_struct *)(e_acsl_8));
+ mpz_clear((__mpz_struct *)(e_acsl_9));
+ }
+
+ return;
+}
+
int main(void)
{
int __retres;
int x;
+ int t[2];
int e_acsl_4;
mpz_t e_acsl_11;
int e_acsl_14;
@@ -529,6 +656,7 @@ int main(void)
mpz_clear((__mpz_struct *)(e_acsl_17));
}
+ g(t,& x);
__retres = 0;
mpz_clear((__mpz_struct *)(e_acsl_11));
return (__retres);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
index 2a78fbc5edb263eb52f2faf670dfb6514bdb2a09..70db2542d422729cca6f23e892719892600de362 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
@@ -718,10 +718,64 @@ void f(void)
}
+void g(int *p, int *q)
+{
+ int e_acsl_1;
+ int e_acsl_2;
+ int e_acsl_6;
+ int e_acsl_7;
+ *p = 0;
+ *(p + 1) = 1;
+ *q = 0;
+ L1: e_acsl_6 = *q;
+ e_acsl_1 = *q;
+ *p = 2;
+ *(p + 1) = 3;
+ *q = 1;
+ L2: e_acsl_2 = *(p + e_acsl_1);
+ A = 4;
+ /*@ assert \at(*(p+\at(*q,L1)),L2) ≡ 2; */ ;
+ {
+ mpz_t e_acsl_3;
+ mpz_t e_acsl_4;
+ int e_acsl_5;
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_3),(long)e_acsl_2);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_4),(long)2);
+ e_acsl_5 = __gmpz_cmp((__mpz_struct const *)(e_acsl_3),
+ (__mpz_struct const *)(e_acsl_4));
+ if (! (e_acsl_5 == 0)) {
+ e_acsl_fail((char *)"(\\at(*(p+\\at(*q,L1)),L2) == 2)");
+ }
+ __gmpz_clear((__mpz_struct *)(e_acsl_3));
+ __gmpz_clear((__mpz_struct *)(e_acsl_4));
+ }
+
+ L3:
+ /*@ assert \at(*(p+\at(*q,L1)),Here) ≡ 2; */ ;
+ {
+ mpz_t e_acsl_8;
+ mpz_t e_acsl_9;
+ int e_acsl_10;
+ e_acsl_7 = *(p + e_acsl_6);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_8),(long)e_acsl_7);
+ __gmpz_init_set_si((__mpz_struct *)(e_acsl_9),(long)2);
+ e_acsl_10 = __gmpz_cmp((__mpz_struct const *)(e_acsl_8),
+ (__mpz_struct const *)(e_acsl_9));
+ if (! (e_acsl_10 == 0)) {
+ e_acsl_fail((char *)"(\\at(*(p+\\at(*q,L1)),Here) == 2)");
+ }
+ __gmpz_clear((__mpz_struct *)(e_acsl_8));
+ __gmpz_clear((__mpz_struct *)(e_acsl_9));
+ }
+
+ return;
+}
+
int main(void)
{
int __retres;
int x;
+ int t[2];
int e_acsl_4;
mpz_t e_acsl_11;
int e_acsl_14;
@@ -805,6 +859,7 @@ int main(void)
__gmpz_clear((__mpz_struct *)(e_acsl_17));
}
+ g(t,& x);
__retres = 0;
__gmpz_clear((__mpz_struct *)(e_acsl_11));
return (__retres);