Skip to content
Snippets Groups Projects
Commit 0ae70c2e authored by Patrick Baudin's avatar Patrick Baudin Committed by Andre Maroneze
Browse files

[tests] minor changes

parent 940ee266
No related branches found
No related tags found
No related merge requests found
/* 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;
......
[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)
......@@ -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 ======
......
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