Skip to content
Snippets Groups Projects
Commit 01c1a8fd authored by Fonenantsoa Maurica's avatar Fonenantsoa Maurica
Browse files

add -eva-no-alloc-returns-null to gmp/test_config

parent a8665b8a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/tests/gmp/oracle/at_on-purely-logic-variables.0.res.oracle
+ 16
− 88
View file @ 01c1a8fd
...@@ -35,15 +35,10 @@ ...@@ -35,15 +35,10 @@
allocating variable __malloc_main_l28 allocating variable __malloc_main_l28
[eva] using specification for function __e_acsl_store_block [eva] using specification for function __e_acsl_store_block
[eva] using specification for function __e_acsl_full_init [eva] using specification for function __e_acsl_full_init
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:37: Warning:
out of bounds write. assert \valid(__gen_e_acsl_at_4 + 0);
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
out of bounds write.
assert \valid(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_j_2 - 2));
[eva] tests/gmp/at_on-purely-logic-variables.c:29: [eva] tests/gmp/at_on-purely-logic-variables.c:29:
starting to merge loop iterations starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:28: Warning: [eva] tests/gmp/at_on-purely-logic-variables.c:57:
out of bounds write. assert \valid(__gen_e_acsl_at + 0); starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:57: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:57: Warning:
out of bounds write. out of bounds write.
assert assert
...@@ -51,22 +46,8 @@ ...@@ -51,22 +46,8 @@
(int)((int)((int)(__gen_e_acsl_u_6 - 10) * 300) + (int)((int)((int)(__gen_e_acsl_u_6 - 10) * 300) +
(int)((int)((int)((int)(__gen_e_acsl_v_6 - -10) - 1) * 100) + (int)((int)((int)((int)(__gen_e_acsl_v_6 - -10) - 1) * 100) +
(int)((int)(__gen_e_acsl_w_2 - 100) - 1)))); (int)((int)(__gen_e_acsl_w_2 - 100) - 1))));
[eva] tests/gmp/at_on-purely-logic-variables.c:57:
starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:45: Warning:
out of bounds write.
assert
\valid(__gen_e_acsl_at_6 +
(int)((int)((int)(__gen_e_acsl_u_4 - 9) * 32) +
(int)((int)(__gen_e_acsl_v_4 - -5) - 1)));
[eva] tests/gmp/at_on-purely-logic-variables.c:45: [eva] tests/gmp/at_on-purely-logic-variables.c:45:
starting to merge loop iterations starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:34: Warning:
out of bounds write.
assert
\valid(__gen_e_acsl_at_3 +
(int)((int)((int)(__gen_e_acsl_u_2 - 9) * 11) +
(int)((int)(__gen_e_acsl_v_2 - -5) - 1)));
[eva] tests/gmp/at_on-purely-logic-variables.c:34: [eva] tests/gmp/at_on-purely-logic-variables.c:34:
starting to merge loop iterations starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:28: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:28: Warning:
...@@ -75,74 +56,52 @@ ...@@ -75,74 +56,52 @@
[eva] using specification for function __e_acsl_assert [eva] using specification for function __e_acsl_assert
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
assertion got status unknown. assertion got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
accessing uninitialized left-value. accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2)); assert \initialized(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2));
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
out of bounds read.
assert \valid_read(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_j - 2));
[eva] tests/gmp/at_on-purely-logic-variables.c:29: [eva] tests/gmp/at_on-purely-logic-variables.c:29:
starting to merge loop iterations starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:31: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:31: Warning:
assertion got status unknown. assertion got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:34: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:33: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:33: Warning:
accessing uninitialized left-value. accessing uninitialized left-value.
assert assert
\initialized(__gen_e_acsl_at_3 + \initialized(__gen_e_acsl_at_3 +
((__gen_e_acsl_u - 9) * 11 + ((__gen_e_acsl_v - -5) - 1))); ((__gen_e_acsl_u - 9) * 11 + ((__gen_e_acsl_v - -5) - 1)));
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:33: Warning:
out of bounds read.
assert
\valid_read(__gen_e_acsl_at_3 +
(int)((int)((int)(__gen_e_acsl_u - 9) * 11) +
(int)((int)(__gen_e_acsl_v - -5) - 1)));
[eva] tests/gmp/at_on-purely-logic-variables.c:33: [eva] tests/gmp/at_on-purely-logic-variables.c:33:
starting to merge loop iterations starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:34: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:37: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:37: Warning:
assertion got status unknown. assertion got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
out of bounds write.
assert \valid(__gen_e_acsl_at_5 + (int)((int)(__gen_e_acsl_k_4 - -9) - 1));
[eva] tests/gmp/at_on-purely-logic-variables.c:41: [eva] tests/gmp/at_on-purely-logic-variables.c:41:
starting to merge loop iterations starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
assertion got status unknown. assertion got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
accessing uninitialized left-value. accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1)); assert \initialized(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1));
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
out of bounds read.
assert
\valid_read(__gen_e_acsl_at_5 + (int)((int)(__gen_e_acsl_k_3 - -9) - 1));
[eva] tests/gmp/at_on-purely-logic-variables.c:41: [eva] tests/gmp/at_on-purely-logic-variables.c:41:
starting to merge loop iterations starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:43: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:43: Warning:
assertion got status unknown. assertion got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:45: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:44: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:44: Warning:
accessing uninitialized left-value. accessing uninitialized left-value.
assert assert
\initialized(__gen_e_acsl_at_6 + \initialized(__gen_e_acsl_at_6 +
((__gen_e_acsl_u_3 - 9) * 32 + ((__gen_e_acsl_v_3 - -5) - 1))); ((__gen_e_acsl_u_3 - 9) * 32 + ((__gen_e_acsl_v_3 - -5) - 1)));
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:44: Warning:
out of bounds read.
assert
\valid_read(__gen_e_acsl_at_6 +
(int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32) +
(int)((int)(__gen_e_acsl_v_3 - -5) - 1)));
[eva] tests/gmp/at_on-purely-logic-variables.c:44: [eva] tests/gmp/at_on-purely-logic-variables.c:44:
starting to merge loop iterations starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:45: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] tests/gmp/at_on-purely-logic-variables.c:8: [eva] tests/gmp/at_on-purely-logic-variables.c:8:
allocating variable __malloc___gen_e_acsl_f_l8 allocating variable __malloc___gen_e_acsl_f_l8
[eva] tests/gmp/at_on-purely-logic-variables.c:8: [eva] tests/gmp/at_on-purely-logic-variables.c:8:
...@@ -151,68 +110,44 @@ ...@@ -151,68 +110,44 @@
allocating variable __malloc___gen_e_acsl_f_l7 allocating variable __malloc___gen_e_acsl_f_l7
[eva] tests/gmp/at_on-purely-logic-variables.c:7: [eva] tests/gmp/at_on-purely-logic-variables.c:7:
allocating variable __malloc___gen_e_acsl_f_l7_0 allocating variable __malloc___gen_e_acsl_f_l7_0
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:8: Warning:
out of bounds write. assert \valid(__gen_e_acsl_at_4 + 0);
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:8: Warning:
out of bounds write. assert \valid(__gen_e_acsl_at_3 + 0);
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
out of bounds write.
assert \valid(__gen_e_acsl_at_2 + (int)((int)(__gen_e_acsl_n_3 - 1) - 1));
[eva] tests/gmp/at_on-purely-logic-variables.c:7: [eva] tests/gmp/at_on-purely-logic-variables.c:7:
starting to merge loop iterations starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
out of bounds write.
assert \valid(__gen_e_acsl_at + (int)((int)(__gen_e_acsl_n_2 - 1) - 1));
[eva] tests/gmp/at_on-purely-logic-variables.c:7: [eva] tests/gmp/at_on-purely-logic-variables.c:7:
starting to merge loop iterations starting to merge loop iterations
[eva] using specification for function __e_acsl_delete_block [eva] using specification for function __e_acsl_delete_block
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
accessing uninitialized left-value. accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1)); assert \initialized(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1));
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
out of bounds read.
assert \valid_read(__gen_e_acsl_at + (int)((int)(__gen_e_acsl_n - 1) - 1));
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
accessing uninitialized left-value. accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1)); assert \initialized(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
out of bounds read.
assert \valid_read(__gen_e_acsl_at_2 + (int)((int)(__gen_e_acsl_n - 1) - 1));
[eva] tests/gmp/at_on-purely-logic-variables.c:6: [eva] tests/gmp/at_on-purely-logic-variables.c:6:
starting to merge loop iterations starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:6: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:6: Warning:
function __gen_e_acsl_f: postcondition got status unknown. function __gen_e_acsl_f: postcondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:8: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:8: Warning:
function __gen_e_acsl_f: postcondition got status unknown. function __gen_e_acsl_f: postcondition got status unknown.
[eva] tests/gmp/at_on-purely-logic-variables.c:16: [eva] tests/gmp/at_on-purely-logic-variables.c:16:
allocating variable __malloc_g_l16 allocating variable __malloc_g_l16
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
out of bounds write.
assert \valid(__gen_e_acsl_at + (int)(__gen_e_acsl_w_2 - 3));
[eva] tests/gmp/at_on-purely-logic-variables.c:16: [eva] tests/gmp/at_on-purely-logic-variables.c:16:
starting to merge loop iterations starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
assertion got status unknown. assertion got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
accessing uninitialized left-value. accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at + (__gen_e_acsl_w - 3)); assert \initialized(__gen_e_acsl_at + (__gen_e_acsl_w - 3));
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
out of bounds read.
assert \valid_read(__gen_e_acsl_at + (int)(__gen_e_acsl_w - 3));
[eva] tests/gmp/at_on-purely-logic-variables.c:16: [eva] tests/gmp/at_on-purely-logic-variables.c:16:
starting to merge loop iterations starting to merge loop iterations
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:54: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:54: Warning:
assertion got status unknown. assertion got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:57: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:56: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:56: Warning:
accessing uninitialized left-value. accessing uninitialized left-value.
assert assert
...@@ -220,13 +155,6 @@ ...@@ -220,13 +155,6 @@
((__gen_e_acsl_u_5 - 10) * 300 + ((__gen_e_acsl_u_5 - 10) * 300 +
(((__gen_e_acsl_v_5 - -10) - 1) * 100 + (((__gen_e_acsl_v_5 - -10) - 1) * 100 +
((__gen_e_acsl_w - 100) - 1)))); ((__gen_e_acsl_w - 100) - 1))));
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:56: Warning:
out of bounds read.
assert
\valid_read(__gen_e_acsl_at_7 +
(int)((int)((int)(__gen_e_acsl_u_5 - 10) * 300) +
(int)((int)((int)((int)(__gen_e_acsl_v_5 - -10) - 1) * 100)
+ (int)((int)(__gen_e_acsl_w - 100) - 1))));
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:63: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:63: Warning:
assertion got status unknown. assertion got status unknown.
[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:65: Warning: [eva:alarm] tests/gmp/at_on-purely-logic-variables.c:65: Warning:
......
src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables.c
+ 0
− 87
View file @ 01c1a8fd
...@@ -28,10 +28,6 @@ void g(void) ...@@ -28,10 +28,6 @@ void g(void)
__gen_e_acsl_w_2 = 3; __gen_e_acsl_w_2 = 3;
while (1) { while (1) {
if (__gen_e_acsl_w_2 < 6) ; else break; if (__gen_e_acsl_w_2 < 6) ; else break;
/*@ assert
Value: mem_access:
\valid(__gen_e_acsl_at + (int)(__gen_e_acsl_w_2 - 3));
*/
*(__gen_e_acsl_at + (__gen_e_acsl_w_2 - 3)) = m + (long)__gen_e_acsl_w_2 == 12L; *(__gen_e_acsl_at + (__gen_e_acsl_w_2 - 3)) = m + (long)__gen_e_acsl_w_2 == 12L;
__gen_e_acsl_w_2 ++; __gen_e_acsl_w_2 ++;
} }
...@@ -61,10 +57,6 @@ void g(void) ...@@ -61,10 +57,6 @@ void g(void)
Value: initialization: Value: initialization:
\initialized(__gen_e_acsl_at + (__gen_e_acsl_w - 3)); \initialized(__gen_e_acsl_at + (__gen_e_acsl_w - 3));
*/ */
/*@ assert
Value: mem_access:
\valid_read(__gen_e_acsl_at + (int)(__gen_e_acsl_w - 3));
*/
if (! *(__gen_e_acsl_at + (__gen_e_acsl_w - 3))) ; if (! *(__gen_e_acsl_at + (__gen_e_acsl_w - 3))) ;
else { else {
__gen_e_acsl_exists = 1; __gen_e_acsl_exists = 1;
...@@ -109,7 +101,6 @@ int main(void) ...@@ -109,7 +101,6 @@ int main(void)
{ {
int __gen_e_acsl_i_4; int __gen_e_acsl_i_4;
__gen_e_acsl_i_4 = 3; __gen_e_acsl_i_4 = 3;
/*@ assert Value: mem_access: \valid(__gen_e_acsl_at_4 + 0); */
*(__gen_e_acsl_at_4 + 0) = n + (long)__gen_e_acsl_i_4; *(__gen_e_acsl_at_4 + 0) = n + (long)__gen_e_acsl_i_4;
} }
{ {
...@@ -117,10 +108,6 @@ int main(void) ...@@ -117,10 +108,6 @@ int main(void)
__gen_e_acsl_j_2 = 2; __gen_e_acsl_j_2 = 2;
while (1) { while (1) {
if (__gen_e_acsl_j_2 < 5) ; else break; if (__gen_e_acsl_j_2 < 5) ; else break;
/*@ assert
Value: mem_access:
\valid(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_j_2 - 2));
*/
*(__gen_e_acsl_at_2 + (__gen_e_acsl_j_2 - 2)) = n + (long)__gen_e_acsl_j_2 == 11L; *(__gen_e_acsl_at_2 + (__gen_e_acsl_j_2 - 2)) = n + (long)__gen_e_acsl_j_2 == 11L;
__gen_e_acsl_j_2 ++; __gen_e_acsl_j_2 ++;
} }
...@@ -128,7 +115,6 @@ int main(void) ...@@ -128,7 +115,6 @@ int main(void)
{ {
int __gen_e_acsl_i_2; int __gen_e_acsl_i_2;
__gen_e_acsl_i_2 = 3; __gen_e_acsl_i_2 = 3;
/*@ assert Value: mem_access: \valid(__gen_e_acsl_at + 0); */
*(__gen_e_acsl_at + 0) = n + (long)__gen_e_acsl_i_2 == 10L; *(__gen_e_acsl_at + 0) = n + (long)__gen_e_acsl_i_2 == 10L;
} }
; ;
...@@ -195,12 +181,6 @@ int main(void) ...@@ -195,12 +181,6 @@ int main(void)
else __gen_e_acsl_if_2 = 3; else __gen_e_acsl_if_2 = 3;
if (__gen_e_acsl_v_4 <= __gen_e_acsl_if_2) ; else break; if (__gen_e_acsl_v_4 <= __gen_e_acsl_if_2) ; else break;
} }
/*@ assert
Value: mem_access:
\valid(__gen_e_acsl_at_6 +
(int)((int)((int)(__gen_e_acsl_u_4 - 9) * 32) +
(int)((int)(__gen_e_acsl_v_4 - -5) - 1)));
*/
*(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_4 - 9) * 32 + ((__gen_e_acsl_v_4 - -5) - 1))) = *(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_4 - 9) * 32 + ((__gen_e_acsl_v_4 - -5) - 1))) =
(n + (long)__gen_e_acsl_u_4) + n > 0L; (n + (long)__gen_e_acsl_u_4) + n > 0L;
__gen_e_acsl_v_4 ++; __gen_e_acsl_v_4 ++;
...@@ -223,12 +203,6 @@ int main(void) ...@@ -223,12 +203,6 @@ int main(void)
long __gen_e_acsl_if; long __gen_e_acsl_if;
if (__gen_e_acsl_u_2 > 0) __gen_e_acsl_if = n + (long)__gen_e_acsl_k_2; if (__gen_e_acsl_u_2 > 0) __gen_e_acsl_if = n + (long)__gen_e_acsl_k_2;
else __gen_e_acsl_if = __gen_e_acsl_u_2 + __gen_e_acsl_v_2; else __gen_e_acsl_if = __gen_e_acsl_u_2 + __gen_e_acsl_v_2;
/*@ assert
Value: mem_access:
\valid(__gen_e_acsl_at_3 +
(int)((int)((int)(__gen_e_acsl_u_2 - 9) * 11) +
(int)((int)(__gen_e_acsl_v_2 - -5) - 1)));
*/
*(__gen_e_acsl_at_3 + ((__gen_e_acsl_u_2 - 9) * 11 + ((__gen_e_acsl_v_2 - -5) - 1))) = *(__gen_e_acsl_at_3 + ((__gen_e_acsl_u_2 - 9) * 11 + ((__gen_e_acsl_v_2 - -5) - 1))) =
__gen_e_acsl_if > 0L; __gen_e_acsl_if > 0L;
} }
...@@ -280,10 +254,6 @@ int main(void) ...@@ -280,10 +254,6 @@ int main(void)
Value: initialization: Value: initialization:
\initialized(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2)); \initialized(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2));
*/ */
/*@ assert
Value: mem_access:
\valid_read(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_j - 2));
*/
if (! *(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2))) ; if (! *(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2))) ;
else { else {
__gen_e_acsl_exists = 1; __gen_e_acsl_exists = 1;
...@@ -339,12 +309,6 @@ int main(void) ...@@ -339,12 +309,6 @@ int main(void)
((__gen_e_acsl_u - 9) * 11 + ((__gen_e_acsl_u - 9) * 11 +
((__gen_e_acsl_v - -5) - 1))); ((__gen_e_acsl_v - -5) - 1)));
*/ */
/*@ assert
Value: mem_access:
\valid_read(__gen_e_acsl_at_3 +
(int)((int)((int)(__gen_e_acsl_u - 9) * 11) +
(int)((int)(__gen_e_acsl_v - -5) - 1)));
*/
if (*(__gen_e_acsl_at_3 + ((__gen_e_acsl_u - 9) * 11 + (( if (*(__gen_e_acsl_at_3 + ((__gen_e_acsl_u - 9) * 11 + ((
__gen_e_acsl_v - -5) - 1)))) __gen_e_acsl_v - -5) - 1))))
; ;
...@@ -393,11 +357,6 @@ int main(void) ...@@ -393,11 +357,6 @@ int main(void)
__gen_e_acsl_k_4 = -9 + 1; __gen_e_acsl_k_4 = -9 + 1;
while (1) { while (1) {
if (__gen_e_acsl_k_4 < 0) ; else break; if (__gen_e_acsl_k_4 < 0) ; else break;
/*@ assert
Value: mem_access:
\valid(__gen_e_acsl_at_5 +
(int)((int)(__gen_e_acsl_k_4 - -9) - 1));
*/
*(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_4 - -9) - 1)) = m + (long)__gen_e_acsl_k_4; *(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_4 - -9) - 1)) = m + (long)__gen_e_acsl_k_4;
__gen_e_acsl_k_4 ++; __gen_e_acsl_k_4 ++;
} }
...@@ -429,11 +388,6 @@ int main(void) ...@@ -429,11 +388,6 @@ int main(void)
Value: initialization: Value: initialization:
\initialized(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1)); \initialized(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1));
*/ */
/*@ assert
Value: mem_access:
\valid_read(__gen_e_acsl_at_5 +
(int)((int)(__gen_e_acsl_k_3 - -9) - 1));
*/
if (! (*(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1)) == 0L)) if (! (*(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1)) == 0L))
; ;
else { else {
...@@ -493,12 +447,6 @@ int main(void) ...@@ -493,12 +447,6 @@ int main(void)
((__gen_e_acsl_u_3 - 9) * 32 + ((__gen_e_acsl_u_3 - 9) * 32 +
((__gen_e_acsl_v_3 - -5) - 1))); ((__gen_e_acsl_v_3 - -5) - 1)));
*/ */
/*@ assert
Value: mem_access:
\valid_read(__gen_e_acsl_at_6 +
(int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32) +
(int)((int)(__gen_e_acsl_v_3 - -5) - 1)));
*/
if (*(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_3 - 9) * 32 + ( if (*(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_3 - 9) * 32 + (
(__gen_e_acsl_v_3 - -5) - 1)))) (__gen_e_acsl_v_3 - -5) - 1))))
; ;
...@@ -589,21 +537,6 @@ int main(void) ...@@ -589,21 +537,6 @@ int main(void)
(((__gen_e_acsl_v_5 - -10) - 1) * 100 + (((__gen_e_acsl_v_5 - -10) - 1) * 100 +
((__gen_e_acsl_w - 100) - 1)))); ((__gen_e_acsl_w - 100) - 1))));
*/ */
/*@ assert
Value: mem_access:
\valid_read(__gen_e_acsl_at_7 +
(int)((int)((int)(__gen_e_acsl_u_5 - 10) *
300)
+
(int)((int)((int)((int)(__gen_e_acsl_v_5
- -10)
- 1)
* 100)
+
(int)((int)(__gen_e_acsl_w -
100)
- 1))));
*/
if (! *(__gen_e_acsl_at_7 + ((__gen_e_acsl_u_5 - 10) * 300 + ( if (! *(__gen_e_acsl_at_7 + ((__gen_e_acsl_u_5 - 10) * 300 + (
((__gen_e_acsl_v_5 - -10) - 1) * 100 + ( ((__gen_e_acsl_v_5 - -10) - 1) * 100 + (
(__gen_e_acsl_w - 100) - 1))))) (__gen_e_acsl_w - 100) - 1)))))
...@@ -674,13 +607,11 @@ void __gen_e_acsl_f(int *t) ...@@ -674,13 +607,11 @@ void __gen_e_acsl_f(int *t)
{ {
int __gen_e_acsl_m_3; int __gen_e_acsl_m_3;
__gen_e_acsl_m_3 = 4; __gen_e_acsl_m_3 = 4;
/*@ assert Value: mem_access: \valid(__gen_e_acsl_at_4 + 0); */
*(__gen_e_acsl_at_4 + 0) = *(t + (__gen_e_acsl_m_3 - 4)); *(__gen_e_acsl_at_4 + 0) = *(t + (__gen_e_acsl_m_3 - 4));
} }
{ {
int __gen_e_acsl_m_2; int __gen_e_acsl_m_2;
__gen_e_acsl_m_2 = 4; __gen_e_acsl_m_2 = 4;
/*@ assert Value: mem_access: \valid(__gen_e_acsl_at_3 + 0); */
*(__gen_e_acsl_at_3 + 0) = *(t + __gen_e_acsl_m_2) == -4; *(__gen_e_acsl_at_3 + 0) = *(t + __gen_e_acsl_m_2) == -4;
} }
{ {
...@@ -688,10 +619,6 @@ void __gen_e_acsl_f(int *t) ...@@ -688,10 +619,6 @@ void __gen_e_acsl_f(int *t)
__gen_e_acsl_n_3 = 1 + 1; __gen_e_acsl_n_3 = 1 + 1;
while (1) { while (1) {
if (__gen_e_acsl_n_3 <= 3) ; else break; if (__gen_e_acsl_n_3 <= 3) ; else break;
/*@ assert
Value: mem_access:
\valid(__gen_e_acsl_at_2 + (int)((int)(__gen_e_acsl_n_3 - 1) - 1));
*/
*(__gen_e_acsl_at_2 + ((__gen_e_acsl_n_3 - 1) - 1)) = *(t + (__gen_e_acsl_n_3 - 1)) > 5; *(__gen_e_acsl_at_2 + ((__gen_e_acsl_n_3 - 1) - 1)) = *(t + (__gen_e_acsl_n_3 - 1)) > 5;
__gen_e_acsl_n_3 ++; __gen_e_acsl_n_3 ++;
} }
...@@ -701,10 +628,6 @@ void __gen_e_acsl_f(int *t) ...@@ -701,10 +628,6 @@ void __gen_e_acsl_f(int *t)
__gen_e_acsl_n_2 = 1 + 1; __gen_e_acsl_n_2 = 1 + 1;
while (1) { while (1) {
if (__gen_e_acsl_n_2 <= 3) ; else break; if (__gen_e_acsl_n_2 <= 3) ; else break;
/*@ assert
Value: mem_access:
\valid(__gen_e_acsl_at + (int)((int)(__gen_e_acsl_n_2 - 1) - 1));
*/
*(__gen_e_acsl_at + ((__gen_e_acsl_n_2 - 1) - 1)) = *(t + __gen_e_acsl_n_2) == 12; *(__gen_e_acsl_at + ((__gen_e_acsl_n_2 - 1) - 1)) = *(t + __gen_e_acsl_n_2) == 12;
__gen_e_acsl_n_2 ++; __gen_e_acsl_n_2 ++;
} }
...@@ -737,11 +660,6 @@ void __gen_e_acsl_f(int *t) ...@@ -737,11 +660,6 @@ void __gen_e_acsl_f(int *t)
Value: initialization: Value: initialization:
\initialized(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1)); \initialized(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1));
*/ */
/*@ assert
Value: mem_access:
\valid_read(__gen_e_acsl_at +
(int)((int)(__gen_e_acsl_n - 1) - 1));
*/
if (*(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1))) { if (*(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1))) {
int __gen_e_acsl_valid_read_2; int __gen_e_acsl_valid_read_2;
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_2 + (int)( __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(__gen_e_acsl_at_2 + (int)(
...@@ -758,11 +676,6 @@ void __gen_e_acsl_f(int *t) ...@@ -758,11 +676,6 @@ void __gen_e_acsl_f(int *t)
Value: initialization: Value: initialization:
\initialized(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1)); \initialized(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
*/ */
/*@ assert
Value: mem_access:
\valid_read(__gen_e_acsl_at_2 +
(int)((int)(__gen_e_acsl_n - 1) - 1));
*/
__gen_e_acsl_and = *(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1)); __gen_e_acsl_and = *(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
} }
else __gen_e_acsl_and = 0; else __gen_e_acsl_and = 0;
......
src/plugins/e-acsl/tests/gmp/test_config
+ 2
− 2
View file @ 01c1a8fd
LOG: gen_@PTEST_NAME@.c LOG: gen_@PTEST_NAME@.c
OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results -eva-no-alloc-returns-null
EXEC: ./scripts/testrun.sh @PTEST_NAME@ gmp "1" "--frama-c=@frama-c@" EXEC: ./scripts/testrun.sh @PTEST_NAME@ gmp "1" "--frama-c=@frama-c@"
LOG: gen_@PTEST_NAME@2.c LOG: gen_@PTEST_NAME@2.c
OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-gmp-only -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@2.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-gmp-only -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@2.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results -eva-no-alloc-returns-null
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment