Skip to content
Snippets Groups Projects
Commit 1d415e2b authored by David Bühler's avatar David Bühler
Browse files

Fixes an oracle wrt frama-c!1571.

By default, rte now emits is_finite alarms which are not yet supported.
parent 9a76ed4d
No related branches found
No related tags found
No related merge requests found
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.
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