diff --git a/src/plugins/e-acsl/tests/gmp/cast.i b/src/plugins/e-acsl/tests/gmp/cast.i index 700d338841e3c8b337bbf333ed40279312eb8e21..3b014c861aded0bf4ab25b8890056633155615ce 100644 --- a/src/plugins/e-acsl/tests/gmp/cast.i +++ b/src/plugins/e-acsl/tests/gmp/cast.i @@ -20,7 +20,7 @@ int main(void) { /* heterogeneous casts from/to integers */ int t[2] = { 0, 1 }; - /*@ assert (float)x == t[(int)0.1]; */ + /*@ assert (float)x == (float)t[(int)0.1]; */ return 0; } diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle index 560ddd4e17b9118068f868734e6d6ae93c9d01cd..c7d593ec80cc2411e52c34eda81414905ba26cf7 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle @@ -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] [value] using specification for function __e_acsl_memory_init [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 diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle index 23514bf035f716bdbb120e743dfd1e96614cf312..d4f8dd847ac145e43086a00a13cc9697343d5498 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle @@ -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_get_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 __gen_e_acsl_cast_9 < 2; [value] done for function main