From 8a6cf288ab9d85c537dc49b9f629ffee6a91168b Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.oliveiramaroneze@cea.fr> Date: Mon, 9 Jan 2017 10:03:38 +0100 Subject: [PATCH] synchronize with frama-c/frama-c!1104 --- src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle | 2 -- src/plugins/e-acsl/tests/runtime/oracle/lazy.res.oracle | 3 --- 2 files changed, 5 deletions(-) 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 7929e983b04..f2bae8ef88f 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 8fc4269b3fa..c33737e3cac 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. -- GitLab