Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
44c1e708
Commit
44c1e708
authored
3 years ago
by
David Bühler
Browse files
Options
Downloads
Patches
Plain Diff
[Eva] Fixes some tests.
parent
b7f2779f
No related branches found
No related tags found
No related merge requests found
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
tests/value/memexec.c
+2
-2
2 additions, 2 deletions
tests/value/memexec.c
tests/value/oracle/summary.4.res.oracle
+3
-3
3 additions, 3 deletions
tests/value/oracle/summary.4.res.oracle
tests/value/summary.i
+2
-2
2 additions, 2 deletions
tests/value/summary.i
with
7 additions
and
7 deletions
tests/value/memexec.c
+
2
−
2
View file @
44c1e708
/* run.config*
/* run.config*
STDOPT: +"-rte-select fbug @RTE_TEST@ -then -eva"
PLUGIN: @PTEST_PLUGIN@ rtegen
STDOPT: #"-machdep x86_32 -rte-select fbug @RTE_TEST@ -then -eva"
*/
*/
int
x1
,
y1
,
z1
,
z2
;
volatile
int
c
,
nondet
;
int
x1
,
y1
,
z1
,
z2
;
volatile
int
c
,
nondet
;
void
f11
()
{
void
f11
()
{
...
...
This diff is collapsed.
Click to expand it.
tests/value/oracle/summary.4.res.oracle
+
3
−
3
View file @
44c1e708
[kernel] Warning: -slevel is a deprecated alias for option -eva-slevel.
Please use -eva-slevel instead.
[kernel] Parsing summary.i (no preprocessing)
[kernel] Parsing summary.i (no preprocessing)
[rte:annot] annotating function alarms
[rte:annot] annotating function alarms
[rte:annot] annotating function bottom
[rte:annot] annotating function bottom
...
@@ -8,6 +6,8 @@
...
@@ -8,6 +6,8 @@
[rte:annot] annotating function logic
[rte:annot] annotating function logic
[rte:annot] annotating function main
[rte:annot] annotating function main
[rte:annot] annotating function minimal
[rte:annot] annotating function minimal
[kernel] Warning: -slevel is a deprecated alias for option -eva-slevel.
Please use -eva-slevel instead.
[eva] Analyzing a complete application starting at main
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Computing initial state
[eva] Initial state computed
[eva] Initial state computed
...
@@ -107,7 +107,7 @@
...
@@ -107,7 +107,7 @@
----------------------------------------------------------------------------
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
Some errors and warnings have been raised during the analysis:
by the Eva analyzer: 0 errors 1 warning
by the Eva analyzer: 0 errors 1 warning
by the Frama-C kernel: 0 errors
2
warnings
by the Frama-C kernel: 0 errors
3
warnings
----------------------------------------------------------------------------
----------------------------------------------------------------------------
18 alarms generated by the analysis:
18 alarms generated by the analysis:
3 invalid memory accesses
3 invalid memory accesses
...
...
This diff is collapsed.
Click to expand it.
tests/value/summary.i
+
2
−
2
View file @
44c1e708
...
@@ -3,8 +3,8 @@
...
@@ -3,8 +3,8 @@
STDOPT: +"-eva-msg-key=summary -main minimal"
STDOPT: +"-eva-msg-key=summary -main minimal"
STDOPT: +"-eva-msg-key=summary -main bottom"
STDOPT: +"-eva-msg-key=summary -main bottom"
STDOPT: +"-eva-msg-key=summary -main main"
STDOPT: +"-eva-msg-key=summary -main main"
PLUGIN: @PTEST_PLUGIN@ rtegen
PLUGIN: @PTEST_PLUGIN@ rtegen
STD
OPT:
+"@RTE
_TEST@ -eva-msg-key=summary -main main -slevel 0
"
OPT:
-machdep x86_32 @RTE_TEST@ -then @EVA
_TEST@ -eva-msg-key=summary -main main -slevel 0
*/
*/
/* Tests the summary on the smallest possible program. */
/* Tests the summary on the smallest possible program. */
void
minimalist
()
;
void
minimalist
()
;
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment