Skip to content
Snippets Groups Projects
Commit 85e1595b authored by Julien Signoles's avatar Julien Signoles
Browse files

[e-acsl] - generated variable names are shortest 

	 - fixed bug when reusing variables in a different typing context
	 - fixed bug with boolean
	 - fixed bug with negation and GMP integers
	 - fixed bug with conditional and GMP integers
	 - fixed wrongly generated oracles
parent f6fe8507
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 2929 additions and 2618 deletions
src/plugins/e-acsl/tests/e-acsl-runtime/at.i
+ 1
− 1
View file @ 85e1595b
/* 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 -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_at.c > /dev/null && gcc -pedantic -Wno-long-long -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
EXECNOW: LOG gen_at2.c BIN gen_at2.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/arith.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_at2.c > /dev/null && gcc -pedantic -Wno-long-long -o ./tests/e-acsl-runtime/result/gen_at2.out ./tests/e-acsl-runtime/result/gen_at2.c -lgmp && ./tests/e-acsl-runtime/result/gen_at2.out
EXECNOW: LOG gen_at2.c BIN gen_at2.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/at.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_at2.c > /dev/null && gcc -pedantic -Wno-long-long -o ./tests/e-acsl-runtime/result/gen_at2.out ./tests/e-acsl-runtime/result/gen_at2.c -lgmp && ./tests/e-acsl-runtime/result/gen_at2.out
*/
int A = 0;
......
src/plugins/e-acsl/tests/e-acsl-runtime/function_contract.i
+ 1
− 1
View file @ 85e1595b
/* run.config
COMMENT: function contract
EXECNOW: LOG gen_function_contract.c BIN gen_function_contract.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/function_contract.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_function_contract.c > /dev/null && gcc -pedantic -Wno-long-long -o ./tests/e-acsl-runtime/result/gen_function_contract.out ./tests/e-acsl-runtime/result/gen_function_contract.c -lgmp && ./tests/e-acsl-runtime/result/gen_function_contract.out
EXECNOW: LOG gen_function_contract2.c BIN gen_function_contract2.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/arith.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_function_contract2.c > /dev/null && gcc -pedantic -Wno-long-long -o ./tests/e-acsl-runtime/result/gen_function_contract2.out ./tests/e-acsl-runtime/result/gen_function_contract2.c -lgmp && ./tests/e-acsl-runtime/result/gen_function_contract2.out
EXECNOW: LOG gen_function_contract2.c BIN gen_function_contract2.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/function_contract.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_function_contract2.c > /dev/null && gcc -pedantic -Wno-long-long -o ./tests/e-acsl-runtime/result/gen_function_contract2.out ./tests/e-acsl-runtime/result/gen_function_contract2.c -lgmp && ./tests/e-acsl-runtime/result/gen_function_contract2.out
*/
int X = 0, Y = 2;
......
src/plugins/e-acsl/tests/e-acsl-runtime/linear_search.i
+ 1
− 1
View file @ 85e1595b
/* 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
EXECNOW: LOG gen_linear_search2.c BIN gen_linear_search2.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/arith.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_linear_search2.c > /dev/null && gcc -pedantic -Wno-long-long -o ./tests/e-acsl-runtime/result/gen_linear_search2.out ./tests/e-acsl-runtime/result/gen_linear_search2.c -lgmp && ./tests/e-acsl-runtime/result/gen_linear_search2.out
EXECNOW: LOG gen_linear_search2.c BIN gen_linear_search2.out FRAMAC_SHARE=./share @frama-c@ ./tests/e-acsl-runtime/linear_search.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_linear_search2.c > /dev/null && gcc -pedantic -Wno-long-long -o ./tests/e-acsl-runtime/result/gen_linear_search2.out ./tests/e-acsl-runtime/result/gen_linear_search2.c -lgmp && ./tests/e-acsl-runtime/result/gen_linear_search2.out
*/
int A[10];
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
+ 18
− 18
View file @ 85e1595b
......@@ -163,53 +163,53 @@ int main(void)
(char *)"Assertion",(char *)"(x*3 == -9)",18);
/*@ assert x/3 ≡ -1; */ ;
{
int __e_acsl_var;
int __e_acsl;
/*@ assert 3 ≢ 0; */ ;
e_acsl_assert(! (3 == 0),(char *)"Assertion",(char *)"(3 == 0)",19);
__e_acsl_var = x / 3;
e_acsl_assert(__e_acsl_var == -1,(char *)"Assertion",
(char *)"(x/3 == -1)",19);
__e_acsl = x / 3;
e_acsl_assert(__e_acsl == -1,(char *)"Assertion",(char *)"(x/3 == -1)",
19);
}
/*@ assert 0xfffffffffff/0xfffffffffff ≡ 1; */ ;
{
int __e_acsl_var_2;
int __e_acsl_2;
/*@ assert 0xfffffffffff ≢ 0; */ ;
e_acsl_assert(! (0xfffffffffff == (long long)0),(char *)"Assertion",
(char *)"(0xfffffffffff == 0)",20);
__e_acsl_var_2 = (int)(0xfffffffffff / 0xfffffffffff);
e_acsl_assert(__e_acsl_var_2 == 1,(char *)"Assertion",
__e_acsl_2 = (int)(0xfffffffffff / 0xfffffffffff);
e_acsl_assert(__e_acsl_2 == 1,(char *)"Assertion",
(char *)"(0xfffffffffff/0xfffffffffff == 1)",20);
}
/*@ assert x%2 ≡ -1; */ ;
{
int __e_acsl_var_3;
int __e_acsl_3;
/*@ assert 2 ≢ 0; */ ;
e_acsl_assert(! (2 == 0),(char *)"Assertion",(char *)"(2 == 0)",21);
__e_acsl_var_3 = x % 2;
e_acsl_assert(__e_acsl_var_3 == -1,(char *)"Assertion",
(char *)"(x%2 == -1)",21);
__e_acsl_3 = x % 2;
e_acsl_assert(__e_acsl_3 == -1,(char *)"Assertion",(char *)"(x%2 == -1)",
21);
}
/*@ assert -3%-2 ≡ -1; */ ;
{
int __e_acsl_var_4;
int __e_acsl_4;
/*@ assert -2 ≢ 0; */ ;
e_acsl_assert(! (-2 == 0),(char *)"Assertion",(char *)"(-2 == 0)",22);
__e_acsl_var_4 = -3 % -2;
e_acsl_assert(__e_acsl_var_4 == -1,(char *)"Assertion",
__e_acsl_4 = -3 % -2;
e_acsl_assert(__e_acsl_4 == -1,(char *)"Assertion",
(char *)"(-3%-2 == -1)",22);
}
/*@ assert 3%-2 ≡ 1; */ ;
{
int __e_acsl_var_5;
int __e_acsl_5;
/*@ assert -2 ≢ 0; */ ;
e_acsl_assert(! (-2 == 0),(char *)"Assertion",(char *)"(-2 == 0)",23);
__e_acsl_var_5 = 3 % -2;
e_acsl_assert(__e_acsl_var_5 == 1,(char *)"Assertion",
(char *)"(3%-2 == 1)",23);
__e_acsl_5 = 3 % -2;
e_acsl_assert(__e_acsl_5 == 1,(char *)"Assertion",(char *)"(3%-2 == 1)",
23);
}
/*@ assert ((x*2+(3+y))-4)+(x-y) ≡ -10; */ ;
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
+ 20
− 20
View file @ 85e1595b
......@@ -126,32 +126,32 @@ int main(void)
/*@ assert T1[0] ≡ T2[0]; */ ;
{
mpz_t __e_acsl_var;
mpz_t __e_acsl_var_2;
int __e_acsl_var_3;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var),(long)T1[0]);
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var_2),(long)T2[0]);
__e_acsl_var_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_var),
(__mpz_struct const *)(__e_acsl_var_2));
e_acsl_assert(__e_acsl_var_3 == 0,(char *)"Assertion",
mpz_t __e_acsl;
mpz_t __e_acsl_2;
int __e_acsl_3;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl),(long)T1[0]);
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_2),(long)T2[0]);
__e_acsl_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl),
(__mpz_struct const *)(__e_acsl_2));
e_acsl_assert(__e_acsl_3 == 0,(char *)"Assertion",
(char *)"(T1[0] == T2[0])",14);
__gmpz_clear((__mpz_struct *)(__e_acsl_var));
__gmpz_clear((__mpz_struct *)(__e_acsl_var_2));
__gmpz_clear((__mpz_struct *)(__e_acsl));
__gmpz_clear((__mpz_struct *)(__e_acsl_2));
}
/*@ assert T1[1] ≢ T2[1]; */ ;
{
mpz_t __e_acsl_var_4;
mpz_t __e_acsl_var_5;
int __e_acsl_var_6;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var_4),(long)T1[1]);
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var_5),(long)T2[1]);
__e_acsl_var_6 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_var_4),
(__mpz_struct const *)(__e_acsl_var_5));
e_acsl_assert(__e_acsl_var_6 != 0,(char *)"Assertion",
mpz_t __e_acsl_4;
mpz_t __e_acsl_5;
int __e_acsl_6;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_4),(long)T1[1]);
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_5),(long)T2[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 *)"Assertion",
(char *)"(T1[1] != T2[1])",15);
__gmpz_clear((__mpz_struct *)(__e_acsl_var_4));
__gmpz_clear((__mpz_struct *)(__e_acsl_var_5));
__gmpz_clear((__mpz_struct *)(__e_acsl_4));
__gmpz_clear((__mpz_struct *)(__e_acsl_5));
}
__retres = 0;
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
+ 65
− 65
View file @ 85e1595b
......@@ -9,14 +9,14 @@ tests/e-acsl-runtime/at.i:34:[e-acsl] warning: missing guard for ensuring that p
[value] Initial state computed
[value] Values of globals at initialization
A ∈ {0}
PROJECT_FILE.i:311:[value] Assertion got status valid.
PROJECT_FILE.i:310:[value] Assertion got status valid.
[value] computing for function e_acsl_assert <- main.
Called from PROJECT_FILE.i:312.
Called from PROJECT_FILE.i:311.
PROJECT_FILE.i:221:[value] Function e_acsl_assert: precondition got status valid.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
[value] computing for function f <- main.
Called from PROJECT_FILE.i:316.
Called from PROJECT_FILE.i:315.
PROJECT_FILE.i:247:[value] Assertion got status valid.
[value] computing for function e_acsl_assert <- f <- main.
Called from PROJECT_FILE.i:248.
......@@ -38,37 +38,37 @@ PROJECT_FILE.i:257:[value] Assertion got status unknown.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
[value] computing for function e_acsl_assert <- f <- main.
Called from PROJECT_FILE.i:263.
Called from PROJECT_FILE.i:262.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
PROJECT_FILE.i:231:[value] Function f: postcondition got status valid.
[value] Recording results for f
[value] Done for function f
PROJECT_FILE.i:317:[value] Assertion got status unknown.
PROJECT_FILE.i:316:[value] Assertion got status unknown.
[value] computing for function e_acsl_assert <- main.
Called from PROJECT_FILE.i:318.
Called from PROJECT_FILE.i:317.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
PROJECT_FILE.i:320:[value] Assertion got status unknown.
PROJECT_FILE.i:319:[value] Assertion got status unknown.
[value] computing for function e_acsl_assert <- main.
Called from PROJECT_FILE.i:321.
Called from PROJECT_FILE.i:320.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
PROJECT_FILE.i:324:[value] Assertion got status unknown.
PROJECT_FILE.i:323:[value] Assertion got status unknown.
[value] computing for function e_acsl_assert <- main.
Called from PROJECT_FILE.i:325.
Called from PROJECT_FILE.i:324.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
[value] computing for function g <- main.
Called from PROJECT_FILE.i:328.
PROJECT_FILE.i:285:[value] Assertion got status unknown.
Called from PROJECT_FILE.i:327.
PROJECT_FILE.i:284:[value] Assertion got status unknown.
[value] computing for function e_acsl_assert <- g <- main.
Called from PROJECT_FILE.i:286.
Called from PROJECT_FILE.i:285.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
PROJECT_FILE.i:290:[value] Assertion got status unknown.
PROJECT_FILE.i:289:[value] Assertion got status unknown.
[value] computing for function e_acsl_assert <- g <- main.
Called from PROJECT_FILE.i:292.
Called from PROJECT_FILE.i:291.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
[value] Recording results for g
......@@ -79,18 +79,18 @@ PROJECT_FILE.i:290:[value] Assertion got status unknown.
[value] Values at end of function e_acsl_assert:
[value] Values at end of function f:
A ∈ {3}
__e_acsl_var ∈ {0}
__e_acsl_var_2 ∈ {1}
__e_acsl_var_3 ∈ {2}
__e_acsl_var_4 ∈ {0}
__e_acsl_var_5 ∈ {0}
__e_acsl_var_6 ∈ {3}
__e_acsl ∈ {0}
__e_acsl_2 ∈ {1}
__e_acsl_3 ∈ {2}
__e_acsl_4 ∈ {0}
__e_acsl_5 ∈ {0}
__e_acsl_6 ∈ {3}
[value] Values at end of function g:
A ∈ {4}
__e_acsl_var ∈ {0}
__e_acsl_var_2 ∈ {2}
__e_acsl_var_3 ∈ {0}
__e_acsl_var_4 ∈ {2}
__e_acsl ∈ {0}
__e_acsl_2 ∈ {2}
__e_acsl_3 ∈ {0}
__e_acsl_4 ∈ {2}
x ∈ {1}
t[0] ∈ {2}
[1] ∈ {3}
......@@ -100,9 +100,9 @@ PROJECT_FILE.i:290:[value] Assertion got status unknown.
x ∈ {1}
t[0] ∈ {2}
[1] ∈ {3}
__e_acsl_var ∈ {0}
__e_acsl_var_2 ∈ {1}
__e_acsl_var_3 ∈ {0}
__e_acsl ∈ {0}
__e_acsl_2 ∈ {1}
__e_acsl_3 ∈ {0}
/* Generated by Frama-C */
/*@ terminates \false;
ensures \false;
......@@ -125,61 +125,61 @@ int A = 0;
/*@ ensures \at(A,Post) ≡ 3; */
void f(void)
{
int __e_acsl_var;
int __e_acsl_var_2;
int __e_acsl_var_3;
int __e_acsl_var_4;
int __e_acsl_var_5;
int __e_acsl_var_6;
__e_acsl_var_4 = A;
__e_acsl_var = A;
int __e_acsl;
int __e_acsl_2;
int __e_acsl_3;
int __e_acsl_4;
int __e_acsl_5;
int __e_acsl_6;
__e_acsl_4 = A;
__e_acsl = A;
A = 1;
F: __e_acsl_var_5 = __e_acsl_var_4;
__e_acsl_var_2 = A;
F: __e_acsl_5 = __e_acsl_4;
__e_acsl_2 = A;
A = 2;
/*@ assert \at(A,Pre) ≡ 0; */ ;
e_acsl_assert(__e_acsl_var == 0,(char *)"Assertion",
e_acsl_assert(__e_acsl == 0,(char *)"Assertion",
(char *)"(\\at(A,Pre) == 0)",13);
/*@ assert \at(A,F) ≡ 1; */ ;
e_acsl_assert(__e_acsl_var_2 == 1,(char *)"Assertion",
e_acsl_assert(__e_acsl_2 == 1,(char *)"Assertion",
(char *)"(\\at(A,F) == 1)",14);
/*@ assert \at(A,Here) ≡ 2; */ ;
__e_acsl_var_3 = A;
e_acsl_assert(__e_acsl_var_3 == 2,(char *)"Assertion",
__e_acsl_3 = A;
e_acsl_assert(__e_acsl_3 == 2,(char *)"Assertion",
(char *)"(\\at(A,Here) == 2)",15);
/*@ assert \at(\at(A,Pre),F) ≡ 0; */ ;
e_acsl_assert(__e_acsl_var_5 == 0,(char *)"Assertion",
e_acsl_assert(__e_acsl_5 == 0,(char *)"Assertion",
(char *)"(\\at(\\at(A,Pre),F) == 0)",16);
A = 3;
__e_acsl_var_6 = A;
e_acsl_assert(__e_acsl_var_6 == 3,(char *)"Postcondition",
__e_acsl_6 = A;
e_acsl_assert(__e_acsl_6 == 3,(char *)"Postcondition",
(char *)"(\\at(A,Post) == 3)",9);
return;
}
void g(int *p, int *q)
{
int __e_acsl_var;
int __e_acsl_var_2;
int __e_acsl_var_3;
int __e_acsl_var_4;
int __e_acsl;
int __e_acsl_2;
int __e_acsl_3;
int __e_acsl_4;
*p = 0;
*(p + 1) = 1;
*q = 0;
L1: __e_acsl_var_3 = *q;
__e_acsl_var = *q;
L1: __e_acsl_3 = *q;
__e_acsl = *q;
*p = 2;
*(p + 1) = 3;
*q = 1;
L2: __e_acsl_var_2 = *(p + __e_acsl_var);
L2: __e_acsl_2 = *(p + __e_acsl);
A = 4;
/*@ assert \at(*(p+\at(*q,L1)),L2) ≡ 2; */ ;
e_acsl_assert(__e_acsl_var_2 == 2,(char *)"Assertion",
e_acsl_assert(__e_acsl_2 == 2,(char *)"Assertion",
(char *)"(\\at(*(p+\\at(*q,L1)),L2) == 2)",32);
L3:
/*@ assert \at(*(p+\at(*q,L1)),Here) ≡ 2; */ ;
__e_acsl_var_4 = *(p + __e_acsl_var_3);
e_acsl_assert(__e_acsl_var_4 == 2,(char *)"Assertion",
__e_acsl_4 = *(p + __e_acsl_3);
e_acsl_assert(__e_acsl_4 == 2,(char *)"Assertion",
(char *)"(\\at(*(p+\\at(*q,L1)),Here) == 2)",34);
return;
}
......@@ -189,26 +189,26 @@ int main(void)
int __retres;
int x;
int t[2];
int __e_acsl_var;
long long __e_acsl_var_2;
int __e_acsl_var_3;
int __e_acsl;
long long __e_acsl_2;
int __e_acsl_3;
x = 0;
L: __e_acsl_var_3 = x;
__e_acsl_var_2 = (long long)x + (long long)1;
__e_acsl_var = x;
L: __e_acsl_3 = x;
__e_acsl_2 = (long long)x + (long long)1;
__e_acsl = x;
/*@ assert x ≡ 0; */ ;
e_acsl_assert(x == 0,(char *)"Assertion",(char *)"(x == 0)",45);
x = 1;
x = 2;
f();
/*@ assert \at(x,L) ≡ 0; */ ;
e_acsl_assert(__e_acsl_var == 0,(char *)"Assertion",
(char *)"(\\at(x,L) == 0)",50);
e_acsl_assert(__e_acsl == 0,(char *)"Assertion",(char *)"(\\at(x,L) == 0)",
50);
/*@ assert \at(x+1,L) ≡ 1; */ ;
e_acsl_assert(__e_acsl_var_2 == (long long)1,(char *)"Assertion",
e_acsl_assert(__e_acsl_2 == (long long)1,(char *)"Assertion",
(char *)"(\\at(x+1,L) == 1)",51);
/*@ assert \at(x,L)+1 ≡ 1; */ ;
e_acsl_assert((long long)__e_acsl_var_3 + (long long)1 == (long long)1,
e_acsl_assert((long long)__e_acsl_3 + (long long)1 == (long long)1,
(char *)"Assertion",(char *)"(\\at(x,L)+1 == 1)",52);
g(t,& x);
__retres = 0;
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
+ 74
− 74
View file @ 85e1595b
......@@ -215,110 +215,110 @@ int main(void)
y = 0;
/*@ assert (int)x ≡ y; */ ;
{
mpz_t __e_acsl_var;
mpz_t __e_acsl_var_2;
int __e_acsl_var_3;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var),(long)((int)x));
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var_2),(long)y);
__e_acsl_var_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_var),
(__mpz_struct const *)(__e_acsl_var_2));
e_acsl_assert(__e_acsl_var_3 == 0,(char *)"Assertion",
mpz_t __e_acsl;
mpz_t __e_acsl_2;
int __e_acsl_3;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl),(long)((int)x));
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_2),(long)y);
__e_acsl_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl),
(__mpz_struct const *)(__e_acsl_2));
e_acsl_assert(__e_acsl_3 == 0,(char *)"Assertion",
(char *)"((int)x == y)",11);
__gmpz_clear((__mpz_struct *)(__e_acsl_var));
__gmpz_clear((__mpz_struct *)(__e_acsl_var_2));
__gmpz_clear((__mpz_struct *)(__e_acsl));
__gmpz_clear((__mpz_struct *)(__e_acsl_2));
}
/*@ assert x ≡ (long)y; */ ;
{
mpz_t __e_acsl_var_4;
mpz_t __e_acsl_var_5;
int __e_acsl_var_6;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var_4),x);
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var_5),(long)y);
__e_acsl_var_6 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_var_4),
(__mpz_struct const *)(__e_acsl_var_5));
e_acsl_assert(__e_acsl_var_6 == 0,(char *)"Assertion",
mpz_t __e_acsl_4;
mpz_t __e_acsl_5;
int __e_acsl_6;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_4),x);
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_5),(long)y);
__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 *)"(x == (long)y)",12);
__gmpz_clear((__mpz_struct *)(__e_acsl_var_4));
__gmpz_clear((__mpz_struct *)(__e_acsl_var_5));
__gmpz_clear((__mpz_struct *)(__e_acsl_4));
__gmpz_clear((__mpz_struct *)(__e_acsl_5));
}
/*@ assert y ≡ (int)0; */ ;
{
mpz_t __e_acsl_var_7;
mpz_t __e_acsl_var_8;
int __e_acsl_var_9;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var_7),(long)y);
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var_8),(long)0);
__e_acsl_var_9 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_var_7),
(__mpz_struct const *)(__e_acsl_var_8));
e_acsl_assert(__e_acsl_var_9 == 0,(char *)"Assertion",
mpz_t __e_acsl_7;
mpz_t __e_acsl_8;
int __e_acsl_9;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_7),(long)y);
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_8),(long)0);
__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 *)"Assertion",
(char *)"(y == (int)0)",14);
__gmpz_clear((__mpz_struct *)(__e_acsl_var_7));
__gmpz_clear((__mpz_struct *)(__e_acsl_var_8));
__gmpz_clear((__mpz_struct *)(__e_acsl_7));
__gmpz_clear((__mpz_struct *)(__e_acsl_8));
}
/*@ assert (unsigned int)y ≡ (unsigned int)0; */ ;
{
mpz_t __e_acsl_var_10;
mpz_t __e_acsl_var_11;
int __e_acsl_var_12;
__gmpz_init_set_ui((__mpz_struct *)(__e_acsl_var_10),
mpz_t __e_acsl_10;
mpz_t __e_acsl_11;
int __e_acsl_12;
__gmpz_init_set_ui((__mpz_struct *)(__e_acsl_10),
(unsigned long)((unsigned int)y));
__gmpz_init_set_ui((__mpz_struct *)(__e_acsl_var_11),
__gmpz_init_set_ui((__mpz_struct *)(__e_acsl_11),
(unsigned long)((unsigned int)0));
__e_acsl_var_12 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_var_10),
(__mpz_struct const *)(__e_acsl_var_11));
e_acsl_assert(__e_acsl_var_12 == 0,(char *)"Assertion",
__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 *)"Assertion",
(char *)"((unsigned int)y == (unsigned int)0)",15);
__gmpz_clear((__mpz_struct *)(__e_acsl_var_10));
__gmpz_clear((__mpz_struct *)(__e_acsl_var_11));
__gmpz_clear((__mpz_struct *)(__e_acsl_10));
__gmpz_clear((__mpz_struct *)(__e_acsl_11));
}
/*@ assert y ≢ (int)0xfffffffffffffff; */ ;
{
mpz_t __e_acsl_var_13;
mpz_t __e_acsl_var_14;
unsigned long __e_acsl_var_15;
mpz_t __e_acsl_var_16;
int __e_acsl_var_17;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var_13),(long)y);
__gmpz_init_set_str((__mpz_struct *)(__e_acsl_var_14),
"1152921504606846975",10);
__e_acsl_var_15 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_var_14));
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var_16),
(long)((int)__e_acsl_var_15));
__e_acsl_var_17 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_var_13),
(__mpz_struct const *)(__e_acsl_var_16));
e_acsl_assert(__e_acsl_var_17 != 0,(char *)"Assertion",
mpz_t __e_acsl_13;
mpz_t __e_acsl_14;
unsigned long __e_acsl_15;
mpz_t __e_acsl_16;
int __e_acsl_17;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_13),(long)y);
__gmpz_init_set_str((__mpz_struct *)(__e_acsl_14),"1152921504606846975",
10);
__e_acsl_15 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_14));
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_16),
(long)((int)__e_acsl_15));
__e_acsl_17 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_13),
(__mpz_struct const *)(__e_acsl_16));
e_acsl_assert(__e_acsl_17 != 0,(char *)"Assertion",
(char *)"(y != (int)0xfffffffffffffff)",18);
__gmpz_clear((__mpz_struct *)(__e_acsl_var_13));
__gmpz_clear((__mpz_struct *)(__e_acsl_var_14));
__gmpz_clear((__mpz_struct *)(__e_acsl_var_16));
__gmpz_clear((__mpz_struct *)(__e_acsl_13));
__gmpz_clear((__mpz_struct *)(__e_acsl_14));
__gmpz_clear((__mpz_struct *)(__e_acsl_16));
}
/*@ assert (unsigned int)y ≢ (unsigned int)0xfffffffffffffff; */ ;
{
mpz_t __e_acsl_var_18;
mpz_t __e_acsl_var_19;
unsigned long __e_acsl_var_20;
mpz_t __e_acsl_var_21;
int __e_acsl_var_22;
__gmpz_init_set_ui((__mpz_struct *)(__e_acsl_var_18),
mpz_t __e_acsl_18;
mpz_t __e_acsl_19;
unsigned long __e_acsl_20;
mpz_t __e_acsl_21;
int __e_acsl_22;
__gmpz_init_set_ui((__mpz_struct *)(__e_acsl_18),
(unsigned long)((unsigned int)y));
__gmpz_init_set_str((__mpz_struct *)(__e_acsl_var_19),
"1152921504606846975",10);
__e_acsl_var_20 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_var_19));
__gmpz_init_set_ui((__mpz_struct *)(__e_acsl_var_21),
(unsigned long)((unsigned int)__e_acsl_var_20));
__e_acsl_var_22 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_var_18),
(__mpz_struct const *)(__e_acsl_var_21));
e_acsl_assert(__e_acsl_var_22 != 0,(char *)"Assertion",
__gmpz_init_set_str((__mpz_struct *)(__e_acsl_19),"1152921504606846975",
10);
__e_acsl_20 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_19));
__gmpz_init_set_ui((__mpz_struct *)(__e_acsl_21),
(unsigned long)((unsigned int)__e_acsl_20));
__e_acsl_22 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_18),
(__mpz_struct const *)(__e_acsl_21));
e_acsl_assert(__e_acsl_22 != 0,(char *)"Assertion",
(char *)"((unsigned int)y != (unsigned int)0xfffffffffffffff)",
19);
__gmpz_clear((__mpz_struct *)(__e_acsl_var_18));
__gmpz_clear((__mpz_struct *)(__e_acsl_var_19));
__gmpz_clear((__mpz_struct *)(__e_acsl_var_21));
__gmpz_clear((__mpz_struct *)(__e_acsl_18));
__gmpz_clear((__mpz_struct *)(__e_acsl_19));
__gmpz_clear((__mpz_struct *)(__e_acsl_21));
}
__retres = 0;
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
+ 57
− 58
View file @ 85e1595b
......@@ -5,7 +5,7 @@
X ∈ {0}
Y ∈ {2}
[value] computing for function f <- main.
Called from PROJECT_FILE.i:402.
Called from PROJECT_FILE.i:401.
[value] computing for function e_acsl_assert <- f <- main.
Called from PROJECT_FILE.i:236.
PROJECT_FILE.i:221:[value] Function e_acsl_assert: precondition got status valid.
......@@ -15,7 +15,7 @@ PROJECT_FILE.i:232:[value] Function f: postcondition got status valid.
[value] Recording results for f
[value] Done for function f
[value] computing for function g <- main.
Called from PROJECT_FILE.i:403.
Called from PROJECT_FILE.i:402.
[value] computing for function e_acsl_assert <- g <- main.
Called from PROJECT_FILE.i:245.
[value] Recording results for e_acsl_assert
......@@ -29,7 +29,7 @@ PROJECT_FILE.i:241:[value] Function g: postcondition got status valid.
[value] Recording results for g
[value] Done for function g
[value] computing for function h <- main.
Called from PROJECT_FILE.i:404.
Called from PROJECT_FILE.i:403.
PROJECT_FILE.i:250:[value] Function h: precondition got status valid.
[value] computing for function e_acsl_assert <- h <- main.
Called from PROJECT_FILE.i:253.
......@@ -38,7 +38,7 @@ PROJECT_FILE.i:250:[value] Function h: precondition got status valid.
[value] Recording results for h
[value] Done for function h
[value] computing for function i <- main.
Called from PROJECT_FILE.i:405.
Called from PROJECT_FILE.i:404.
PROJECT_FILE.i:258:[value] Function i: precondition got status valid.
PROJECT_FILE.i:259:[value] Function i: precondition got status valid.
[value] computing for function e_acsl_assert <- i <- main.
......@@ -52,7 +52,7 @@ PROJECT_FILE.i:259:[value] Function i: precondition got status valid.
[value] Recording results for i
[value] Done for function i
[value] computing for function j <- main.
Called from PROJECT_FILE.i:406.
Called from PROJECT_FILE.i:405.
PROJECT_FILE.i:269:[value] Function j, behavior b1: precondition got status valid.
PROJECT_FILE.i:273:[value] Function j, behavior b2: precondition got status valid.
PROJECT_FILE.i:274:[value] Function j, behavior b2: precondition got status valid.
......@@ -81,7 +81,7 @@ PROJECT_FILE.i:275:[value] Function j, behavior b2: postcondition got status val
[value] Recording results for j
[value] Done for function j
[value] computing for function k <- main.
Called from PROJECT_FILE.i:407.
Called from PROJECT_FILE.i:406.
PROJECT_FILE.i:294:[value] Function k, behavior b1: assumption got status invalid; precondition not evaluated.
PROJECT_FILE.i:299:[value] Function k, behavior b2: precondition got status valid.
PROJECT_FILE.i:300:[value] Function k, behavior b2: precondition got status valid.
......@@ -100,7 +100,7 @@ PROJECT_FILE.i:300:[value] Function k, behavior b2: precondition got status vali
[value] Recording results for k
[value] Done for function k
[value] computing for function l <- main.
Called from PROJECT_FILE.i:408.
Called from PROJECT_FILE.i:407.
PROJECT_FILE.i:336:[value] Assertion got status valid.
[value] computing for function e_acsl_assert <- l <- main.
Called from PROJECT_FILE.i:337.
......@@ -114,7 +114,7 @@ PROJECT_FILE.i:333:[value] Function l: postcondition got status valid.
[value] Recording results for l
[value] Done for function l
[value] computing for function m <- main.
Called from PROJECT_FILE.i:409.
Called from PROJECT_FILE.i:408.
[value] computing for function e_acsl_assert <- m <- main.
Called from PROJECT_FILE.i:382.
[value] Recording results for e_acsl_assert
......@@ -124,7 +124,7 @@ PROJECT_FILE.i:333:[value] Function l: postcondition got status valid.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
[value] computing for function e_acsl_assert <- m <- main.
Called from PROJECT_FILE.i:392.
Called from PROJECT_FILE.i:391.
[value] Recording results for e_acsl_assert
[value] Done for function e_acsl_assert
PROJECT_FILE.i:345:[value] Function m, behavior b1: assumes got status invalid; post-condition not evaluated.
......@@ -151,10 +151,10 @@ PROJECT_FILE.i:351:[value] Function m, behavior b2: postcondition got status val
[value] Values at end of function l:
[value] Values at end of function m:
X ∈ {7}
__e_acsl_var ∈ {0}
__e_acsl_var_4 ∈ {1}
__e_acsl_var_7 ∈ {1}
__e_acsl_var_8 ∈ {5}
__e_acsl ∈ {0}
__e_acsl_4 ∈ {1}
__e_acsl_7 ∈ {1}
__e_acsl_8 ∈ {5}
[value] Values at end of function main:
X ∈ {7}
__retres ∈ {0}
......@@ -253,26 +253,26 @@ void j(void)
void k(void)
{
{
int __e_acsl_var;
int __e_acsl_var_2;
int __e_acsl_var_3;
int __e_acsl_var_4;
int __e_acsl_var_5;
if (! (X == 1)) { __e_acsl_var = 1; }
else { __e_acsl_var = X == 0; }
e_acsl_assert(__e_acsl_var,(char *)"Precondition",
int __e_acsl;
int __e_acsl_2;
int __e_acsl_3;
int __e_acsl_4;
int __e_acsl_5;
if (! (X == 1)) { __e_acsl = 1; }
else { __e_acsl = X == 0; }
e_acsl_assert(__e_acsl,(char *)"Precondition",
(char *)"(X == 1 ==> X == 0)",40);
if (X == 3) { __e_acsl_var_2 = Y == 2; }
else { __e_acsl_var_2 = 0; }
if (! __e_acsl_var_2) { __e_acsl_var_3 = 1; }
else { __e_acsl_var_3 = X == 3; }
e_acsl_assert(__e_acsl_var_3,(char *)"Precondition",
if (X == 3) { __e_acsl_2 = Y == 2; }
else { __e_acsl_2 = 0; }
if (! __e_acsl_2) { __e_acsl_3 = 1; }
else { __e_acsl_3 = X == 3; }
e_acsl_assert(__e_acsl_3,(char *)"Precondition",
(char *)"(X == 3 && Y == 2 ==> X == 3)",44);
if (X == 3) { __e_acsl_var_4 = Y == 2; }
else { __e_acsl_var_4 = 0; }
if (! __e_acsl_var_4) { __e_acsl_var_5 = 1; }
else { __e_acsl_var_5 = (long long)X + (long long)Y == (long long)5; }
e_acsl_assert(__e_acsl_var_5,(char *)"Precondition",
if (X == 3) { __e_acsl_4 = Y == 2; }
else { __e_acsl_4 = 0; }
if (! __e_acsl_4) { __e_acsl_5 = 1; }
else { __e_acsl_5 = (long long)X + (long long)Y == (long long)5; }
e_acsl_assert(__e_acsl_5,(char *)"Precondition",
(char *)"(X == 3 && Y == 2 ==> X+Y == 5)",45);
X += Y;
}
......@@ -303,42 +303,41 @@ int l(void)
*/
void m(void)
{
int __e_acsl_var;
int __e_acsl_var_4;
int __e_acsl_var_7;
int __e_acsl_var_8;
__e_acsl_var_8 = X;
{ int __e_acsl_var_6;
if (X == 5) { __e_acsl_var_6 = Y == 2; }
else { __e_acsl_var_6 = 0; }
__e_acsl_var_7 = __e_acsl_var_6;
int __e_acsl;
int __e_acsl_4;
int __e_acsl_7;
int __e_acsl_8;
__e_acsl_8 = X;
{ int __e_acsl_6;
if (X == 5) { __e_acsl_6 = Y == 2; }
else { __e_acsl_6 = 0; }
__e_acsl_7 = __e_acsl_6;
}
{ int __e_acsl_var_3;
if (X == 5) { __e_acsl_var_3 = Y == 2; }
else { __e_acsl_var_3 = 0; }
__e_acsl_var_4 = __e_acsl_var_3;
{ int __e_acsl_3;
if (X == 5) { __e_acsl_3 = Y == 2; }
else { __e_acsl_3 = 0; }
__e_acsl_4 = __e_acsl_3;
}
__e_acsl_var = X == 7;
__e_acsl = X == 7;
X += Y;
{
int __e_acsl_var_2;
int __e_acsl_var_5;
int __e_acsl_var_9;
if (! __e_acsl_var) { __e_acsl_var_2 = 1; }
else { __e_acsl_var_2 = X == 95; }
e_acsl_assert(__e_acsl_var_2,(char *)"Postcondition",
int __e_acsl_2;
int __e_acsl_5;
int __e_acsl_9;
if (! __e_acsl) { __e_acsl_2 = 1; }
else { __e_acsl_2 = X == 95; }
e_acsl_assert(__e_acsl_2,(char *)"Postcondition",
(char *)"(\\old(X == 7) ==> X == 95)",58);
if (! __e_acsl_var_4) { __e_acsl_var_5 = 1; }
else { __e_acsl_var_5 = X == 7; }
e_acsl_assert(__e_acsl_var_5,(char *)"Postcondition",
if (! __e_acsl_4) { __e_acsl_5 = 1; }
else { __e_acsl_5 = X == 7; }
e_acsl_assert(__e_acsl_5,(char *)"Postcondition",
(char *)"(\\old(X == 5 && Y == 2) ==> X == 7)",62);
if (! __e_acsl_var_7) { __e_acsl_var_9 = 1; }
else {
__e_acsl_var_9 = (long long)X == (long long)__e_acsl_var_8 + (long long)Y;
if (! __e_acsl_7) { __e_acsl_9 = 1; }
else { __e_acsl_9 = (long long)X == (long long)__e_acsl_8 + (long long)Y;
}
e_acsl_assert(__e_acsl_var_9,(char *)"Postcondition",
e_acsl_assert(__e_acsl_9,(char *)"Postcondition",
(char *)"(\\old(X == 5 && Y == 2) ==> X == \\old(X)+Y)",63);
return;
}
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
+ 18
− 18
View file @ 85e1595b
......@@ -40,53 +40,53 @@ int main(void)
(char *)"Assertion",(char *)"(x*3 == -9)",18);
/*@ assert x/3 ≡ -1; */ ;
{
int __e_acsl_var;
int __e_acsl;
/*@ assert 3 ≢ 0; */ ;
e_acsl_assert(! (3 == 0),(char *)"Assertion",(char *)"(3 == 0)",19);
__e_acsl_var = x / 3;
e_acsl_assert(__e_acsl_var == -1,(char *)"Assertion",
(char *)"(x/3 == -1)",19);
__e_acsl = x / 3;
e_acsl_assert(__e_acsl == -1,(char *)"Assertion",(char *)"(x/3 == -1)",
19);
}
/*@ assert 0xfffffffffff/0xfffffffffff ≡ 1; */ ;
{
int __e_acsl_var_2;
int __e_acsl_2;
/*@ assert 0xfffffffffff ≢ 0; */ ;
e_acsl_assert(! (0xfffffffffff == (long long)0),(char *)"Assertion",
(char *)"(0xfffffffffff == 0)",20);
__e_acsl_var_2 = (int)(0xfffffffffff / 0xfffffffffff);
e_acsl_assert(__e_acsl_var_2 == 1,(char *)"Assertion",
__e_acsl_2 = (int)(0xfffffffffff / 0xfffffffffff);
e_acsl_assert(__e_acsl_2 == 1,(char *)"Assertion",
(char *)"(0xfffffffffff/0xfffffffffff == 1)",20);
}
/*@ assert x%2 ≡ -1; */ ;
{
int __e_acsl_var_3;
int __e_acsl_3;
/*@ assert 2 ≢ 0; */ ;
e_acsl_assert(! (2 == 0),(char *)"Assertion",(char *)"(2 == 0)",21);
__e_acsl_var_3 = x % 2;
e_acsl_assert(__e_acsl_var_3 == -1,(char *)"Assertion",
(char *)"(x%2 == -1)",21);
__e_acsl_3 = x % 2;
e_acsl_assert(__e_acsl_3 == -1,(char *)"Assertion",(char *)"(x%2 == -1)",
21);
}
/*@ assert -3%-2 ≡ -1; */ ;
{
int __e_acsl_var_4;
int __e_acsl_4;
/*@ assert -2 ≢ 0; */ ;
e_acsl_assert(! (-2 == 0),(char *)"Assertion",(char *)"(-2 == 0)",22);
__e_acsl_var_4 = -3 % -2;
e_acsl_assert(__e_acsl_var_4 == -1,(char *)"Assertion",
__e_acsl_4 = -3 % -2;
e_acsl_assert(__e_acsl_4 == -1,(char *)"Assertion",
(char *)"(-3%-2 == -1)",22);
}
/*@ assert 3%-2 ≡ 1; */ ;
{
int __e_acsl_var_5;
int __e_acsl_5;
/*@ assert -2 ≢ 0; */ ;
e_acsl_assert(! (-2 == 0),(char *)"Assertion",(char *)"(-2 == 0)",23);
__e_acsl_var_5 = 3 % -2;
e_acsl_assert(__e_acsl_var_5 == 1,(char *)"Assertion",
(char *)"(3%-2 == 1)",23);
__e_acsl_5 = 3 % -2;
e_acsl_assert(__e_acsl_5 == 1,(char *)"Assertion",(char *)"(3%-2 == 1)",
23);
}
/*@ assert ((x*2+(3+y))-4)+(x-y) ≡ -10; */ ;
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c
+ 510
− 344
View file @ 85e1595b
This diff is collapsed.
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c
+ 20
− 20
View file @ 85e1595b
......@@ -58,32 +58,32 @@ int main(void)
/*@ assert T1[0] ≡ T2[0]; */ ;
{
mpz_t __e_acsl_var;
mpz_t __e_acsl_var_2;
int __e_acsl_var_3;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var),(long)T1[0]);
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var_2),(long)T2[0]);
__e_acsl_var_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_var),
(__mpz_struct const *)(__e_acsl_var_2));
e_acsl_assert(__e_acsl_var_3 == 0,(char *)"Assertion",
mpz_t __e_acsl;
mpz_t __e_acsl_2;
int __e_acsl_3;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl),(long)T1[0]);
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_2),(long)T2[0]);
__e_acsl_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl),
(__mpz_struct const *)(__e_acsl_2));
e_acsl_assert(__e_acsl_3 == 0,(char *)"Assertion",
(char *)"(T1[0] == T2[0])",14);
__gmpz_clear((__mpz_struct *)(__e_acsl_var));
__gmpz_clear((__mpz_struct *)(__e_acsl_var_2));
__gmpz_clear((__mpz_struct *)(__e_acsl));
__gmpz_clear((__mpz_struct *)(__e_acsl_2));
}
/*@ assert T1[1] ≢ T2[1]; */ ;
{
mpz_t __e_acsl_var_4;
mpz_t __e_acsl_var_5;
int __e_acsl_var_6;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var_4),(long)T1[1]);
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var_5),(long)T2[1]);
__e_acsl_var_6 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_var_4),
(__mpz_struct const *)(__e_acsl_var_5));
e_acsl_assert(__e_acsl_var_6 != 0,(char *)"Assertion",
mpz_t __e_acsl_4;
mpz_t __e_acsl_5;
int __e_acsl_6;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_4),(long)T1[1]);
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_5),(long)T2[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 *)"Assertion",
(char *)"(T1[1] != T2[1])",15);
__gmpz_clear((__mpz_struct *)(__e_acsl_var_4));
__gmpz_clear((__mpz_struct *)(__e_acsl_var_5));
__gmpz_clear((__mpz_struct *)(__e_acsl_4));
__gmpz_clear((__mpz_struct *)(__e_acsl_5));
}
__retres = 0;
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
+ 37
− 37
View file @ 85e1595b
......@@ -20,61 +20,61 @@ int A = 0;
/*@ ensures \at(A,Post) ≡ 3; */
void f(void)
{
int __e_acsl_var;
int __e_acsl_var_2;
int __e_acsl_var_3;
int __e_acsl_var_4;
int __e_acsl_var_5;
int __e_acsl_var_6;
__e_acsl_var_4 = A;
__e_acsl_var = A;
int __e_acsl;
int __e_acsl_2;
int __e_acsl_3;
int __e_acsl_4;
int __e_acsl_5;
int __e_acsl_6;
__e_acsl_4 = A;
__e_acsl = A;
A = 1;
F: __e_acsl_var_5 = __e_acsl_var_4;
__e_acsl_var_2 = A;
F: __e_acsl_5 = __e_acsl_4;
__e_acsl_2 = A;
A = 2;
/*@ assert \at(A,Pre) ≡ 0; */ ;
e_acsl_assert(__e_acsl_var == 0,(char *)"Assertion",
e_acsl_assert(__e_acsl == 0,(char *)"Assertion",
(char *)"(\\at(A,Pre) == 0)",13);
/*@ assert \at(A,F) ≡ 1; */ ;
e_acsl_assert(__e_acsl_var_2 == 1,(char *)"Assertion",
e_acsl_assert(__e_acsl_2 == 1,(char *)"Assertion",
(char *)"(\\at(A,F) == 1)",14);
/*@ assert \at(A,Here) ≡ 2; */ ;
__e_acsl_var_3 = A;
e_acsl_assert(__e_acsl_var_3 == 2,(char *)"Assertion",
__e_acsl_3 = A;
e_acsl_assert(__e_acsl_3 == 2,(char *)"Assertion",
(char *)"(\\at(A,Here) == 2)",15);
/*@ assert \at(\at(A,Pre),F) ≡ 0; */ ;
e_acsl_assert(__e_acsl_var_5 == 0,(char *)"Assertion",
e_acsl_assert(__e_acsl_5 == 0,(char *)"Assertion",
(char *)"(\\at(\\at(A,Pre),F) == 0)",16);
A = 3;
__e_acsl_var_6 = A;
e_acsl_assert(__e_acsl_var_6 == 3,(char *)"Postcondition",
__e_acsl_6 = A;
e_acsl_assert(__e_acsl_6 == 3,(char *)"Postcondition",
(char *)"(\\at(A,Post) == 3)",9);
return;
}
void g(int *p, int *q)
{
int __e_acsl_var;
int __e_acsl_var_2;
int __e_acsl_var_3;
int __e_acsl_var_4;
int __e_acsl;
int __e_acsl_2;
int __e_acsl_3;
int __e_acsl_4;
*p = 0;
*(p + 1) = 1;
*q = 0;
L1: __e_acsl_var_3 = *q;
__e_acsl_var = *q;
L1: __e_acsl_3 = *q;
__e_acsl = *q;
*p = 2;
*(p + 1) = 3;
*q = 1;
L2: __e_acsl_var_2 = *(p + __e_acsl_var);
L2: __e_acsl_2 = *(p + __e_acsl);
A = 4;
/*@ assert \at(*(p+\at(*q,L1)),L2) ≡ 2; */ ;
e_acsl_assert(__e_acsl_var_2 == 2,(char *)"Assertion",
e_acsl_assert(__e_acsl_2 == 2,(char *)"Assertion",
(char *)"(\\at(*(p+\\at(*q,L1)),L2) == 2)",32);
L3:
/*@ assert \at(*(p+\at(*q,L1)),Here) ≡ 2; */ ;
__e_acsl_var_4 = *(p + __e_acsl_var_3);
e_acsl_assert(__e_acsl_var_4 == 2,(char *)"Assertion",
__e_acsl_4 = *(p + __e_acsl_3);
e_acsl_assert(__e_acsl_4 == 2,(char *)"Assertion",
(char *)"(\\at(*(p+\\at(*q,L1)),Here) == 2)",34);
return;
}
......@@ -84,26 +84,26 @@ int main(void)
int __retres;
int x;
int t[2];
int __e_acsl_var;
long long __e_acsl_var_2;
int __e_acsl_var_3;
int __e_acsl;
long long __e_acsl_2;
int __e_acsl_3;
x = 0;
L: __e_acsl_var_3 = x;
__e_acsl_var_2 = (long long)x + (long long)1;
__e_acsl_var = x;
L: __e_acsl_3 = x;
__e_acsl_2 = (long long)x + (long long)1;
__e_acsl = x;
/*@ assert x ≡ 0; */ ;
e_acsl_assert(x == 0,(char *)"Assertion",(char *)"(x == 0)",45);
x = 1;
x = 2;
f();
/*@ assert \at(x,L) ≡ 0; */ ;
e_acsl_assert(__e_acsl_var == 0,(char *)"Assertion",
(char *)"(\\at(x,L) == 0)",50);
e_acsl_assert(__e_acsl == 0,(char *)"Assertion",(char *)"(\\at(x,L) == 0)",
50);
/*@ assert \at(x+1,L) ≡ 1; */ ;
e_acsl_assert(__e_acsl_var_2 == (long long)1,(char *)"Assertion",
e_acsl_assert(__e_acsl_2 == (long long)1,(char *)"Assertion",
(char *)"(\\at(x+1,L) == 1)",51);
/*@ assert \at(x,L)+1 ≡ 1; */ ;
e_acsl_assert((long long)__e_acsl_var_3 + (long long)1 == (long long)1,
e_acsl_assert((long long)__e_acsl_3 + (long long)1 == (long long)1,
(char *)"Assertion",(char *)"(\\at(x,L)+1 == 1)",52);
g(t,& x);
__retres = 0;
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
+ 210
− 426
View file @ 85e1595b
This diff is collapsed.
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c
+ 74
− 74
View file @ 85e1595b
......@@ -55,110 +55,110 @@ int main(void)
y = 0;
/*@ assert (int)x ≡ y; */ ;
{
mpz_t __e_acsl_var;
mpz_t __e_acsl_var_2;
int __e_acsl_var_3;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var),(long)((int)x));
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var_2),(long)y);
__e_acsl_var_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_var),
(__mpz_struct const *)(__e_acsl_var_2));
e_acsl_assert(__e_acsl_var_3 == 0,(char *)"Assertion",
mpz_t __e_acsl;
mpz_t __e_acsl_2;
int __e_acsl_3;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl),(long)((int)x));
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_2),(long)y);
__e_acsl_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl),
(__mpz_struct const *)(__e_acsl_2));
e_acsl_assert(__e_acsl_3 == 0,(char *)"Assertion",
(char *)"((int)x == y)",11);
__gmpz_clear((__mpz_struct *)(__e_acsl_var));
__gmpz_clear((__mpz_struct *)(__e_acsl_var_2));
__gmpz_clear((__mpz_struct *)(__e_acsl));
__gmpz_clear((__mpz_struct *)(__e_acsl_2));
}
/*@ assert x ≡ (long)y; */ ;
{
mpz_t __e_acsl_var_4;
mpz_t __e_acsl_var_5;
int __e_acsl_var_6;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var_4),x);
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var_5),(long)y);
__e_acsl_var_6 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_var_4),
(__mpz_struct const *)(__e_acsl_var_5));
e_acsl_assert(__e_acsl_var_6 == 0,(char *)"Assertion",
mpz_t __e_acsl_4;
mpz_t __e_acsl_5;
int __e_acsl_6;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_4),x);
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_5),(long)y);
__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 *)"(x == (long)y)",12);
__gmpz_clear((__mpz_struct *)(__e_acsl_var_4));
__gmpz_clear((__mpz_struct *)(__e_acsl_var_5));
__gmpz_clear((__mpz_struct *)(__e_acsl_4));
__gmpz_clear((__mpz_struct *)(__e_acsl_5));
}
/*@ assert y ≡ (int)0; */ ;
{
mpz_t __e_acsl_var_7;
mpz_t __e_acsl_var_8;
int __e_acsl_var_9;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var_7),(long)y);
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var_8),(long)0);
__e_acsl_var_9 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_var_7),
(__mpz_struct const *)(__e_acsl_var_8));
e_acsl_assert(__e_acsl_var_9 == 0,(char *)"Assertion",
mpz_t __e_acsl_7;
mpz_t __e_acsl_8;
int __e_acsl_9;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_7),(long)y);
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_8),(long)0);
__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 *)"Assertion",
(char *)"(y == (int)0)",14);
__gmpz_clear((__mpz_struct *)(__e_acsl_var_7));
__gmpz_clear((__mpz_struct *)(__e_acsl_var_8));
__gmpz_clear((__mpz_struct *)(__e_acsl_7));
__gmpz_clear((__mpz_struct *)(__e_acsl_8));
}
/*@ assert (unsigned int)y ≡ (unsigned int)0; */ ;
{
mpz_t __e_acsl_var_10;
mpz_t __e_acsl_var_11;
int __e_acsl_var_12;
__gmpz_init_set_ui((__mpz_struct *)(__e_acsl_var_10),
mpz_t __e_acsl_10;
mpz_t __e_acsl_11;
int __e_acsl_12;
__gmpz_init_set_ui((__mpz_struct *)(__e_acsl_10),
(unsigned long)((unsigned int)y));
__gmpz_init_set_ui((__mpz_struct *)(__e_acsl_var_11),
__gmpz_init_set_ui((__mpz_struct *)(__e_acsl_11),
(unsigned long)((unsigned int)0));
__e_acsl_var_12 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_var_10),
(__mpz_struct const *)(__e_acsl_var_11));
e_acsl_assert(__e_acsl_var_12 == 0,(char *)"Assertion",
__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 *)"Assertion",
(char *)"((unsigned int)y == (unsigned int)0)",15);
__gmpz_clear((__mpz_struct *)(__e_acsl_var_10));
__gmpz_clear((__mpz_struct *)(__e_acsl_var_11));
__gmpz_clear((__mpz_struct *)(__e_acsl_10));
__gmpz_clear((__mpz_struct *)(__e_acsl_11));
}
/*@ assert y ≢ (int)0xfffffffffffffff; */ ;
{
mpz_t __e_acsl_var_13;
mpz_t __e_acsl_var_14;
unsigned long __e_acsl_var_15;
mpz_t __e_acsl_var_16;
int __e_acsl_var_17;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var_13),(long)y);
__gmpz_init_set_str((__mpz_struct *)(__e_acsl_var_14),
"1152921504606846975",10);
__e_acsl_var_15 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_var_14));
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_var_16),
(long)((int)__e_acsl_var_15));
__e_acsl_var_17 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_var_13),
(__mpz_struct const *)(__e_acsl_var_16));
e_acsl_assert(__e_acsl_var_17 != 0,(char *)"Assertion",
mpz_t __e_acsl_13;
mpz_t __e_acsl_14;
unsigned long __e_acsl_15;
mpz_t __e_acsl_16;
int __e_acsl_17;
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_13),(long)y);
__gmpz_init_set_str((__mpz_struct *)(__e_acsl_14),"1152921504606846975",
10);
__e_acsl_15 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_14));
__gmpz_init_set_si((__mpz_struct *)(__e_acsl_16),
(long)((int)__e_acsl_15));
__e_acsl_17 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_13),
(__mpz_struct const *)(__e_acsl_16));
e_acsl_assert(__e_acsl_17 != 0,(char *)"Assertion",
(char *)"(y != (int)0xfffffffffffffff)",18);
__gmpz_clear((__mpz_struct *)(__e_acsl_var_13));
__gmpz_clear((__mpz_struct *)(__e_acsl_var_14));
__gmpz_clear((__mpz_struct *)(__e_acsl_var_16));
__gmpz_clear((__mpz_struct *)(__e_acsl_13));
__gmpz_clear((__mpz_struct *)(__e_acsl_14));
__gmpz_clear((__mpz_struct *)(__e_acsl_16));
}
/*@ assert (unsigned int)y ≢ (unsigned int)0xfffffffffffffff; */ ;
{
mpz_t __e_acsl_var_18;
mpz_t __e_acsl_var_19;
unsigned long __e_acsl_var_20;
mpz_t __e_acsl_var_21;
int __e_acsl_var_22;
__gmpz_init_set_ui((__mpz_struct *)(__e_acsl_var_18),
mpz_t __e_acsl_18;
mpz_t __e_acsl_19;
unsigned long __e_acsl_20;
mpz_t __e_acsl_21;
int __e_acsl_22;
__gmpz_init_set_ui((__mpz_struct *)(__e_acsl_18),
(unsigned long)((unsigned int)y));
__gmpz_init_set_str((__mpz_struct *)(__e_acsl_var_19),
"1152921504606846975",10);
__e_acsl_var_20 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_var_19));
__gmpz_init_set_ui((__mpz_struct *)(__e_acsl_var_21),
(unsigned long)((unsigned int)__e_acsl_var_20));
__e_acsl_var_22 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_var_18),
(__mpz_struct const *)(__e_acsl_var_21));
e_acsl_assert(__e_acsl_var_22 != 0,(char *)"Assertion",
__gmpz_init_set_str((__mpz_struct *)(__e_acsl_19),"1152921504606846975",
10);
__e_acsl_20 = __gmpz_get_ui((__mpz_struct const *)(__e_acsl_19));
__gmpz_init_set_ui((__mpz_struct *)(__e_acsl_21),
(unsigned long)((unsigned int)__e_acsl_20));
__e_acsl_22 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_18),
(__mpz_struct const *)(__e_acsl_21));
e_acsl_assert(__e_acsl_22 != 0,(char *)"Assertion",
(char *)"((unsigned int)y != (unsigned int)0xfffffffffffffff)",
19);
__gmpz_clear((__mpz_struct *)(__e_acsl_var_18));
__gmpz_clear((__mpz_struct *)(__e_acsl_var_19));
__gmpz_clear((__mpz_struct *)(__e_acsl_var_21));
__gmpz_clear((__mpz_struct *)(__e_acsl_18));
__gmpz_clear((__mpz_struct *)(__e_acsl_19));
__gmpz_clear((__mpz_struct *)(__e_acsl_21));
}
__retres = 0;
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
+ 44
− 45
View file @ 85e1595b
......@@ -93,26 +93,26 @@ void j(void)
void k(void)
{
{
int __e_acsl_var;
int __e_acsl_var_2;
int __e_acsl_var_3;
int __e_acsl_var_4;
int __e_acsl_var_5;
if (! (X == 1)) { __e_acsl_var = 1; }
else { __e_acsl_var = X == 0; }
e_acsl_assert(__e_acsl_var,(char *)"Precondition",
int __e_acsl;
int __e_acsl_2;
int __e_acsl_3;
int __e_acsl_4;
int __e_acsl_5;
if (! (X == 1)) { __e_acsl = 1; }
else { __e_acsl = X == 0; }
e_acsl_assert(__e_acsl,(char *)"Precondition",
(char *)"(X == 1 ==> X == 0)",40);
if (X == 3) { __e_acsl_var_2 = Y == 2; }
else { __e_acsl_var_2 = 0; }
if (! __e_acsl_var_2) { __e_acsl_var_3 = 1; }
else { __e_acsl_var_3 = X == 3; }
e_acsl_assert(__e_acsl_var_3,(char *)"Precondition",
if (X == 3) { __e_acsl_2 = Y == 2; }
else { __e_acsl_2 = 0; }
if (! __e_acsl_2) { __e_acsl_3 = 1; }
else { __e_acsl_3 = X == 3; }
e_acsl_assert(__e_acsl_3,(char *)"Precondition",
(char *)"(X == 3 && Y == 2 ==> X == 3)",44);
if (X == 3) { __e_acsl_var_4 = Y == 2; }
else { __e_acsl_var_4 = 0; }
if (! __e_acsl_var_4) { __e_acsl_var_5 = 1; }
else { __e_acsl_var_5 = (long long)X + (long long)Y == (long long)5; }
e_acsl_assert(__e_acsl_var_5,(char *)"Precondition",
if (X == 3) { __e_acsl_4 = Y == 2; }
else { __e_acsl_4 = 0; }
if (! __e_acsl_4) { __e_acsl_5 = 1; }
else { __e_acsl_5 = (long long)X + (long long)Y == (long long)5; }
e_acsl_assert(__e_acsl_5,(char *)"Precondition",
(char *)"(X == 3 && Y == 2 ==> X+Y == 5)",45);
X += Y;
}
......@@ -143,42 +143,41 @@ int l(void)
*/
void m(void)
{
int __e_acsl_var;
int __e_acsl_var_4;
int __e_acsl_var_7;
int __e_acsl_var_8;
__e_acsl_var_8 = X;
{ int __e_acsl_var_6;
if (X == 5) { __e_acsl_var_6 = Y == 2; }
else { __e_acsl_var_6 = 0; }
__e_acsl_var_7 = __e_acsl_var_6;
int __e_acsl;
int __e_acsl_4;
int __e_acsl_7;
int __e_acsl_8;
__e_acsl_8 = X;
{ int __e_acsl_6;
if (X == 5) { __e_acsl_6 = Y == 2; }
else { __e_acsl_6 = 0; }
__e_acsl_7 = __e_acsl_6;
}
{ int __e_acsl_var_3;
if (X == 5) { __e_acsl_var_3 = Y == 2; }
else { __e_acsl_var_3 = 0; }
__e_acsl_var_4 = __e_acsl_var_3;
{ int __e_acsl_3;
if (X == 5) { __e_acsl_3 = Y == 2; }
else { __e_acsl_3 = 0; }
__e_acsl_4 = __e_acsl_3;
}
__e_acsl_var = X == 7;
__e_acsl = X == 7;
X += Y;
{
int __e_acsl_var_2;
int __e_acsl_var_5;
int __e_acsl_var_9;
if (! __e_acsl_var) { __e_acsl_var_2 = 1; }
else { __e_acsl_var_2 = X == 95; }
e_acsl_assert(__e_acsl_var_2,(char *)"Postcondition",
int __e_acsl_2;
int __e_acsl_5;
int __e_acsl_9;
if (! __e_acsl) { __e_acsl_2 = 1; }
else { __e_acsl_2 = X == 95; }
e_acsl_assert(__e_acsl_2,(char *)"Postcondition",
(char *)"(\\old(X == 7) ==> X == 95)",58);
if (! __e_acsl_var_4) { __e_acsl_var_5 = 1; }
else { __e_acsl_var_5 = X == 7; }
e_acsl_assert(__e_acsl_var_5,(char *)"Postcondition",
if (! __e_acsl_4) { __e_acsl_5 = 1; }
else { __e_acsl_5 = X == 7; }
e_acsl_assert(__e_acsl_5,(char *)"Postcondition",
(char *)"(\\old(X == 5 && Y == 2) ==> X == 7)",62);
if (! __e_acsl_var_7) { __e_acsl_var_9 = 1; }
else {
__e_acsl_var_9 = (long long)X == (long long)__e_acsl_var_8 + (long long)Y;
if (! __e_acsl_7) { __e_acsl_9 = 1; }
else { __e_acsl_9 = (long long)X == (long long)__e_acsl_8 + (long long)Y;
}
e_acsl_assert(__e_acsl_var_9,(char *)"Postcondition",
e_acsl_assert(__e_acsl_9,(char *)"Postcondition",
(char *)"(\\old(X == 5 && Y == 2) ==> X == \\old(X)+Y)",63);
return;
}
......
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