From b21cf242453bc2d14fb7e95998b982a15d9fcce4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Tue, 8 Dec 2020 15:42:48 +0100 Subject: [PATCH] [Eva] Updates alternative oracles: the test Longinit_sequencer.i has been removed. --- tests/builtins/diff_apron | 131 --------------------------------- tests/builtins/diff_bitwise | 9 --- tests/builtins/diff_equalities | 9 --- tests/builtins/diff_gauges | 9 --- tests/builtins/diff_octagons | 9 --- tests/builtins/diff_symblocs | 9 --- 6 files changed, 176 deletions(-) diff --git a/tests/builtins/diff_apron b/tests/builtins/diff_apron index 138fb410e26..befd75c34a2 100644 --- a/tests/builtins/diff_apron +++ b/tests/builtins/diff_apron @@ -1,134 +1,3 @@ -diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_apron/Longinit_sequencer.res.oracle -59,62c59,78 -< [eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze -< [eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze -< [eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze -< [eva] tests/builtins/long_init.c:29: Reusing old results for call to subanalyze ---- -> [eva] computing for function subanalyze <- analyze <- init_inner <- init_outer <- -> main. -> Called from tests/builtins/long_init.c:29. -> [eva] Recording results for subanalyze -> [eva] Done for function subanalyze -> [eva] computing for function subanalyze <- analyze <- init_inner <- init_outer <- -> main. -> Called from tests/builtins/long_init.c:29. -> [eva] Recording results for subanalyze -> [eva] Done for function subanalyze -> [eva] computing for function subanalyze <- analyze <- init_inner <- init_outer <- -> main. -> Called from tests/builtins/long_init.c:29. -> [eva] Recording results for subanalyze -> [eva] Done for function subanalyze -> [eva] computing for function subanalyze <- analyze <- init_inner <- init_outer <- -> main. -> Called from tests/builtins/long_init.c:29. -> [eva] Recording results for subanalyze -> [eva] Done for function subanalyze -148,149c164,211 -< [eva] tests/builtins/long_init.c:93: Reusing old results for call to analyze -< [eva] tests/builtins/long_init.c:94: Reusing old results for call to analyze ---- -> [eva] computing for function analyze <- main. -> Called from tests/builtins/long_init.c:93. -> [eva] computing for function subanalyze <- analyze <- main. -> Called from tests/builtins/long_init.c:29. -> [eva] Recording results for subanalyze -> [eva] Done for function subanalyze -> [eva] computing for function subanalyze <- analyze <- main. -> Called from tests/builtins/long_init.c:29. -> [eva] Recording results for subanalyze -> [eva] Done for function subanalyze -> [eva] computing for function subanalyze <- analyze <- main. -> Called from tests/builtins/long_init.c:29. -> [eva] Recording results for subanalyze -> [eva] Done for function subanalyze -> [eva] computing for function subanalyze <- analyze <- main. -> Called from tests/builtins/long_init.c:29. -> [eva] Recording results for subanalyze -> [eva] Done for function subanalyze -> [eva] computing for function subanalyze <- analyze <- main. -> Called from tests/builtins/long_init.c:29. -> [eva] Recording results for subanalyze -> [eva] Done for function subanalyze -> [eva] Recording results for analyze -> [eva] Done for function analyze -> [eva] computing for function analyze <- main. -> Called from tests/builtins/long_init.c:94. -> [eva] computing for function subanalyze <- analyze <- main. -> Called from tests/builtins/long_init.c:29. -> [eva] Recording results for subanalyze -> [eva] Done for function subanalyze -> [eva] computing for function subanalyze <- analyze <- main. -> Called from tests/builtins/long_init.c:29. -> [eva] Recording results for subanalyze -> [eva] Done for function subanalyze -> [eva] computing for function subanalyze <- analyze <- main. -> Called from tests/builtins/long_init.c:29. -> [eva] Recording results for subanalyze -> [eva] Done for function subanalyze -> [eva] computing for function subanalyze <- analyze <- main. -> Called from tests/builtins/long_init.c:29. -> [eva] Recording results for subanalyze -> [eva] Done for function subanalyze -> [eva] computing for function subanalyze <- analyze <- main. -> Called from tests/builtins/long_init.c:29. -> [eva] Recording results for subanalyze -> [eva] Done for function subanalyze -> [eva] Recording results for analyze -> [eva] Done for function analyze -320c382 -< tests/builtins/result/Longinit_sequencer.sav ---- -> tests/builtins/result_apron/Longinit_sequencer.sav -411,414c473,488 -< [eva] tests/builtins/long_init2.c:29: Reusing old results for call to subanalyze -< [eva] tests/builtins/long_init2.c:29: Reusing old results for call to subanalyze -< [eva] tests/builtins/long_init2.c:29: Reusing old results for call to subanalyze -< [eva] tests/builtins/long_init2.c:29: Reusing old results for call to subanalyze ---- -> [eva] computing for function subanalyze <- analyze <- main. -> Called from tests/builtins/long_init2.c:29. -> [eva] Recording results for subanalyze -> [eva] Done for function subanalyze -> [eva] computing for function subanalyze <- analyze <- main. -> Called from tests/builtins/long_init2.c:29. -> [eva] Recording results for subanalyze -> [eva] Done for function subanalyze -> [eva] computing for function subanalyze <- analyze <- main. -> Called from tests/builtins/long_init2.c:29. -> [eva] Recording results for subanalyze -> [eva] Done for function subanalyze -> [eva] computing for function subanalyze <- analyze <- main. -> Called from tests/builtins/long_init2.c:29. -> [eva] Recording results for subanalyze -> [eva] Done for function subanalyze -556c630 -< tests/builtins/result/Longinit_sequencer.sav ---- -> tests/builtins/result_apron/Longinit_sequencer.sav -643,646c717,732 -< [eva] tests/builtins/long_init3.c:29: Reusing old results for call to subanalyze -< [eva] tests/builtins/long_init3.c:29: Reusing old results for call to subanalyze -< [eva] tests/builtins/long_init3.c:29: Reusing old results for call to subanalyze -< [eva] tests/builtins/long_init3.c:29: Reusing old results for call to subanalyze ---- -> [eva] computing for function subanalyze <- analyze <- main. -> Called from tests/builtins/long_init3.c:29. -> [eva] Recording results for subanalyze -> [eva] Done for function subanalyze -> [eva] computing for function subanalyze <- analyze <- main. -> Called from tests/builtins/long_init3.c:29. -> [eva] Recording results for subanalyze -> [eva] Done for function subanalyze -> [eva] computing for function subanalyze <- analyze <- main. -> Called from tests/builtins/long_init3.c:29. -> [eva] Recording results for subanalyze -> [eva] Done for function subanalyze -> [eva] computing for function subanalyze <- analyze <- main. -> Called from tests/builtins/long_init3.c:29. -> [eva] Recording results for subanalyze -> [eva] Done for function subanalyze diff tests/builtins/oracle/allocated.0.res.oracle tests/builtins/oracle_apron/allocated.0.res.oracle 260a261,263 > [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc diff --git a/tests/builtins/diff_bitwise b/tests/builtins/diff_bitwise index e2e2efc04cf..98cc819af46 100644 --- a/tests/builtins/diff_bitwise +++ b/tests/builtins/diff_bitwise @@ -1,12 +1,3 @@ -diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_bitwise/Longinit_sequencer.res.oracle -320c320 -< tests/builtins/result/Longinit_sequencer.sav ---- -> tests/builtins/result_bitwise/Longinit_sequencer.sav -556c556 -< tests/builtins/result/Longinit_sequencer.sav ---- -> tests/builtins/result_bitwise/Longinit_sequencer.sav diff tests/builtins/oracle/allocated.0.res.oracle tests/builtins/oracle_bitwise/allocated.0.res.oracle 260a261,263 > [eva] tests/builtins/allocated.c:127: Call to builtin __fc_vla_alloc diff --git a/tests/builtins/diff_equalities b/tests/builtins/diff_equalities index 3956b94f249..45b1a53ba88 100644 --- a/tests/builtins/diff_equalities +++ b/tests/builtins/diff_equalities @@ -1,12 +1,3 @@ -diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_equalities/Longinit_sequencer.res.oracle -320c320 -< tests/builtins/result/Longinit_sequencer.sav ---- -> tests/builtins/result_equalities/Longinit_sequencer.sav -556c556 -< tests/builtins/result/Longinit_sequencer.sav ---- -> tests/builtins/result_equalities/Longinit_sequencer.sav diff tests/builtins/oracle/alloc_weak.res.oracle tests/builtins/oracle_equalities/alloc_weak.res.oracle 36,37d35 < [eva:alarm] tests/builtins/alloc_weak.c:30: Warning: diff --git a/tests/builtins/diff_gauges b/tests/builtins/diff_gauges index ca4a1580fa4..aed43a80b45 100644 --- a/tests/builtins/diff_gauges +++ b/tests/builtins/diff_gauges @@ -1,12 +1,3 @@ -diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_gauges/Longinit_sequencer.res.oracle -320c320 -< tests/builtins/result/Longinit_sequencer.sav ---- -> tests/builtins/result_gauges/Longinit_sequencer.sav -556c556 -< tests/builtins/result/Longinit_sequencer.sav ---- -> tests/builtins/result_gauges/Longinit_sequencer.sav diff tests/builtins/oracle/linked_list.0.res.oracle tests/builtins/oracle_gauges/linked_list.0.res.oracle 1122a1123,1128 > [eva] computing for function printf_va_1 <- main. diff --git a/tests/builtins/diff_octagons b/tests/builtins/diff_octagons index c2b18889ac5..d091e1809e5 100644 --- a/tests/builtins/diff_octagons +++ b/tests/builtins/diff_octagons @@ -1,12 +1,3 @@ -diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_octagons/Longinit_sequencer.res.oracle -320c320 -< tests/builtins/result/Longinit_sequencer.sav ---- -> tests/builtins/result_octagons/Longinit_sequencer.sav -556c556 -< tests/builtins/result/Longinit_sequencer.sav ---- -> tests/builtins/result_octagons/Longinit_sequencer.sav diff tests/builtins/oracle/allocated.0.res.oracle tests/builtins/oracle_octagons/allocated.0.res.oracle 273c273 < j ∈ [1..2147483647] diff --git a/tests/builtins/diff_symblocs b/tests/builtins/diff_symblocs index f640a0f7322..f1bda9cc8ce 100644 --- a/tests/builtins/diff_symblocs +++ b/tests/builtins/diff_symblocs @@ -1,12 +1,3 @@ -diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_symblocs/Longinit_sequencer.res.oracle -320c320 -< tests/builtins/result/Longinit_sequencer.sav ---- -> tests/builtins/result_symblocs/Longinit_sequencer.sav -556c556 -< tests/builtins/result/Longinit_sequencer.sav ---- -> tests/builtins/result_symblocs/Longinit_sequencer.sav diff tests/builtins/oracle/alloc_weak.res.oracle tests/builtins/oracle_symblocs/alloc_weak.res.oracle 36,37d35 < [eva:alarm] tests/builtins/alloc_weak.c:30: Warning: -- GitLab