Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
35b4442f
Commit
35b4442f
authored
Mar 13, 2020
by
David Bühler
Committed by
Andre Maroneze
Apr 06, 2020
Browse files
[Eva] Updates test oracles.
parent
014fffbd
Changes
6
Hide whitespace changes
Inline
Side-by-side
tests/value/numerors/oracle/numerors.res.oracle
View file @
35b4442f
[eva:experimental] Warning: The numerors domain is experimental.
[kernel] Parsing tests/value/numerors/numerors.c (with preprocessing)
[kernel:parser:decimal-float] tests/value/numerors/numerors.c:24: Warning:
Floating-point constant 0.69314718056 is not represented exactly. Will use 0x1.62e42fefa3bdcp-1.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[kernel:typing:implicit-function-declaration] tests/value/numerors/numerors.c:246: Warning:
Calling undeclared function DPRINTFrama_C_domain_show_each_ex10. Old style K&R code?
[eva:experimental] Warning: The numerors domain is experimental.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
...
...
@@ -298,7 +298,7 @@
In these functions, 257 statements reached (out of 257): 100% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
by the Eva analyzer: 0 errors
0
warning
s
by the Eva analyzer: 0 errors
1
warning
by the Frama-C kernel: 0 errors 3 warnings
----------------------------------------------------------------------------
0 alarms generated by the analysis.
...
...
tests/value/traces/oracle/test1.res.oracle
View file @
35b4442f
[eva:experimental] Warning: The traces domain is experimental.
[kernel] Parsing tests/value/traces/test1.c (with preprocessing)
[eva:experimental] Warning: The traces domain is experimental.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
...
...
tests/value/traces/oracle/test2.res.oracle
View file @
35b4442f
[eva:experimental] Warning: The traces domain is experimental.
[kernel] Parsing tests/value/traces/test2.i (no preprocessing)
[eva:experimental] Warning: The traces domain is experimental.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
...
...
tests/value/traces/oracle/test3.res.oracle
View file @
35b4442f
[eva:experimental] Warning: The traces domain is experimental.
[kernel] Parsing tests/value/traces/test3.i (no preprocessing)
[eva:experimental] Warning: The traces domain is experimental.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
...
...
tests/value/traces/oracle/test4.res.oracle
View file @
35b4442f
[eva:experimental] Warning: The traces domain is experimental.
[kernel] Parsing tests/value/traces/test4.i (no preprocessing)
[eva:experimental] Warning: The traces domain is experimental.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
...
...
tests/value/traces/oracle/test5.res.oracle
View file @
35b4442f
[eva:experimental] Warning: The traces domain is experimental.
[kernel] Parsing tests/value/traces/test5.i (no preprocessing)
[kernel:typing:implicit-function-declaration] tests/value/traces/test5.i:21: Warning:
Calling undeclared function my_switch. Old style K&R code?
[eva:experimental] Warning: The traces domain is experimental.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment