Commit 0b222f19 authored by Basile Desloges's avatar Basile Desloges Committed by Julien Signoles
Browse files

[eacsl:runtime] Update `__e_acsl_assert` signature

A `file` parameter is added before `line`, and the `char *` parameters
have been converted to `const char *`.
parent 876e35ce
......@@ -19,6 +19,7 @@
# configure configure
###############################################################################
- E-ACSL [2020/02/09] Improve verdict messages emitted by e_acsl_assert.
-* E-ACSL [2020/01/06] Fix typing bug in presence of variable-length
arrays that may lead to incorrect generated code.
-* E-ACSL [2019/12/04] Fix bug with compiler built-ins.
......
......@@ -124,10 +124,12 @@
* \param kind C string representing a kind an annotation (e.g., "Assertion")
* \param fct
* \param pred_txt stringified predicate
* \param file un-instrumented file of predicate placement
* \param line line of predicate placement in the un-instrumented file */
/*@ requires pred != 0;
@ assigns \nothing; */
void assert(int pred, char *kind, char *fct, char *pred_txt, int line)
void assert(int pred, const char *kind, const char *fct, const char *pred_txt,
const char * file, int line)
__attribute__((FC_BUILTIN));
/* }}} */
......
......@@ -105,11 +105,15 @@ int runtime_sound_verdict = 1;
#ifndef E_ACSL_EXTERNAL_ASSERT
/*! \brief Default implementation of E-ACSL runtime assertions */
void runtime_assert(int predicate, char *kind, char *fct, char *pred_txt, int line) {
void runtime_assert(int predicate, const char *kind, const char *fct,
const char *pred_txt, const char * file, int line) {
if (runtime_sound_verdict) {
if (! predicate) {
STDERR("%s failed at line %d (function %s).\n"
"The failing predicate is:\n%s.\n", kind, line, fct, pred_txt);
STDERR("%s: In function '%s'\n"
"%s:%d: Error: %s failed:\n"
"\tThe failing predicate is:\n"
"\t%s.\n",
file, fct, file, line, kind, pred_txt);
#ifndef E_ACSL_NO_ASSERT_FAIL /* Do fail on assertions */
#ifdef E_ACSL_FAIL_EXITCODE /* Fail by exit with a given code */
exit(E_ACSL_FAIL_EXITCODE);
......@@ -119,10 +123,11 @@ void runtime_assert(int predicate, char *kind, char *fct, char *pred_txt, int li
#endif
}
} else
STDERR("warning: no sound verdict (guess: %s) at line %d "
"(function %s).\nThe considered predicate is:\n%s.\n",
predicate ? "ok" : "FAIL",
line, fct, pred_txt);
STDERR("%s: In function '%s'\n"
"%s:%d: Warning: no sound verdict for %s (guess: %s).\n"
"\tthe considered predicate is:\n"
"\t%s\n",
file, fct, file, line, kind, predicate ? "ok": "FAIL", pred_txt);
}
#endif
......
......@@ -158,6 +158,7 @@ let mk_runtime_check ?(reverse=false) kind kf e p =
Kernel.Unicode.without_unicode
(Format.asprintf "%a@?" Printer.pp_predicate) p
in
let file = (fst loc).Filepath.pos_path in
let line = (fst loc).Filepath.pos_lnum in
let e =
if reverse
......@@ -170,6 +171,7 @@ let mk_runtime_check ?(reverse=false) kind kf e p =
kind_to_string loc kind;
Cil.mkString ~loc (Functions.RTL.get_original_name kf);
Cil.mkString ~loc msg;
Cil.mkString ~loc (Filepath.Normalized.to_pretty_string file);
Cil.integer loc line ]
(*
......
......@@ -8,25 +8,25 @@ int main(void)
int x = -3;
int y = 2;
long z = 2L;
__e_acsl_assert(-3 == x,(char *)"Assertion",(char *)"main",
(char *)"-3 == x",10);
__e_acsl_assert(-3 == x,"Assertion","main","-3 == x","tests/arith/arith.i",
10);
/*@ assert -3 ≡ x; */ ;
__e_acsl_assert(x == -3,(char *)"Assertion",(char *)"main",
(char *)"x == -3",11);
__e_acsl_assert(x == -3,"Assertion","main","x == -3","tests/arith/arith.i",
11);
/*@ assert x ≡ -3; */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"0 != ~0",12);
__e_acsl_assert(1,"Assertion","main","0 != ~0","tests/arith/arith.i",12);
/*@ assert 0 ≢ ~0; */ ;
__e_acsl_assert(x + 1L == -2L,(char *)"Assertion",(char *)"main",
(char *)"x + 1 == -2",14);
__e_acsl_assert(x + 1L == -2L,"Assertion","main","x + 1 == -2",
"tests/arith/arith.i",14);
/*@ assert x + 1 ≡ -2; */ ;
__e_acsl_assert(x - 1L == -4L,(char *)"Assertion",(char *)"main",
(char *)"x - 1 == -4",15);
__e_acsl_assert(x - 1L == -4L,"Assertion","main","x - 1 == -4",
"tests/arith/arith.i",15);
/*@ assert x - 1 ≡ -4; */ ;
__e_acsl_assert(x * 3L == -9L,(char *)"Assertion",(char *)"main",
(char *)"x * 3 == -9",16);
__e_acsl_assert(x * 3L == -9L,"Assertion","main","x * 3 == -9",
"tests/arith/arith.i",16);
/*@ assert x * 3 ≡ -9; */ ;
__e_acsl_assert(x / 3 == -1,(char *)"Assertion",(char *)"main",
(char *)"x / 3 == -1",17);
__e_acsl_assert(x / 3 == -1,"Assertion","main","x / 3 == -1",
"tests/arith/arith.i",17);
/*@ assert x / 3 ≡ -1; */ ;
{
__e_acsl_mpz_t __gen_e_acsl_;
......@@ -40,53 +40,53 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
__gmpz_init(__gen_e_acsl_div);
/*@ assert E_ACSL: 0xffffffffffffffffffffff ≢ 0; */
__e_acsl_assert(! (__gen_e_acsl_div_guard == 0),(char *)"Assertion",
(char *)"main",(char *)"0xffffffffffffffffffffff == 0",
18);
__e_acsl_assert(! (__gen_e_acsl_div_guard == 0),"Assertion","main",
"0xffffffffffffffffffffff == 0","tests/arith/arith.i",18);
__gmpz_tdiv_q(__gen_e_acsl_div,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_),
(__e_acsl_mpz_struct const *)(__gen_e_acsl_));
__gen_e_acsl__3 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_div));
__e_acsl_assert(__gen_e_acsl__3 == 1L,(char *)"Assertion",(char *)"main",
(char *)"0xffffffffffffffffffffff / 0xffffffffffffffffffffff == 1",
18);
__e_acsl_assert(__gen_e_acsl__3 == 1L,"Assertion","main",
"0xffffffffffffffffffffff / 0xffffffffffffffffffffff == 1",
"tests/arith/arith.i",18);
__gmpz_clear(__gen_e_acsl_);
__gmpz_clear(__gen_e_acsl__2);
__gmpz_clear(__gen_e_acsl_div);
}
/*@ assert 0xffffffffffffffffffffff / 0xffffffffffffffffffffff ≡ 1; */ ;
__e_acsl_assert(x % 2 == -1,(char *)"Assertion",(char *)"main",
(char *)"x % 2 == -1",19);
__e_acsl_assert(x % 2 == -1,"Assertion","main","x % 2 == -1",
"tests/arith/arith.i",19);
/*@ assert x % 2 ≡ -1; */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"-3 % -2 == -1",20);
__e_acsl_assert(1,"Assertion","main","-3 % -2 == -1","tests/arith/arith.i",
20);
/*@ assert -3 % -2 ≡ -1; */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"3 % -2 == 1",
__e_acsl_assert(1,"Assertion","main","3 % -2 == 1","tests/arith/arith.i",
21);
/*@ assert 3 % -2 ≡ 1; */ ;
__e_acsl_assert(((x * 2L + (3L + y)) - 4L) + (x - (long)y) == -10L,
(char *)"Assertion",(char *)"main",
(char *)"((x * 2 + (3 + y)) - 4) + (x - y) == -10",23);
"Assertion","main",
"((x * 2 + (3 + y)) - 4) + (x - y) == -10",
"tests/arith/arith.i",23);
/*@ assert ((x * 2 + (3 + y)) - 4) + (x - y) ≡ -10; */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"(0 == 1) == !(0 == 0)",25);
__e_acsl_assert(1,"Assertion","main","(0 == 1) == !(0 == 0)",
"tests/arith/arith.i",25);
/*@ assert (0 ≡ 1) ≡ !(0 ≡ 0); */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"(0 <= -1) == (0 > 0)",26);
__e_acsl_assert(1,"Assertion","main","(0 <= -1) == (0 > 0)",
"tests/arith/arith.i",26);
/*@ assert (0 ≤ -1) ≡ (0 > 0); */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"(0 >= -1) == (0 <= 0)",27);
__e_acsl_assert(1,"Assertion","main","(0 >= -1) == (0 <= 0)",
"tests/arith/arith.i",27);
/*@ assert (0 ≥ -1) ≡ (0 ≤ 0); */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"(0 != 1) == !(0 != 0)",28);
__e_acsl_assert(1,"Assertion","main","(0 != 1) == !(0 != 0)",
"tests/arith/arith.i",28);
/*@ assert (0 ≢ 1) ≡ !(0 ≢ 0); */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
(char *)"(0 != 0) == !(1 != 0)",30);
__e_acsl_assert(1,"Assertion","main","(0 != 0) == !(1 != 0)",
"tests/arith/arith.i",30);
/*@ assert (0 ≢ 0) ≡ !(1 ≢ 0); */ ;
__e_acsl_assert(y != 0,(char *)"RTE",(char *)"main",
(char *)"division_by_zero: y != 0",31);
__e_acsl_assert(4 / y == 2,(char *)"Assertion",(char *)"main",
(char *)"4 / y == 2",31);
__e_acsl_assert(y != 0,"RTE","main","division_by_zero: y != 0",
"tests/arith/arith.i",31);
__e_acsl_assert(4 / y == 2,"Assertion","main","4 / y == 2",
"tests/arith/arith.i",31);
/*@ assert 4 / y ≡ 2; */ ;
{
__e_acsl_mpz_t __gen_e_acsl_z;
......@@ -109,17 +109,17 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__6));
__gmpz_init(__gen_e_acsl_div_2);
/*@ assert E_ACSL: y - 123456789123456789 ≢ 0; */
__e_acsl_assert(! (__gen_e_acsl_div_guard_2 == 0),(char *)"Assertion",
(char *)"main",(char *)"y - 123456789123456789 == 0",34);
__e_acsl_assert(! (__gen_e_acsl_div_guard_2 == 0),"Assertion","main",
"y - 123456789123456789 == 0","tests/arith/arith.i",34);
__gmpz_tdiv_q(__gen_e_acsl_div_2,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
__gen_e_acsl__7 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_div_2));
/*@ assert Eva: signed_overflow: -2147483648 ≤ 1 + __gen_e_acsl__7; */
/*@ assert Eva: signed_overflow: 1 + __gen_e_acsl__7 ≤ 2147483647; */
__e_acsl_assert(1 + __gen_e_acsl__7 == 1,(char *)"Assertion",
(char *)"main",
(char *)"1 + (z + 1) / (y - 123456789123456789) == 1",34);
__e_acsl_assert(1 + __gen_e_acsl__7 == 1,"Assertion","main",
"1 + (z + 1) / (y - 123456789123456789) == 1",
"tests/arith/arith.i",34);
__gmpz_clear(__gen_e_acsl_z);
__gmpz_clear(__gen_e_acsl__4);
__gmpz_clear(__gen_e_acsl_add);
......@@ -128,8 +128,8 @@ int main(void)
__gmpz_clear(__gen_e_acsl_div_2);
}
/*@ assert 1 + (z + 1) / (y - 123456789123456789) ≡ 1; */ ;
__e_acsl_assert(1L - x == - ((long)x) + 1L,(char *)"Assertion",
(char *)"main",(char *)"1 - x == -x + 1",36);
__e_acsl_assert(1L - x == - ((long)x) + 1L,"Assertion","main",
"1 - x == -x + 1","tests/arith/arith.i",36);
/*@ assert 1 - x ≡ -x + 1; */ ;
__retres = 0;
return __retres;
......
......@@ -21,11 +21,11 @@ int main(void)
i_0 ++;
}
}
__e_acsl_assert(T1[0] == T2[0],(char *)"Assertion",(char *)"main",
(char *)"T1[0] == T2[0]",13);
__e_acsl_assert(T1[0] == T2[0],"Assertion","main","T1[0] == T2[0]",
"tests/arith/array.i",13);
/*@ assert T1[0] ≡ T2[0]; */ ;
__e_acsl_assert(T1[1] != T2[1],(char *)"Assertion",(char *)"main",
(char *)"T1[1] != T2[1]",14);
__e_acsl_assert(T1[1] != T2[1],"Assertion","main","T1[1] != T2[1]",
"tests/arith/array.i",14);
/*@ assert T1[1] ≢ T2[1]; */ ;
__retres = 0;
return __retres;
......
......@@ -21,17 +21,17 @@ void f(void)
__gen_e_acsl_at_2 = A;
A = 2;
}
__e_acsl_assert(__gen_e_acsl_at == 0,(char *)"Assertion",(char *)"f",
(char *)"\\at(A,Pre) == 0",11);
__e_acsl_assert(__gen_e_acsl_at == 0,"Assertion","f","\\at(A,Pre) == 0",
"tests/arith/at.i",11);
/*@ assert \at(A,Pre) ≡ 0; */ ;
__e_acsl_assert(__gen_e_acsl_at_2 == 1,(char *)"Assertion",(char *)"f",
(char *)"\\at(A,F) == 1",12);
__e_acsl_assert(__gen_e_acsl_at_2 == 1,"Assertion","f","\\at(A,F) == 1",
"tests/arith/at.i",12);
/*@ assert \at(A,F) ≡ 1; */ ;
__e_acsl_assert(A == 2,(char *)"Assertion",(char *)"f",
(char *)"\\at(A,Here) == 2",13);
__e_acsl_assert(A == 2,"Assertion","f","\\at(A,Here) == 2",
"tests/arith/at.i",13);
/*@ assert \at(A,Here) ≡ 2; */ ;
__e_acsl_assert(__gen_e_acsl_at_4 == 0,(char *)"Assertion",(char *)"f",
(char *)"\\at(\\at(A,Pre),F) == 0",14);
__e_acsl_assert(__gen_e_acsl_at_4 == 0,"Assertion","f",
"\\at(\\at(A,Pre),F) == 0","tests/arith/at.i",14);
/*@ assert \at(\at(A,Pre),F) ≡ 0; */ ;
A = 3;
return;
......@@ -57,16 +57,16 @@ void g(int *p, int *q)
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)q,sizeof(int),
(void *)q,
(void *)(& q));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(q)",28);
__e_acsl_assert(__gen_e_acsl_valid_read_3,"RTE","g",
"mem_access: \\valid_read(q)","tests/arith/at.i",28);
__gen_e_acsl_at_3 = *q;
}
{
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)q,sizeof(int),
(void *)q,(void *)(& q));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(q)",26);
__e_acsl_assert(__gen_e_acsl_valid_read,"RTE","g",
"mem_access: \\valid_read(q)","tests/arith/at.i",26);
__gen_e_acsl_at = *q;
}
__e_acsl_initialize((void *)p,sizeof(int));
......@@ -83,15 +83,16 @@ void g(int *p, int *q)
__gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at),
sizeof(int),(void *)p,
(void *)(& p));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(p + __gen_e_acsl_at)",
26);
__e_acsl_assert(__gen_e_acsl_valid_read_2,"RTE","g",
"mem_access: \\valid_read(p + __gen_e_acsl_at)",
"tests/arith/at.i",26);
__gen_e_acsl_at_2 = *(p + __gen_e_acsl_at);
}
A = 4;
}
__e_acsl_assert(__gen_e_acsl_at_2 == 2,(char *)"Assertion",(char *)"g",
(char *)"\\at(*(p + \\at(*q,__invalid_label)),L2) == 2",26);
__e_acsl_assert(__gen_e_acsl_at_2 == 2,"Assertion","g",
"\\at(*(p + \\at(*q,__invalid_label)),L2) == 2",
"tests/arith/at.i",26);
/*@ assert \at(*(p + \at(*q,__invalid_label)),L2) ≡ 2; */ ;
L3:
/*@ assert \at(*(p + \at(*q,__invalid_label)),Here) ≡ 2; */
......@@ -100,13 +101,12 @@ void g(int *p, int *q)
__gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at_3),
sizeof(int),(void *)p,
(void *)(& p));
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(p + __gen_e_acsl_at_3)",
28);
__e_acsl_assert(*(p + __gen_e_acsl_at_3) == 2,(char *)"Assertion",
(char *)"g",
(char *)"\\at(*(p + \\at(*q,__invalid_label)),Here) == 2",
28);
__e_acsl_assert(__gen_e_acsl_valid_read_4,"RTE","g",
"mem_access: \\valid_read(p + __gen_e_acsl_at_3)",
"tests/arith/at.i",28);
__e_acsl_assert(*(p + __gen_e_acsl_at_3) == 2,"Assertion","g",
"\\at(*(p + \\at(*q,__invalid_label)),Here) == 2",
"tests/arith/at.i",28);
}
__e_acsl_delete_block((void *)(& q));
__e_acsl_delete_block((void *)(& p));
......@@ -142,23 +142,21 @@ int main(void)
__gen_e_acsl_at_3 = (long)x;
__gen_e_acsl_at_2 = x + 1L;
__gen_e_acsl_at = x;
__e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",
(char *)"x == 0",43);
__e_acsl_assert(x == 0,"Assertion","main","x == 0","tests/arith/at.i",43);
}
__e_acsl_full_init((void *)(& x));
x = 1;
__e_acsl_full_init((void *)(& x));
x = 2;
__gen_e_acsl_f();
__e_acsl_assert(__gen_e_acsl_at == 0,(char *)"Assertion",(char *)"main",
(char *)"\\at(x,__invalid_label) == 0",48);
__e_acsl_assert(__gen_e_acsl_at == 0,"Assertion","main",
"\\at(x,__invalid_label) == 0","tests/arith/at.i",48);
/*@ assert \at(x,__invalid_label) ≡ 0; */ ;
__e_acsl_assert(__gen_e_acsl_at_2 == 1L,(char *)"Assertion",(char *)"main",
(char *)"\\at(x + 1,__invalid_label) == 1",49);
__e_acsl_assert(__gen_e_acsl_at_2 == 1L,"Assertion","main",
"\\at(x + 1,__invalid_label) == 1","tests/arith/at.i",49);
/*@ assert \at(x + 1,__invalid_label) ≡ 1; */ ;
__e_acsl_assert(__gen_e_acsl_at_3 + 1L == 1L,(char *)"Assertion",
(char *)"main",(char *)"\\at(x,__invalid_label) + 1 == 1",
50);
__e_acsl_assert(__gen_e_acsl_at_3 + 1L == 1L,"Assertion","main",
"\\at(x,__invalid_label) + 1 == 1","tests/arith/at.i",50);
/*@ assert \at(x,__invalid_label) + 1 ≡ 1; */ ;
g(t,& x);
__retres = 0;
......@@ -177,8 +175,8 @@ int __gen_e_acsl_h(int x)
__e_acsl_store_block((void *)(& x),(size_t)4);
__gen_e_acsl_at = x;
__retres = h(x);
__e_acsl_assert(__retres == __gen_e_acsl_at,(char *)"Postcondition",
(char *)"h",(char *)"\\result == \\old(x)",35);
__e_acsl_assert(__retres == __gen_e_acsl_at,"Postcondition","h",
"\\result == \\old(x)","tests/arith/at.i",35);
__e_acsl_delete_block((void *)(& x));
__e_acsl_delete_block((void *)(& __retres));
return __retres;
......@@ -190,8 +188,8 @@ void __gen_e_acsl_f(void)
int __gen_e_acsl_at;
f();
__gen_e_acsl_at = A;
__e_acsl_assert(__gen_e_acsl_at == 3,(char *)"Postcondition",(char *)"f",
(char *)"\\at(A,Post) == 3",7);
__e_acsl_assert(__gen_e_acsl_at == 3,"Postcondition","f",
"\\at(A,Post) == 3","tests/arith/at.i",7);
return;
}
......
......@@ -51,9 +51,9 @@ void g(void)
sizeof(int),
(void *)__gen_e_acsl_at,
(void *)(& __gen_e_acsl_at));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"g",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at + (int)(__gen_e_acsl_w - 3))",
16);
__e_acsl_assert(__gen_e_acsl_valid_read,"RTE","g",
"mem_access: \\valid_read(__gen_e_acsl_at + (int)(__gen_e_acsl_w - 3))",
"tests/arith/at_on-purely-logic-variables.c",16);
/*@ assert
Eva: initialization:
\initialized(__gen_e_acsl_at + (__gen_e_acsl_w - 3));
......@@ -67,9 +67,9 @@ void g(void)
__gen_e_acsl_w ++;
}
e_acsl_end_loop1: ;
__e_acsl_assert(__gen_e_acsl_exists,(char *)"Assertion",(char *)"g",
(char *)"\\exists integer w; 3 <= w < 6 && \\at(m + w == 12,Q)",
16);
__e_acsl_assert(__gen_e_acsl_exists,"Assertion","g",
"\\exists integer w; 3 <= w < 6 && \\at(m + w == 12,Q)",
"tests/arith/at_on-purely-logic-variables.c",16);
}
/*@ assert ∃ ℤ w; 3 ≤ w < 6 ∧ \at(m + w ≡ 12,Q); */ ;
free((void *)__gen_e_acsl_at);
......@@ -213,12 +213,12 @@ int main(void)
sizeof(int),
(void *)__gen_e_acsl_at,
(void *)(& __gen_e_acsl_at));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at + 0)",
28);
__e_acsl_assert(*(__gen_e_acsl_at + 0),(char *)"Assertion",
(char *)"main",
(char *)"\\let i = 3; \\at(n + i == 10,L)",28);
__e_acsl_assert(__gen_e_acsl_valid_read,"RTE","main",
"mem_access: \\valid_read(__gen_e_acsl_at + 0)",
"tests/arith/at_on-purely-logic-variables.c",28);
__e_acsl_assert(*(__gen_e_acsl_at + 0),"Assertion","main",
"\\let i = 3; \\at(n + i == 10,L)",
"tests/arith/at_on-purely-logic-variables.c",28);
}
/*@ assert \let i = 3; \at(n + i ≡ 10,L); */ ;
{
......@@ -235,10 +235,9 @@ int main(void)
sizeof(int),
(void *)__gen_e_acsl_at_2,
(void *)(& __gen_e_acsl_at_2));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
(char *)"main",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_j - 2))",
29);
__e_acsl_assert(__gen_e_acsl_valid_read_2,"RTE","main",
"mem_access: \\valid_read(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_j - 2))",
"tests/arith/at_on-purely-logic-variables.c",29);
/*@ assert
Eva: initialization:
\initialized(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2));
......@@ -252,9 +251,9 @@ int main(void)
__gen_e_acsl_j ++;
}
e_acsl_end_loop2: ;
__e_acsl_assert(__gen_e_acsl_exists,(char *)"Assertion",(char *)"main",
(char *)"\\exists integer j; 2 <= j < 5 && \\at(n + j == 11,L)",
29);
__e_acsl_assert(__gen_e_acsl_exists,"Assertion","main",
"\\exists integer j; 2 <= j < 5 && \\at(n + j == 11,L)",
"tests/arith/at_on-purely-logic-variables.c",29);
}
/*@ assert ∃ ℤ j; 2 ≤ j < 5 ∧ \at(n + j ≡ 11,L); */ ;
{
......@@ -284,10 +283,9 @@ int main(void)
sizeof(int),
(void *)__gen_e_acsl_at_3,
(void *)(& __gen_e_acsl_at_3));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",
(char *)"main",
(char *)"mem_access:\n \\valid_read(__gen_e_acsl_at_3 +\n (int)((int)((int)(__gen_e_acsl_u - 9) * 11) +\n (int)((int)(__gen_e_acsl_v - -5) - 1)))",
34);
__e_acsl_assert(__gen_e_acsl_valid_read_3,"RTE","main",
"mem_access:\n \\valid_read(__gen_e_acsl_at_3 +\n (int)((int)((int)(__gen_e_acsl_u - 9) * 11) +\n (int)((int)(__gen_e_acsl_v - -5) - 1)))",
"tests/arith/at_on-purely-logic-variables.c",34);
/*@ assert
Eva: initialization:
\initialized(__gen_e_acsl_at_3 +
......@@ -314,9 +312,9 @@ int main(void)
__gen_e_acsl_u ++;
}
e_acsl_end_loop4: ;
__e_acsl_assert(__gen_e_acsl_exists_2,(char *)"Assertion",(char *)"main",
(char *)"\\let k = -7;\n\\exists integer u;\n 9 <= u < 21 &&\n (\\forall integer v; -5 < v <= 6 ==> \\at((u > 0? n + k: u + v) > 0,K))",
31);
__e_acsl_assert(__gen_e_acsl_exists_2,"Assertion","main",
"\\let k = -7;\n\\exists integer u;\n 9 <= u < 21 &&\n (\\forall integer v; -5 < v <= 6 ==> \\at((u > 0? n + k: u + v) > 0,K))",
"tests/arith/at_on-purely-logic-variables.c",31);
}
/*@
assert \let k = -7;
......@@ -333,12 +331,12 @@ int main(void)
sizeof(long),
(void *)__gen_e_acsl_at_4,
(void *)(& __gen_e_acsl_at_4));
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_4 + 0)",
37);
__e_acsl_assert(*(__gen_e_acsl_at_4 + 0) == 10L,(char *)"Assertion",
(char *)"main",
(char *)"\\let i = 3; \\at(n + i,L) == 10",37);
__e_acsl_assert(__gen_e_acsl_valid_read_4,"RTE","main",
"mem_access: \\valid_read(__gen_e_acsl_at_4 + 0)",
"tests/arith/at_on-purely-logic-variables.c",37);
__e_acsl_assert(*(__gen_e_acsl_at_4 + 0) == 10L,"Assertion","main",
"\\let i = 3; \\at(n + i,L) == 10",
"tests/arith/at_on-purely-logic-variables.c",37);
}
/*@ assert \let i = 3; \at(n + i,L) ≡ 10; */ ;
unsigned int m = (unsigned int)3;
......@@ -371,10 +369,9 @@ int main(void)
sizeof(long),
(void *)__gen_e_acsl_at_5,
(void *)(& __gen_e_acsl_at_5));
__e_acsl_assert(__gen_e_acsl_valid_read_5,(char *)"RTE",
(char *)"main",
(char *)"mem_access:\n \\valid_read(__gen_e_acsl_at_5 + (int)((int)(__gen_e_acsl_k_3 - -9) - 1))",
41);
__e_acsl_assert(__gen_e_acsl_valid_read_5,"RTE","main",
"mem_access:\n \\valid_read(__gen_e_acsl_at_5 + (int)((int)(__gen_e_acsl_k_3 - -9) - 1))",
"tests/arith/at_on-purely-logic-variables.c",41);
/*@ assert
Eva: initialization:
\initialized(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1));
......@@ -389,9 +386,9 @@ int main(void)
__gen_e_acsl_k_3 ++;
}
e_acsl_end_loop5: ;
__e_acsl_assert(__gen_e_acsl_exists_3,(char *)"Assertion",(char *)"main",
(char *)"\\exists integer k; -9 < k < 0 && \\at(m + k,G) == 0",
41);
__e_acsl_assert(__gen_e_acsl_exists_3,"Assertion","main",
"\\exists integer k; -9 < k < 0 && \\at(m + k,G) == 0",
"tests/arith/at_on-purely-logic-variables.c",41);
}
/*@ assert ∃ ℤ k; -9 < k < 0 ∧ \at(m + k,G) ≡ 0; */ ;
{
......@@ -424,10 +421,9 @@ int main(void)
sizeof(int),
(void *)__gen_e_acsl_at_6,
(void *)(& __gen_e_acsl_at_6));
__e_acsl_assert(__gen_e_acsl_valid_read_6,(char *)"RTE",
(char *)"main",
(char *)"mem_access:\n \\valid_read(__gen_e_acsl_at_6 +\n (int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32) +\n (int)((int)(__gen_e_acsl_v_3 - -5) - 1)))",
45);
__e_acsl_assert(__gen_e_acsl_valid_read_6,"RTE","main",
"mem_access:\n \\valid_read(__gen_e_acsl_at_6 +\n (int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32) +\n (int)((int)(__gen_e_acsl_v_3 - -5) - 1)))",
"tests/arith/at_on-purely-logic-variables.c",45);
/*@ assert
Eva: initialization:
\initialized(__gen_e_acsl_at_6 +
......@@ -454,9 +450,9 @@ int main(void)
__gen_e_acsl_u_3 ++;
}
e_acsl_end_loop7: ;
__e_acsl_assert(__gen_e_acsl_exists_4,(char *)"Assertion",(char *)"main",
(char *)"\\exists integer u;\n 9 <= u < 21 &&\n (\\forall integer v; -5 < v <= (u < 15? u + 6: 3) ==> \\at((n + u) + v > 0,K))",
43);
__e_acsl_assert(__gen_e_acsl_exists_4,"Assertion","main",
"\\exists integer u;\n 9 <= u < 21 &&\n (\\forall integer v; -5 < v <= (u < 15? u + 6: 3) ==> \\at((n + u) + v > 0,K))",
"tests/arith/at_on-purely-logic-variables.c",43);
}
/*@
assert
......@@ -511,9 +507,9 @@ int main(void)
sizeof(int),