From 0ae70c2ece0fe5f5077b584ebc99419f5bb3d95d Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 24 Jan 2022 18:29:46 +0100
Subject: [PATCH] [tests] minor changes
---
tests/float/absorb.c | 10 +++++++---
tests/float/oracle/absorb_sav.res | 2 +-
tests/float/oracle/absorb_sav2.res | 6 +++---
3 files changed, 11 insertions(+), 7 deletions(-)
diff --git a/tests/float/absorb.c b/tests/float/absorb.c
index 656a6b9bc1e..731eed760a3 100644
--- a/tests/float/absorb.c
+++ b/tests/float/absorb.c
@@ -1,22 +1,26 @@
/* run.config
COMMENT: run.config is intentionally not-*
-PLUGIN:
+ PLUGIN:
EXECNOW: BIN absorb.sav LOG absorb_sav.res LOG absorb_sav.err @frama-c@ -save @PTEST_RESULT@/absorb.sav @PTEST_FILE@ > @PTEST_RESULT@/absorb_sav.res 2> @PTEST_RESULT@/absorb_sav.err
-PLUGIN: @EVA_PLUGINS@
+ PLUGIN: @EVA_PLUGINS@
EXECNOW: BIN absorb.sav2 LOG absorb_sav2.res LOG absorb_sav2.err @frama-c@ -load %{dep:@PTEST_RESULT@/absorb.sav} -eva @EVA_CONFIG@ -float-hex -save @PTEST_RESULT@/absorb.sav2 > @PTEST_RESULT@/absorb_sav2.res 2> @PTEST_RESULT@/absorb_sav2.err
+ COMMENT: CMD: @frama-c@ @PTEST_OPTIONS@
OPT: -load %{dep:@PTEST_RESULT@/absorb.sav2} -deps -out -input
*/
/* run.config*
DONTRUN:
*/
+
#include "__fc_builtin.h"
+
float x = 1.0, y = 0.0, z, t, min_f, min_fl, den;
+
void main() {
long long b = Frama_C_interval(-2000000001, 2000000001);
b = b * b;
z = y + 1e-286;
while (y != x)
- {
+ {
y = x ; x+=1E-286;
}
t = b;
diff --git a/tests/float/oracle/absorb_sav.res b/tests/float/oracle/absorb_sav.res
index a618fee603c..280a79a32b2 100644
--- a/tests/float/oracle/absorb_sav.res
+++ b/tests/float/oracle/absorb_sav.res
@@ -1,4 +1,4 @@
[kernel] Parsing absorb.c (with preprocessing)
-[kernel:parser:decimal-float] absorb.c:17: Warning:
+[kernel:parser:decimal-float] absorb.c:21: Warning:
Floating-point constant 1e-286 is not represented exactly. Will use 0x1.e74404f3daadbp-951.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
diff --git a/tests/float/oracle/absorb_sav2.res b/tests/float/oracle/absorb_sav2.res
index 0e6e5f6ef81..b34d714dc2c 100644
--- a/tests/float/oracle/absorb_sav2.res
+++ b/tests/float/oracle/absorb_sav2.res
@@ -10,12 +10,12 @@
min_fl ∈ {0}
den ∈ {0}
[eva] computing for function Frama_C_interval <- main.
- Called from absorb.c:15.
+ Called from absorb.c:19.
[eva] using specification for function Frama_C_interval
-[eva] absorb.c:15:
+[eva] absorb.c:19:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
-[eva] absorb.c:18: starting to merge loop iterations
+[eva] absorb.c:22: starting to merge loop iterations
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
--
GitLab