From 61253b7fd1fd435ec76aba1e216e0fb4cb9827ec Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Thu, 10 Aug 2023 11:39:43 +0200 Subject: [PATCH] [Eva] Adds test of -eva-flamegraph. --- tests/value/oracle/show_perf.res.oracle | 40 +++++++++---------- tests/value/oracle_apron/show_perf.res.oracle | 36 ++++++++--------- tests/value/show_perf.i | 5 ++- 3 files changed, 42 insertions(+), 39 deletions(-) diff --git a/tests/value/oracle/show_perf.res.oracle b/tests/value/oracle/show_perf.res.oracle index 7202898ac5..511d75fbce 100644 --- a/tests/value/oracle/show_perf.res.oracle +++ b/tests/value/oracle/show_perf.res.oracle @@ -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:41. + Called from show_perf.i:44. [eva] computing for function collatz <- print_collatz <- main. - Called from show_perf.i:35. + Called from show_perf.i:38. [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:36: Reusing old results for call to collatz -[eva] show_perf.i:37: Frama_C_show_each: {7}, {16}, {52} +[eva] show_perf.i:39: 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 diff --git a/tests/value/oracle_apron/show_perf.res.oracle b/tests/value/oracle_apron/show_perf.res.oracle index d997f5e393..e00947e9f8 100644 --- a/tests/value/oracle_apron/show_perf.res.oracle +++ b/tests/value/oracle_apron/show_perf.res.oracle @@ -1,70 +1,70 @@ 77c77,144 -< [eva] show_perf.i:36: Reusing old results for call to collatz +< [eva] show_perf.i:39: Reusing old results for call to collatz --- > [eva] computing for function collatz <- print_collatz <- main. -> Called from show_perf.i:36. +> Called from show_perf.i:39. > [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 diff --git a/tests/value/show_perf.i b/tests/value/show_perf.i index 5dc541cc95..f37e9d7b80 100644 --- a/tests/value/show_perf.i +++ b/tests/value/show_perf.i @@ -1,10 +1,13 @@ /* 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; -- GitLab