From 1d415e2b9228af3b85e90e7a9ec007c9498dcee6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Sat, 9 Dec 2017 09:42:27 +0100 Subject: [PATCH] Fixes an oracle wrt frama-c!1571. By default, rte now emits is_finite alarms which are not yet supported. --- .../e-acsl/tests/bts/oracle/bts1307.res.oracle | 12 ++++++++++++ 1 file changed, 12 insertions(+) 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 8be072503ca..2d258527e20 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle @@ -1,7 +1,19 @@ tests/bts/bts1307.i:14:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float [e-acsl] beginning translation. tests/bts/bts1307.i:23:[e-acsl] warning: approximating a real number by a float +tests/bts/bts1307.i:23:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. + Ignoring annotation. tests/bts/bts1307.i:23:[e-acsl] warning: approximating a real number by a float +tests/bts/bts1307.i:23:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. + Ignoring annotation. tests/bts/bts1307.i:11:[e-acsl] warning: approximating a real number by a float +tests/bts/bts1307.i:11:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. + Ignoring annotation. +tests/bts/bts1307.i:11:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. + Ignoring annotation. +tests/bts/bts1307.i:11:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. + Ignoring annotation. +tests/bts/bts1307.i:11:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported. + Ignoring annotation. [e-acsl] translation done in project "e-acsl". FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown. -- GitLab