diff --git a/tests/value/oracle/show_perf.res.oracle b/tests/value/oracle/show_perf.res.oracle index 7202898ac5f97bb37eb7d77c0a90812a8ea69265..511d75fbce0f7e17de7b69486622af124f2b07bd 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 d997f5e393fedd50e967c0a6c88ddee0434a8b7b..e00947e9f838d930475745273ef6d19b64e82c24 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 5dc541cc95aced5397ce982acb34806eff4c9344..f37e9d7b80c1b7a5b6bbe9f098727b9400e43350 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;