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
61253b7f
Commit
61253b7f
authored
1 year ago
by
David Bühler
Committed by
Andre Maroneze
2 months ago
Browse files
Options
Downloads
Patches
Plain Diff
[Eva] Adds test of -eva-flamegraph.
parent
e4ae43c2
No related branches found
Branches containing commit
No related tags found
No related merge requests found
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
tests/value/oracle/show_perf.res.oracle
+20
-20
20 additions, 20 deletions
tests/value/oracle/show_perf.res.oracle
tests/value/oracle_apron/show_perf.res.oracle
+18
-18
18 additions, 18 deletions
tests/value/oracle_apron/show_perf.res.oracle
tests/value/show_perf.i
+4
-1
4 additions, 1 deletion
tests/value/show_perf.i
with
42 additions
and
39 deletions
tests/value/oracle/show_perf.res.oracle
+
20
−
20
View file @
61253b7f
...
...
@@ -5,77 +5,77 @@
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
[eva] computing for function print_collatz <- main.
Called from show_perf.i:4
1
.
Called from show_perf.i:4
4
.
[eva] computing for function collatz <- print_collatz <- main.
Called from show_perf.i:3
5
.
Called from show_perf.i:3
8
.
[eva] computing for function compute_next <- collatz <- print_collatz <- main.
Called from show_perf.i:
28
.
Called from show_perf.i:
31
.
[eva] Recording results for compute_next
[eva] Done for function compute_next
[eva] computing for function compute_next <- collatz <- print_collatz <- main.
Called from show_perf.i:
28
.
Called from show_perf.i:
31
.
[eva] Recording results for compute_next
[eva] Done for function compute_next
[eva] computing for function compute_next <- collatz <- print_collatz <- main.
Called from show_perf.i:
28
.
Called from show_perf.i:
31
.
[eva] Recording results for compute_next
[eva] Done for function compute_next
[eva] computing for function compute_next <- collatz <- print_collatz <- main.
Called from show_perf.i:
28
.
Called from show_perf.i:
31
.
[eva] Recording results for compute_next
[eva] Done for function compute_next
[eva] computing for function compute_next <- collatz <- print_collatz <- main.
Called from show_perf.i:
28
.
Called from show_perf.i:
31
.
[eva] Recording results for compute_next
[eva] Done for function compute_next
[eva] computing for function compute_next <- collatz <- print_collatz <- main.
Called from show_perf.i:
28
.
Called from show_perf.i:
31
.
[eva] Recording results for compute_next
[eva] Done for function compute_next
[eva] computing for function compute_next <- collatz <- print_collatz <- main.
Called from show_perf.i:
28
.
Called from show_perf.i:
31
.
[eva] Recording results for compute_next
[eva] Done for function compute_next
[eva] computing for function compute_next <- collatz <- print_collatz <- main.
Called from show_perf.i:
28
.
Called from show_perf.i:
31
.
[eva] Recording results for compute_next
[eva] Done for function compute_next
[eva] computing for function compute_next <- collatz <- print_collatz <- main.
Called from show_perf.i:
28
.
Called from show_perf.i:
31
.
[eva] Recording results for compute_next
[eva] Done for function compute_next
[eva] computing for function compute_next <- collatz <- print_collatz <- main.
Called from show_perf.i:
28
.
Called from show_perf.i:
31
.
[eva] Recording results for compute_next
[eva] Done for function compute_next
[eva] computing for function compute_next <- collatz <- print_collatz <- main.
Called from show_perf.i:
28
.
Called from show_perf.i:
31
.
[eva] Recording results for compute_next
[eva] Done for function compute_next
[eva] computing for function compute_next <- collatz <- print_collatz <- main.
Called from show_perf.i:
28
.
Called from show_perf.i:
31
.
[eva] Recording results for compute_next
[eva] Done for function compute_next
[eva] computing for function compute_next <- collatz <- print_collatz <- main.
Called from show_perf.i:
28
.
Called from show_perf.i:
31
.
[eva] Recording results for compute_next
[eva] Done for function compute_next
[eva] computing for function compute_next <- collatz <- print_collatz <- main.
Called from show_perf.i:
28
.
Called from show_perf.i:
31
.
[eva] Recording results for compute_next
[eva] Done for function compute_next
[eva] computing for function compute_next <- collatz <- print_collatz <- main.
Called from show_perf.i:
28
.
Called from show_perf.i:
31
.
[eva] Recording results for compute_next
[eva] Done for function compute_next
[eva] computing for function compute_next <- collatz <- print_collatz <- main.
Called from show_perf.i:
28
.
Called from show_perf.i:
31
.
[eva] Recording results for compute_next
[eva] Done for function compute_next
[eva] Recording results for collatz
[eva] Done for function collatz
[eva] show_perf.i:3
6
: Reusing old results for call to collatz
[eva] show_perf.i:
37
: Frama_C_show_each: {7}, {16}, {52}
[eva] show_perf.i:3
9
: Reusing old results for call to collatz
[eva] show_perf.i:
40
: Frama_C_show_each: {7}, {16}, {52}
[eva] Recording results for print_collatz
[eva] Done for function print_collatz
[eva] Recording results for main
...
...
This diff is collapsed.
Click to expand it.
tests/value/oracle_apron/show_perf.res.oracle
+
18
−
18
View file @
61253b7f
77c77,144
< [eva] show_perf.i:3
6
: Reusing old results for call to collatz
< [eva] show_perf.i:3
9
: Reusing old results for call to collatz
---
> [eva] computing for function collatz <- print_collatz <- main.
> Called from show_perf.i:3
6
.
> Called from show_perf.i:3
9
.
> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
> Called from show_perf.i:
28
.
> Called from show_perf.i:
31
.
> [eva] Recording results for compute_next
> [eva] Done for function compute_next
> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
> Called from show_perf.i:
28
.
> Called from show_perf.i:
31
.
> [eva] Recording results for compute_next
> [eva] Done for function compute_next
> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
> Called from show_perf.i:
28
.
> Called from show_perf.i:
31
.
> [eva] Recording results for compute_next
> [eva] Done for function compute_next
> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
> Called from show_perf.i:
28
.
> Called from show_perf.i:
31
.
> [eva] Recording results for compute_next
> [eva] Done for function compute_next
> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
> Called from show_perf.i:
28
.
> Called from show_perf.i:
31
.
> [eva] Recording results for compute_next
> [eva] Done for function compute_next
> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
> Called from show_perf.i:
28
.
> Called from show_perf.i:
31
.
> [eva] Recording results for compute_next
> [eva] Done for function compute_next
> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
> Called from show_perf.i:
28
.
> Called from show_perf.i:
31
.
> [eva] Recording results for compute_next
> [eva] Done for function compute_next
> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
> Called from show_perf.i:
28
.
> Called from show_perf.i:
31
.
> [eva] Recording results for compute_next
> [eva] Done for function compute_next
> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
> Called from show_perf.i:
28
.
> Called from show_perf.i:
31
.
> [eva] Recording results for compute_next
> [eva] Done for function compute_next
> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
> Called from show_perf.i:
28
.
> Called from show_perf.i:
31
.
> [eva] Recording results for compute_next
> [eva] Done for function compute_next
> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
> Called from show_perf.i:
28
.
> Called from show_perf.i:
31
.
> [eva] Recording results for compute_next
> [eva] Done for function compute_next
> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
> Called from show_perf.i:
28
.
> Called from show_perf.i:
31
.
> [eva] Recording results for compute_next
> [eva] Done for function compute_next
> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
> Called from show_perf.i:
28
.
> Called from show_perf.i:
31
.
> [eva] Recording results for compute_next
> [eva] Done for function compute_next
> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
> Called from show_perf.i:
28
.
> Called from show_perf.i:
31
.
> [eva] Recording results for compute_next
> [eva] Done for function compute_next
> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
> Called from show_perf.i:
28
.
> Called from show_perf.i:
31
.
> [eva] Recording results for compute_next
> [eva] Done for function compute_next
> [eva] computing for function compute_next <- collatz <- print_collatz <- main.
> Called from show_perf.i:
28
.
> Called from show_perf.i:
31
.
> [eva] Recording results for compute_next
> [eva] Done for function compute_next
> [eva] Recording results for collatz
...
...
This diff is collapsed.
Click to expand it.
tests/value/show_perf.i
+
4
−
1
View file @
61253b7f
/* run.config*
FILTER: sed -e 's/\([0-9.]\+\(%\|s\)\)/?\2/g'
STDOPT: +"-eva-show-perf"
EXECNOW: BIN flamegraph.txt BIN flamegraph.err { PTESTS_TESTING=1 %{bin:frama-c} @PTEST_FILE@ -eva -eva-flamegraph flamegraph.txt && NOGUI=1 %{bin:frama-c-script} flamegraph flamegraph.txt; } 1> /dev/null 2> flamegraph.err
*/
/* This example is kept minimal to ensure the stability of the output
of -eva-show-perf. */
of -eva-show-perf on the first run.
The second run only tests that the flamegraph generated by -eva-flamegraph
is valid. */
volatile
int
nondet
;
...
...
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