Skip to content
Snippets Groups Projects
Commit f6d069d4 authored by Boris Yakobowski's avatar Boris Yakobowski
Browse files

Fix test currently broken

(See frama-c/e-acsl!169)
parent dce66325
No related branches found
No related tags found
No related merge requests found
...@@ -20,7 +20,7 @@ int main(void) { ...@@ -20,7 +20,7 @@ int main(void) {
/* heterogeneous casts from/to integers */ /* heterogeneous casts from/to integers */
int t[2] = { 0, 1 }; int t[2] = { 0, 1 };
/*@ assert (float)x == t[(int)0.1]; */ /*@ assert (float)x == (float)t[(int)0.1]; */
return 0; return 0;
} }
...@@ -16,6 +16,4 @@ tests/gmp/cast.i:23:[e-acsl] warning: approximating a real number by a float ...@@ -16,6 +16,4 @@ tests/gmp/cast.i:23:[e-acsl] warning: approximating a real number by a float
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308] __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
[value] using specification for function __e_acsl_memory_init [value] using specification for function __e_acsl_memory_init
[value] using specification for function __e_acsl_assert [value] using specification for function __e_acsl_assert
[value] user error: type long double wider than 64 bits not supported.
Using double instead for the remainder of the analysis.
[value] done for function main [value] done for function main
...@@ -23,8 +23,6 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: preco ...@@ -23,8 +23,6 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: preco
[value] using specification for function __gmpz_clear [value] using specification for function __gmpz_clear
[value] using specification for function __gmpz_get_ui [value] using specification for function __gmpz_get_ui
[value] using specification for function __gmpz_init_set_ui [value] using specification for function __gmpz_init_set_ui
[value] user error: type long double wider than 64 bits not supported.
Using double instead for the remainder of the analysis.
tests/gmp/cast.i:23:[value] warning: accessing out of bounds index. assert 0 ≤ __gen_e_acsl_cast_9; tests/gmp/cast.i:23:[value] warning: accessing out of bounds index. assert 0 ≤ __gen_e_acsl_cast_9;
tests/gmp/cast.i:23:[value] warning: accessing out of bounds index. assert __gen_e_acsl_cast_9 < 2; tests/gmp/cast.i:23:[value] warning: accessing out of bounds index. assert __gen_e_acsl_cast_9 < 2;
[value] done for function main [value] done for function main
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment