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

testing relations

parent df697e32
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/tests/e-acsl-runtime/comparison.i 0 → 100644
+ 17
− 0
View file @ b17aeb16
/* run.config
COMMENT: TODO: this test is incomplete
COMMENT: comparison operators */
void main() {
/* /\*@ assert "toto" < "titi"; *\/ */
/* /\*@ assert "toto" > "titi"; *\/ */
/* /\*@ assert "toto" <= "titi"; *\/ */
/* /\*@ assert "toto" >= "titi"; *\/ */
/* /\*@ assert "toto" == "titi"; *\/ */
/*@ assert "toto" != "titi"; */
/*@ assert 5 < 18; */
/*@ assert 32 > 3; */
/*@ assert 12 <= 13; */
/*@ assert 123 >= 12; */
/*@ assert 0xff == 0xff; */
/*@ assert 1 != 2; */
}
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.err.oracle 0 → 100644
+ 0
− 0
View file @ b17aeb16
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle 0 → 100644
+ 366
− 0
View file @ b17aeb16
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
PROJECT_FILE:73:[value] Assertion got status valid.
PROJECT_FILE:80:[value] Assertion got status valid.
[value] computing for function mpz_init <-main.
Called from PROJECT_FILE:82.
PROJECT_FILE:82:[value] Function mpz_init: postcondition got status unknown
[value] Done for function mpz_init
[value] computing for function mpz_set_si <-main.
Called from PROJECT_FILE:82.
PROJECT_FILE:82:[value] Function mpz_set_si: precondition got status valid
[value] Done for function mpz_set_si
[value] computing for function mpz_init <-main.
Called from PROJECT_FILE:83.
PROJECT_FILE:83:[value] Function mpz_init: postcondition got status unknown
[value] Done for function mpz_init
[value] computing for function mpz_set_si <-main.
Called from PROJECT_FILE:83.
PROJECT_FILE:83:[value] Function mpz_set_si: precondition got status valid
[value] Done for function mpz_set_si
[value] computing for function mpz_cmp <-main.
Called from PROJECT_FILE:84.
PROJECT_FILE:84:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <-main.
Called from PROJECT_FILE:85.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
[value] computing for function exit <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
PROJECT_FILE:69:[value] Function exit: postcondition got status invalid
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
Called from PROJECT_FILE:86.
PROJECT_FILE:86:[value] Function mpz_clear: precondition got status valid
[value] Done for function mpz_clear
[value] computing for function mpz_clear <-main.
Called from PROJECT_FILE:86.
[value] Done for function mpz_clear
PROJECT_FILE:89:[value] Assertion got status valid.
[value] computing for function mpz_init <-main.
Called from PROJECT_FILE:91.
PROJECT_FILE:91:[value] Function mpz_init: postcondition got status unknown
[value] Done for function mpz_init
[value] computing for function mpz_set_si <-main.
Called from PROJECT_FILE:91.
PROJECT_FILE:91:[value] Function mpz_set_si: precondition got status valid
[value] Done for function mpz_set_si
[value] computing for function mpz_init <-main.
Called from PROJECT_FILE:92.
PROJECT_FILE:92:[value] Function mpz_init: postcondition got status unknown
[value] Done for function mpz_init
[value] computing for function mpz_set_si <-main.
Called from PROJECT_FILE:92.
PROJECT_FILE:92:[value] Function mpz_set_si: precondition got status valid
[value] Done for function mpz_set_si
[value] computing for function mpz_cmp <-main.
Called from PROJECT_FILE:93.
PROJECT_FILE:93:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <-main.
Called from PROJECT_FILE:94.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
[value] computing for function exit <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
Called from PROJECT_FILE:95.
PROJECT_FILE:95:[value] Function mpz_clear: precondition got status valid
[value] Done for function mpz_clear
[value] computing for function mpz_clear <-main.
Called from PROJECT_FILE:95.
[value] Done for function mpz_clear
PROJECT_FILE:98:[value] Assertion got status valid.
[value] computing for function mpz_init <-main.
Called from PROJECT_FILE:100.
PROJECT_FILE:100:[value] Function mpz_init: postcondition got status unknown
[value] Done for function mpz_init
[value] computing for function mpz_set_si <-main.
Called from PROJECT_FILE:100.
PROJECT_FILE:100:[value] Function mpz_set_si: precondition got status valid
[value] Done for function mpz_set_si
[value] computing for function mpz_init <-main.
Called from PROJECT_FILE:101.
PROJECT_FILE:101:[value] Function mpz_init: postcondition got status unknown
[value] Done for function mpz_init
[value] computing for function mpz_set_si <-main.
Called from PROJECT_FILE:101.
PROJECT_FILE:101:[value] Function mpz_set_si: precondition got status valid
[value] Done for function mpz_set_si
[value] computing for function mpz_cmp <-main.
Called from PROJECT_FILE:102.
PROJECT_FILE:102:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <-main.
Called from PROJECT_FILE:103.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
[value] computing for function exit <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
Called from PROJECT_FILE:104.
PROJECT_FILE:104:[value] Function mpz_clear: precondition got status valid
[value] Done for function mpz_clear
[value] computing for function mpz_clear <-main.
Called from PROJECT_FILE:104.
[value] Done for function mpz_clear
PROJECT_FILE:107:[value] Assertion got status valid.
[value] computing for function mpz_init <-main.
Called from PROJECT_FILE:109.
PROJECT_FILE:109:[value] Function mpz_init: postcondition got status unknown
[value] Done for function mpz_init
[value] computing for function mpz_set_si <-main.
Called from PROJECT_FILE:109.
PROJECT_FILE:109:[value] Function mpz_set_si: precondition got status valid
[value] Done for function mpz_set_si
[value] computing for function mpz_init <-main.
Called from PROJECT_FILE:110.
PROJECT_FILE:110:[value] Function mpz_init: postcondition got status unknown
[value] Done for function mpz_init
[value] computing for function mpz_set_si <-main.
Called from PROJECT_FILE:110.
PROJECT_FILE:110:[value] Function mpz_set_si: precondition got status valid
[value] Done for function mpz_set_si
[value] computing for function mpz_cmp <-main.
Called from PROJECT_FILE:111.
PROJECT_FILE:111:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <-main.
Called from PROJECT_FILE:112.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
[value] computing for function exit <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
Called from PROJECT_FILE:113.
PROJECT_FILE:113:[value] Function mpz_clear: precondition got status valid
[value] Done for function mpz_clear
[value] computing for function mpz_clear <-main.
Called from PROJECT_FILE:113.
[value] Done for function mpz_clear
PROJECT_FILE:116:[value] Assertion got status valid.
[value] computing for function mpz_init <-main.
Called from PROJECT_FILE:117.
PROJECT_FILE:117:[value] Function mpz_init: postcondition got status unknown
[value] Done for function mpz_init
[value] computing for function mpz_set_si <-main.
Called from PROJECT_FILE:118.
PROJECT_FILE:118:[value] Function mpz_set_si: precondition got status valid
[value] Done for function mpz_set_si
[value] computing for function mpz_cmp <-main.
Called from PROJECT_FILE:119.
PROJECT_FILE:119:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <-main.
Called from PROJECT_FILE:120.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
[value] computing for function exit <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
Called from PROJECT_FILE:121.
PROJECT_FILE:121:[value] Function mpz_clear: precondition got status valid
[value] Done for function mpz_clear
PROJECT_FILE:124:[value] Assertion got status valid.
[value] computing for function mpz_init <-main.
Called from PROJECT_FILE:126.
PROJECT_FILE:126:[value] Function mpz_init: postcondition got status unknown
[value] Done for function mpz_init
[value] computing for function mpz_set_si <-main.
Called from PROJECT_FILE:126.
PROJECT_FILE:126:[value] Function mpz_set_si: precondition got status valid
[value] Done for function mpz_set_si
[value] computing for function mpz_init <-main.
Called from PROJECT_FILE:127.
PROJECT_FILE:127:[value] Function mpz_init: postcondition got status unknown
[value] Done for function mpz_init
[value] computing for function mpz_set_si <-main.
Called from PROJECT_FILE:127.
PROJECT_FILE:127:[value] Function mpz_set_si: precondition got status valid
[value] Done for function mpz_set_si
[value] computing for function mpz_cmp <-main.
Called from PROJECT_FILE:128.
PROJECT_FILE:128:[value] Function mpz_cmp: precondition got status valid
[value] Done for function mpz_cmp
[value] computing for function e_acsl_fail <-main.
Called from PROJECT_FILE:129.
[value] computing for function eprintf <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function eprintf
[value] computing for function exit <-e_acsl_fail <-main.
Called from PROJECT_FILE:69.
[value] Done for function exit
[value] Recording results for e_acsl_fail
[value] Done for function e_acsl_fail
[value] computing for function mpz_clear <-main.
Called from PROJECT_FILE:130.
PROJECT_FILE:130:[value] Function mpz_clear: precondition got status valid
[value] Done for function mpz_clear
[value] computing for function mpz_clear <-main.
Called from PROJECT_FILE:130.
[value] Done for function mpz_clear
[value] Recording results for main
[value] done for function main
[from] Computing for function mpz_init
[from] Done for function mpz_init
[from] Computing for function mpz_set_si
[from] Done for function mpz_set_si
[from] Computing for function mpz_cmp
[from] Done for function mpz_cmp
[from] Computing for function e_acsl_fail
[from] Computing for function eprintf <-e_acsl_fail
[from] Done for function eprintf
[from] Computing for function exit <-e_acsl_fail
[from] Done for function exit
PROJECT_FILE:69:[from] Non terminating function (no dependencies)
[from] Done for function e_acsl_fail
[from] Computing for function mpz_clear
[from] Done for function mpz_clear
[dominators] computing for function main
[dominators] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values for function e_acsl_fail:
NON TERMINATING FUNCTION
[value] Values for function main:
/* 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(\at(x,Old));
assigns *x; */
extern void mpz_init(__mpz_struct * /*[1]*/ x ) ;
/*@ requires \valid(x);
assigns *x; */
extern void mpz_clear(__mpz_struct * /*[1]*/ x ) ;
/*@ requires \valid(z);
assigns *z; */
extern void mpz_set_si(__mpz_struct * /*[1]*/ z , long n ) ;
/*@ requires \valid(z1);
requires \valid(z2);
assigns \nothing; */
extern int mpz_cmp(__mpz_struct * /*[1]*/ z1 , __mpz_struct * /*[1]*/ z2 ) ;
/*@ terminates \false;
ensures \false;
assigns \nothing; */
extern void exit(int status ) ;
/*@ assigns \nothing; */
extern void eprintf(char * ) ;
void e_acsl_fail(char *msg )
{
eprintf(msg);
exit(1);
return;
}
void main(void)
{
/*@ assert ("toto" ≢ "titi"); */ ;
if ("toto" == "titi") {
e_acsl_fail((char *)"((\"toto\" \342\211\242 \"titi\"))");
}
/*@ assert (5 < 18); */ ;
{ mpz_t e_acsl_cst_1 ; mpz_t e_acsl_cst_2 ; int e_acsl_cst_3 ;
mpz_init((__mpz_struct *)(e_acsl_cst_1));
mpz_set_si((__mpz_struct *)(e_acsl_cst_1),(long )5);
mpz_init((__mpz_struct *)(e_acsl_cst_2));
mpz_set_si((__mpz_struct *)(e_acsl_cst_2),(long )18);
e_acsl_cst_3 = mpz_cmp((__mpz_struct *)(e_acsl_cst_1),
(__mpz_struct *)(e_acsl_cst_2));
if (e_acsl_cst_3 >= 0) { e_acsl_fail((char *)"((5 < 18))"); }
mpz_clear((__mpz_struct *)(e_acsl_cst_2));
mpz_clear((__mpz_struct *)(e_acsl_cst_1));
}
/*@ assert (32 > 3); */ ;
{ mpz_t e_acsl_cst_4 ; mpz_t e_acsl_cst_5 ; int e_acsl_cst_6 ;
mpz_init((__mpz_struct *)(e_acsl_cst_4));
mpz_set_si((__mpz_struct *)(e_acsl_cst_4),(long )32);
mpz_init((__mpz_struct *)(e_acsl_cst_5));
mpz_set_si((__mpz_struct *)(e_acsl_cst_5),(long )3);
e_acsl_cst_6 = mpz_cmp((__mpz_struct *)(e_acsl_cst_4),
(__mpz_struct *)(e_acsl_cst_5));
if (e_acsl_cst_6 <= 0) { e_acsl_fail((char *)"((32 > 3))"); }
mpz_clear((__mpz_struct *)(e_acsl_cst_5));
mpz_clear((__mpz_struct *)(e_acsl_cst_4));
}
/*@ assert (12 ≤ 13); */ ;
{ mpz_t e_acsl_cst_7 ; mpz_t e_acsl_cst_8 ; int e_acsl_cst_9 ;
mpz_init((__mpz_struct *)(e_acsl_cst_7));
mpz_set_si((__mpz_struct *)(e_acsl_cst_7),(long )12);
mpz_init((__mpz_struct *)(e_acsl_cst_8));
mpz_set_si((__mpz_struct *)(e_acsl_cst_8),(long )13);
e_acsl_cst_9 = mpz_cmp((__mpz_struct *)(e_acsl_cst_7),
(__mpz_struct *)(e_acsl_cst_8));
if (e_acsl_cst_9 > 0) { e_acsl_fail((char *)"((12 \342\211\244 13))"); }
mpz_clear((__mpz_struct *)(e_acsl_cst_8));
mpz_clear((__mpz_struct *)(e_acsl_cst_7));
}
/*@ assert (123 ≥ 12); */ ;
{ mpz_t e_acsl_cst_10 ; mpz_t e_acsl_cst_11 ; int e_acsl_cst_12 ;
mpz_init((__mpz_struct *)(e_acsl_cst_10));
mpz_set_si((__mpz_struct *)(e_acsl_cst_10),(long )123);
mpz_init((__mpz_struct *)(e_acsl_cst_11));
mpz_set_si((__mpz_struct *)(e_acsl_cst_11),(long )12);
e_acsl_cst_12 = mpz_cmp((__mpz_struct *)(e_acsl_cst_10),
(__mpz_struct *)(e_acsl_cst_11));
if (e_acsl_cst_12 < 0) { e_acsl_fail((char *)"((123 \342\211\245 12))");
} mpz_clear((__mpz_struct *)(e_acsl_cst_11));
mpz_clear((__mpz_struct *)(e_acsl_cst_10));
}
/*@ assert (0xff ≡ 0xff); */ ;
{ mpz_t e_acsl_cst_13 ; int e_acsl_cst_14 ;
mpz_init((__mpz_struct *)(e_acsl_cst_13));
mpz_set_si((__mpz_struct *)(e_acsl_cst_13),(long )0xff);
e_acsl_cst_14 = mpz_cmp((__mpz_struct *)(e_acsl_cst_13),
(__mpz_struct *)(e_acsl_cst_13));
if (e_acsl_cst_14 != 0) {
e_acsl_fail((char *)"((0xff \342\211\241 0xff))");
} mpz_clear((__mpz_struct *)(e_acsl_cst_13));
}
/*@ assert (1 ≢ 2); */ ;
{ mpz_t e_acsl_cst_15 ; mpz_t e_acsl_cst_16 ; int e_acsl_cst_17 ;
mpz_init((__mpz_struct *)(e_acsl_cst_15));
mpz_set_si((__mpz_struct *)(e_acsl_cst_15),(long )1);
mpz_init((__mpz_struct *)(e_acsl_cst_16));
mpz_set_si((__mpz_struct *)(e_acsl_cst_16),(long )2);
e_acsl_cst_17 = mpz_cmp((__mpz_struct *)(e_acsl_cst_15),
(__mpz_struct *)(e_acsl_cst_16));
if (e_acsl_cst_17 == 0) { e_acsl_fail((char *)"((1 \342\211\242 2))"); }
mpz_clear((__mpz_struct *)(e_acsl_cst_16));
mpz_clear((__mpz_struct *)(e_acsl_cst_15));
}
return;
}
src/plugins/e-acsl/visit.ml
+ 0
− 1
View file @ b17aeb16
......@@ -229,7 +229,6 @@ let rec term_to_exp is_global t = match t.term_node with
| Trange _ -> not_yet "range"
| Tlet _ -> not_yet "let binding"
(* [TODO] not fully test *)
let relation_to_revbinop = function
| Rlt -> Ge
| Rgt -> Le
......
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