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

[tests] extended test for floats

parent d396efac
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/tests/gmp/oracle/gen_reals.c
+ 10
− 7
View file @ 64410979
...@@ -74,6 +74,9 @@ int main(void) ...@@ -74,6 +74,9 @@ int main(void)
(char *)"main",(char *)"0.1 == 0.1",16); (char *)"main",(char *)"0.1 == 0.1",16);
__gmpq_clear(__gen_e_acsl__6); __gmpq_clear(__gen_e_acsl__6);
} }
/*@ assert (double)1.0 ≡ 1.0; */
__e_acsl_assert(1. == 1.,(char *)"Assertion",(char *)"main",
(char *)"(double)1.0 == 1.0",17);
/*@ assert (double)0.1 ≢ 0.1; */ /*@ assert (double)0.1 ≢ 0.1; */
{ {
__e_acsl_mpq_t __gen_e_acsl__7; __e_acsl_mpq_t __gen_e_acsl__7;
...@@ -89,7 +92,7 @@ int main(void) ...@@ -89,7 +92,7 @@ int main(void)
__gen_e_acsl_ne_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__9), __gen_e_acsl_ne_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__9),
(__e_acsl_mpq_struct const *)(__gen_e_acsl__7)); (__e_acsl_mpq_struct const *)(__gen_e_acsl__7));
__e_acsl_assert(__gen_e_acsl_ne_2 != 0,(char *)"Assertion", __e_acsl_assert(__gen_e_acsl_ne_2 != 0,(char *)"Assertion",
(char *)"main",(char *)"(double)0.1 != 0.1",17); (char *)"main",(char *)"(double)0.1 != 0.1",18);
__gmpq_clear(__gen_e_acsl__7); __gmpq_clear(__gen_e_acsl__7);
__gmpq_clear(__gen_e_acsl__9); __gmpq_clear(__gen_e_acsl__9);
} }
...@@ -108,7 +111,7 @@ int main(void) ...@@ -108,7 +111,7 @@ int main(void)
*/ */
__e_acsl_assert((double)((float)__gen_e_acsl__11) != __gen_e_acsl__12, __e_acsl_assert((double)((float)__gen_e_acsl__11) != __gen_e_acsl__12,
(char *)"Assertion",(char *)"main", (char *)"Assertion",(char *)"main",
(char *)"(float)0.1 != (double)0.1",18); (char *)"(float)0.1 != (double)0.1",19);
__gmpq_clear(__gen_e_acsl__10); __gmpq_clear(__gen_e_acsl__10);
} }
/*@ assert (double)1.1 ≢ 1 + 0.1; */ /*@ assert (double)1.1 ≢ 1 + 0.1; */
...@@ -137,7 +140,7 @@ int main(void) ...@@ -137,7 +140,7 @@ int main(void)
__gen_e_acsl_ne_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__17), __gen_e_acsl_ne_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__17),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_2)); (__e_acsl_mpq_struct const *)(__gen_e_acsl_add_2));
__e_acsl_assert(__gen_e_acsl_ne_3 != 0,(char *)"Assertion", __e_acsl_assert(__gen_e_acsl_ne_3 != 0,(char *)"Assertion",
(char *)"main",(char *)"(double)1.1 != 1 + 0.1",19); (char *)"main",(char *)"(double)1.1 != 1 + 0.1",20);
__gmpq_clear(__gen_e_acsl__13); __gmpq_clear(__gen_e_acsl__13);
__gmpq_clear(__gen_e_acsl__15); __gmpq_clear(__gen_e_acsl__15);
__gmpq_clear(__gen_e_acsl__16); __gmpq_clear(__gen_e_acsl__16);
...@@ -172,7 +175,7 @@ int main(void) ...@@ -172,7 +175,7 @@ int main(void)
__gen_e_acsl_eq_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_add_3), __gen_e_acsl_eq_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_add_3),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_sub)); (__e_acsl_mpq_struct const *)(__gen_e_acsl_sub));
__e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion", __e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
(char *)"main",(char *)"1 + 0.1 == 2 - 0.9",20); (char *)"main",(char *)"1 + 0.1 == 2 - 0.9",21);
__gmpq_clear(__gen_e_acsl__18); __gmpq_clear(__gen_e_acsl__18);
__gmpq_clear(__gen_e_acsl__19); __gmpq_clear(__gen_e_acsl__19);
__gmpq_clear(__gen_e_acsl_add_3); __gmpq_clear(__gen_e_acsl_add_3);
...@@ -203,7 +206,7 @@ int main(void) ...@@ -203,7 +206,7 @@ int main(void)
__gen_e_acsl_ne_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__23), __gen_e_acsl_ne_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__23),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_mul)); (__e_acsl_mpq_struct const *)(__gen_e_acsl_mul));
__e_acsl_assert(__gen_e_acsl_ne_4 != 0,(char *)"Assertion", __e_acsl_assert(__gen_e_acsl_ne_4 != 0,(char *)"Assertion",
(char *)"main",(char *)"sum != x * y",24); (char *)"main",(char *)"sum != x * y",25);
__gmpq_clear(__gen_e_acsl_y); __gmpq_clear(__gen_e_acsl_y);
__gmpq_clear(__gen_e_acsl__22); __gmpq_clear(__gen_e_acsl__22);
__gmpq_clear(__gen_e_acsl_mul); __gmpq_clear(__gen_e_acsl_mul);
...@@ -231,7 +234,7 @@ int main(void) ...@@ -231,7 +234,7 @@ int main(void)
__gen_e_acsl_eq_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__24), __gen_e_acsl_eq_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__24),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_4)); (__e_acsl_mpq_struct const *)(__gen_e_acsl_add_4));
__e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion", __e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",
(char *)"main",(char *)"\\let n = 1; 4 == n + 3.0",25); (char *)"main",(char *)"\\let n = 1; 4 == n + 3.0",26);
__gmpq_clear(__gen_e_acsl__24); __gmpq_clear(__gen_e_acsl__24);
__gmpq_clear(__gen_e_acsl__25); __gmpq_clear(__gen_e_acsl__25);
__gmpq_clear(__gen_e_acsl__26); __gmpq_clear(__gen_e_acsl__26);
...@@ -259,7 +262,7 @@ int main(void) ...@@ -259,7 +262,7 @@ int main(void)
__gen_e_acsl_ne_5 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__29), __gen_e_acsl_ne_5 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__29),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_5)); (__e_acsl_mpq_struct const *)(__gen_e_acsl_add_5));
__e_acsl_assert(__gen_e_acsl_ne_5 != 0,(char *)"Assertion", __e_acsl_assert(__gen_e_acsl_ne_5 != 0,(char *)"Assertion",
(char *)"main",(char *)"1.1d != 1 + 0.1",31); (char *)"main",(char *)"1.1d != 1 + 0.1",32);
__gmpq_clear(__gen_e_acsl__27); __gmpq_clear(__gen_e_acsl__27);
__gmpq_clear(__gen_e_acsl__28); __gmpq_clear(__gen_e_acsl__28);
__gmpq_clear(__gen_e_acsl_add_5); __gmpq_clear(__gen_e_acsl_add_5);
......
src/plugins/e-acsl/tests/gmp/oracle/gen_reals2.c
+ 10
− 7
View file @ 64410979
...@@ -74,6 +74,9 @@ int main(void) ...@@ -74,6 +74,9 @@ int main(void)
(char *)"main",(char *)"0.1 == 0.1",16); (char *)"main",(char *)"0.1 == 0.1",16);
__gmpq_clear(__gen_e_acsl__6); __gmpq_clear(__gen_e_acsl__6);
} }
/*@ assert (double)1.0 ≡ 1.0; */
__e_acsl_assert(1. == 1.,(char *)"Assertion",(char *)"main",
(char *)"(double)1.0 == 1.0",17);
/*@ assert (double)0.1 ≢ 0.1; */ /*@ assert (double)0.1 ≢ 0.1; */
{ {
__e_acsl_mpq_t __gen_e_acsl__7; __e_acsl_mpq_t __gen_e_acsl__7;
...@@ -89,7 +92,7 @@ int main(void) ...@@ -89,7 +92,7 @@ int main(void)
__gen_e_acsl_ne_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__9), __gen_e_acsl_ne_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__9),
(__e_acsl_mpq_struct const *)(__gen_e_acsl__7)); (__e_acsl_mpq_struct const *)(__gen_e_acsl__7));
__e_acsl_assert(__gen_e_acsl_ne_2 != 0,(char *)"Assertion", __e_acsl_assert(__gen_e_acsl_ne_2 != 0,(char *)"Assertion",
(char *)"main",(char *)"(double)0.1 != 0.1",17); (char *)"main",(char *)"(double)0.1 != 0.1",18);
__gmpq_clear(__gen_e_acsl__7); __gmpq_clear(__gen_e_acsl__7);
__gmpq_clear(__gen_e_acsl__9); __gmpq_clear(__gen_e_acsl__9);
} }
...@@ -108,7 +111,7 @@ int main(void) ...@@ -108,7 +111,7 @@ int main(void)
*/ */
__e_acsl_assert((double)((float)__gen_e_acsl__11) != __gen_e_acsl__12, __e_acsl_assert((double)((float)__gen_e_acsl__11) != __gen_e_acsl__12,
(char *)"Assertion",(char *)"main", (char *)"Assertion",(char *)"main",
(char *)"(float)0.1 != (double)0.1",18); (char *)"(float)0.1 != (double)0.1",19);
__gmpq_clear(__gen_e_acsl__10); __gmpq_clear(__gen_e_acsl__10);
} }
/*@ assert (double)1.1 ≢ 1 + 0.1; */ /*@ assert (double)1.1 ≢ 1 + 0.1; */
...@@ -137,7 +140,7 @@ int main(void) ...@@ -137,7 +140,7 @@ int main(void)
__gen_e_acsl_ne_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__17), __gen_e_acsl_ne_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__17),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_2)); (__e_acsl_mpq_struct const *)(__gen_e_acsl_add_2));
__e_acsl_assert(__gen_e_acsl_ne_3 != 0,(char *)"Assertion", __e_acsl_assert(__gen_e_acsl_ne_3 != 0,(char *)"Assertion",
(char *)"main",(char *)"(double)1.1 != 1 + 0.1",19); (char *)"main",(char *)"(double)1.1 != 1 + 0.1",20);
__gmpq_clear(__gen_e_acsl__13); __gmpq_clear(__gen_e_acsl__13);
__gmpq_clear(__gen_e_acsl__15); __gmpq_clear(__gen_e_acsl__15);
__gmpq_clear(__gen_e_acsl__16); __gmpq_clear(__gen_e_acsl__16);
...@@ -172,7 +175,7 @@ int main(void) ...@@ -172,7 +175,7 @@ int main(void)
__gen_e_acsl_eq_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_add_3), __gen_e_acsl_eq_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_add_3),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_sub)); (__e_acsl_mpq_struct const *)(__gen_e_acsl_sub));
__e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion", __e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
(char *)"main",(char *)"1 + 0.1 == 2 - 0.9",20); (char *)"main",(char *)"1 + 0.1 == 2 - 0.9",21);
__gmpq_clear(__gen_e_acsl__18); __gmpq_clear(__gen_e_acsl__18);
__gmpq_clear(__gen_e_acsl__19); __gmpq_clear(__gen_e_acsl__19);
__gmpq_clear(__gen_e_acsl_add_3); __gmpq_clear(__gen_e_acsl_add_3);
...@@ -203,7 +206,7 @@ int main(void) ...@@ -203,7 +206,7 @@ int main(void)
__gen_e_acsl_ne_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__23), __gen_e_acsl_ne_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__23),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_mul)); (__e_acsl_mpq_struct const *)(__gen_e_acsl_mul));
__e_acsl_assert(__gen_e_acsl_ne_4 != 0,(char *)"Assertion", __e_acsl_assert(__gen_e_acsl_ne_4 != 0,(char *)"Assertion",
(char *)"main",(char *)"sum != x * y",24); (char *)"main",(char *)"sum != x * y",25);
__gmpq_clear(__gen_e_acsl_y); __gmpq_clear(__gen_e_acsl_y);
__gmpq_clear(__gen_e_acsl__22); __gmpq_clear(__gen_e_acsl__22);
__gmpq_clear(__gen_e_acsl_mul); __gmpq_clear(__gen_e_acsl_mul);
...@@ -231,7 +234,7 @@ int main(void) ...@@ -231,7 +234,7 @@ int main(void)
__gen_e_acsl_eq_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__24), __gen_e_acsl_eq_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__24),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_4)); (__e_acsl_mpq_struct const *)(__gen_e_acsl_add_4));
__e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion", __e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",
(char *)"main",(char *)"\\let n = 1; 4 == n + 3.0",25); (char *)"main",(char *)"\\let n = 1; 4 == n + 3.0",26);
__gmpq_clear(__gen_e_acsl__24); __gmpq_clear(__gen_e_acsl__24);
__gmpq_clear(__gen_e_acsl__25); __gmpq_clear(__gen_e_acsl__25);
__gmpq_clear(__gen_e_acsl__26); __gmpq_clear(__gen_e_acsl__26);
...@@ -259,7 +262,7 @@ int main(void) ...@@ -259,7 +262,7 @@ int main(void)
__gen_e_acsl_ne_5 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__29), __gen_e_acsl_ne_5 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__29),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_5)); (__e_acsl_mpq_struct const *)(__gen_e_acsl_add_5));
__e_acsl_assert(__gen_e_acsl_ne_5 != 0,(char *)"Assertion", __e_acsl_assert(__gen_e_acsl_ne_5 != 0,(char *)"Assertion",
(char *)"main",(char *)"1.1d != 1 + 0.1",31); (char *)"main",(char *)"1.1d != 1 + 0.1",32);
__gmpq_clear(__gen_e_acsl__27); __gmpq_clear(__gen_e_acsl__27);
__gmpq_clear(__gen_e_acsl__28); __gmpq_clear(__gen_e_acsl__28);
__gmpq_clear(__gen_e_acsl_add_5); __gmpq_clear(__gen_e_acsl_add_5);
......
src/plugins/e-acsl/tests/gmp/oracle/reals.0.res.oracle
+ 19
− 19
View file @ 64410979
[kernel:parser:decimal-float] tests/gmp/reals.c:21: Warning: [kernel:parser:decimal-float] tests/gmp/reals.c:22: Warning:
Floating-point constant 0.2f is not represented exactly. Will use 0x1.99999a0000000p-3. Floating-point constant 0.2f is not represented exactly. Will use 0x1.99999a0000000p-3.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted) (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[e-acsl] beginning translation. [e-acsl] beginning translation.
[e-acsl] Warning: R to float: double rounding might cause unsoundness [e-acsl] Warning: R to float: double rounding might cause unsoundness
[e-acsl] tests/gmp/reals.c:18: Warning: [e-acsl] tests/gmp/reals.c:19: Warning:
E-ACSL construct `predicate with no definition nor reads clause' E-ACSL construct `predicate with no definition nor reads clause'
is not yet supported. is not yet supported.
Ignoring annotation. Ignoring annotation.
...@@ -33,35 +33,35 @@ ...@@ -33,35 +33,35 @@
[eva:alarm] tests/gmp/reals.c:16: Warning: assertion got status unknown. [eva:alarm] tests/gmp/reals.c:16: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/reals.c:16: Warning: [eva:alarm] tests/gmp/reals.c:16: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:17: Warning: assertion got status unknown. [eva:alarm] tests/gmp/reals.c:18: Warning: assertion got status unknown.
[eva] using specification for function __gmpq_get_d [eva] using specification for function __gmpq_get_d
[eva:alarm] tests/gmp/reals.c:17: Warning: [eva:alarm] tests/gmp/reals.c:18: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__8); non-finite double value. assert \is_finite(__gen_e_acsl__8);
[eva:alarm] tests/gmp/reals.c:17: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:18: Warning: [eva:alarm] tests/gmp/reals.c:18: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:19: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__11); non-finite double value. assert \is_finite(__gen_e_acsl__11);
[eva:alarm] tests/gmp/reals.c:18: Warning: [eva:alarm] tests/gmp/reals.c:19: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__12); non-finite double value. assert \is_finite(__gen_e_acsl__12);
[eva:alarm] tests/gmp/reals.c:18: Warning:
non-finite float value. assert \is_finite((float)__gen_e_acsl__11);
[eva:alarm] tests/gmp/reals.c:18: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:19: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/reals.c:19: Warning: [eva:alarm] tests/gmp/reals.c:19: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__14); non-finite float value. assert \is_finite((float)__gen_e_acsl__11);
[eva:alarm] tests/gmp/reals.c:19: Warning: [eva:alarm] tests/gmp/reals.c:19: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:20: Warning: assertion got status unknown. [eva:alarm] tests/gmp/reals.c:20: Warning: assertion got status unknown.
[eva] using specification for function __gmpq_sub [eva:alarm] tests/gmp/reals.c:20: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__14);
[eva:alarm] tests/gmp/reals.c:20: Warning: [eva:alarm] tests/gmp/reals.c:20: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:21: Warning: assertion got status unknown.
[eva] using specification for function __gmpq_sub
[eva:alarm] tests/gmp/reals.c:21: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __gmpq_mul [eva] using specification for function __gmpq_mul
[eva:alarm] tests/gmp/reals.c:24: Warning: [eva:alarm] tests/gmp/reals.c:25: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:25: Warning: assertion got status unknown. [eva:alarm] tests/gmp/reals.c:26: Warning: assertion got status unknown.
[eva] using specification for function __gmpq_set_si [eva] using specification for function __gmpq_set_si
[eva:alarm] tests/gmp/reals.c:25: Warning: [eva:alarm] tests/gmp/reals.c:26: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __gmpq_set [eva] using specification for function __gmpq_set
[eva] using specification for function __gmpq_div [eva] using specification for function __gmpq_div
...@@ -69,7 +69,7 @@ ...@@ -69,7 +69,7 @@
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:6: Warning: [eva:alarm] tests/gmp/reals.c:6: Warning:
function __gen_e_acsl_avg: postcondition got status unknown. function __gen_e_acsl_avg: postcondition got status unknown.
[eva:alarm] tests/gmp/reals.c:31: Warning: assertion got status unknown. [eva:alarm] tests/gmp/reals.c:32: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/reals.c:31: Warning: [eva:alarm] tests/gmp/reals.c:32: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva] done for function main [eva] done for function main
src/plugins/e-acsl/tests/gmp/oracle/reals.1.res.oracle
+ 19
− 19
View file @ 64410979
[kernel:parser:decimal-float] tests/gmp/reals.c:21: Warning: [kernel:parser:decimal-float] tests/gmp/reals.c:22: Warning:
Floating-point constant 0.2f is not represented exactly. Will use 0x1.99999a0000000p-3. Floating-point constant 0.2f is not represented exactly. Will use 0x1.99999a0000000p-3.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted) (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[e-acsl] beginning translation. [e-acsl] beginning translation.
[e-acsl] Warning: R to float: double rounding might cause unsoundness [e-acsl] Warning: R to float: double rounding might cause unsoundness
[e-acsl] tests/gmp/reals.c:18: Warning: [e-acsl] tests/gmp/reals.c:19: Warning:
E-ACSL construct `predicate with no definition nor reads clause' E-ACSL construct `predicate with no definition nor reads clause'
is not yet supported. is not yet supported.
Ignoring annotation. Ignoring annotation.
...@@ -33,35 +33,35 @@ ...@@ -33,35 +33,35 @@
[eva:alarm] tests/gmp/reals.c:16: Warning: assertion got status unknown. [eva:alarm] tests/gmp/reals.c:16: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/reals.c:16: Warning: [eva:alarm] tests/gmp/reals.c:16: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:17: Warning: assertion got status unknown. [eva:alarm] tests/gmp/reals.c:18: Warning: assertion got status unknown.
[eva] using specification for function __gmpq_get_d [eva] using specification for function __gmpq_get_d
[eva:alarm] tests/gmp/reals.c:17: Warning: [eva:alarm] tests/gmp/reals.c:18: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__8); non-finite double value. assert \is_finite(__gen_e_acsl__8);
[eva:alarm] tests/gmp/reals.c:17: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:18: Warning: [eva:alarm] tests/gmp/reals.c:18: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:19: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__11); non-finite double value. assert \is_finite(__gen_e_acsl__11);
[eva:alarm] tests/gmp/reals.c:18: Warning: [eva:alarm] tests/gmp/reals.c:19: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__12); non-finite double value. assert \is_finite(__gen_e_acsl__12);
[eva:alarm] tests/gmp/reals.c:18: Warning:
non-finite float value. assert \is_finite((float)__gen_e_acsl__11);
[eva:alarm] tests/gmp/reals.c:18: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:19: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/reals.c:19: Warning: [eva:alarm] tests/gmp/reals.c:19: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__14); non-finite float value. assert \is_finite((float)__gen_e_acsl__11);
[eva:alarm] tests/gmp/reals.c:19: Warning: [eva:alarm] tests/gmp/reals.c:19: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:20: Warning: assertion got status unknown. [eva:alarm] tests/gmp/reals.c:20: Warning: assertion got status unknown.
[eva] using specification for function __gmpq_sub [eva:alarm] tests/gmp/reals.c:20: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__14);
[eva:alarm] tests/gmp/reals.c:20: Warning: [eva:alarm] tests/gmp/reals.c:20: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:21: Warning: assertion got status unknown.
[eva] using specification for function __gmpq_sub
[eva:alarm] tests/gmp/reals.c:21: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __gmpq_mul [eva] using specification for function __gmpq_mul
[eva:alarm] tests/gmp/reals.c:24: Warning: [eva:alarm] tests/gmp/reals.c:25: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:25: Warning: assertion got status unknown. [eva:alarm] tests/gmp/reals.c:26: Warning: assertion got status unknown.
[eva] using specification for function __gmpq_set_si [eva] using specification for function __gmpq_set_si
[eva:alarm] tests/gmp/reals.c:25: Warning: [eva:alarm] tests/gmp/reals.c:26: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __gmpq_set [eva] using specification for function __gmpq_set
[eva] using specification for function __gmpq_div [eva] using specification for function __gmpq_div
...@@ -69,7 +69,7 @@ ...@@ -69,7 +69,7 @@
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:6: Warning: [eva:alarm] tests/gmp/reals.c:6: Warning:
function __gen_e_acsl_avg: postcondition got status unknown. function __gen_e_acsl_avg: postcondition got status unknown.
[eva:alarm] tests/gmp/reals.c:31: Warning: assertion got status unknown. [eva:alarm] tests/gmp/reals.c:32: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/reals.c:31: Warning: [eva:alarm] tests/gmp/reals.c:32: Warning:
function __e_acsl_assert: precondition got status unknown. function __e_acsl_assert: precondition got status unknown.
[eva] done for function main [eva] done for function main
src/plugins/e-acsl/tests/gmp/reals.c
+ 1
− 0
View file @ 64410979
...@@ -14,6 +14,7 @@ int main(void) { ...@@ -14,6 +14,7 @@ int main(void) {
/*@ assert 3 != 1.5; */ ; /*@ assert 3 != 1.5; */ ;
/*@ assert 3 == 1.5 + 1.5; */ ; /*@ assert 3 == 1.5 + 1.5; */ ;
/*@ assert 0.1 == 0.1; */ ; /*@ assert 0.1 == 0.1; */ ;
/*@ assert (double)1.0 == 1.0; */ ;
/*@ assert (double)0.1 != 0.1; */ ; /*@ assert (double)0.1 != 0.1; */ ;
/*@ assert (float)0.1 != (double)0.1; */ ; /*@ assert (float)0.1 != (double)0.1; */ ;
/*@ assert (double)1.1 != 1 + 0.1 ;*/ ; /*@ assert (double)1.1 != 1 + 0.1 ;*/ ;
......
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