diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle index 7929e983b04e9e8e371a8591ede0504a6e4bbfc5..f2bae8ef88f912808c1881370fc97938448ea63d 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle @@ -7,5 +7,3 @@ tests/bts/bts1307.i:11:[e-acsl] warning: approximating a real number by a float [e-acsl] translation done in project "e-acsl". FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown. [value] user error: type long double not implemented. Using double instead -tests/bts/bts1307.i:23:[value] warning: function bar, behavior UnderEstimate_Motoring: postcondition got status unknown. -tests/bts/bts1307.i:23:[value] warning: function __gen_e_acsl_bar, behavior UnderEstimate_Motoring: postcondition got status unknown. diff --git a/src/plugins/e-acsl/tests/runtime/oracle/lazy.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/lazy.res.oracle index 8fc4269b3fa64eaff06d093a1ca5fe26f1813889..c33737e3cac6e74853111a99a2a4002b6a9d7094 100644 --- a/src/plugins/e-acsl/tests/runtime/oracle/lazy.res.oracle +++ b/src/plugins/e-acsl/tests/runtime/oracle/lazy.res.oracle @@ -1,6 +1,3 @@ [e-acsl] beginning translation. FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype [e-acsl] translation done in project "e-acsl". -tests/runtime/lazy.i:15:[value] warning: assertion got status unknown. -tests/runtime/lazy.i:16:[value] warning: assertion got status unknown. -tests/runtime/lazy.i:17:[value] warning: assertion got status unknown.