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

[e-acsl] add missing directory `doc' 

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