Merge branch 'feature/tests/refactoring' into 'master'

[tests] New macro for the tests using Eva

See merge request frama-c/frama-c!2219

src/plugins/value/gen_test_config.sh

@@ -6,8 +6,8 @@
 # accordingly. The syntax for the root test_config files is as follows
 # (2 lines):
 #
-# MACRO: VALUECONFIG  <options inherited in all tests>
-# OPT: @VALUECONFIG@  <default options, inherited in tests that use STDOPT>
+# MACRO: EVA_CONFIG  <options inherited in all tests>
+# OPT: @EVA_CONFIG@  <default options, inherited in tests that use STDOPT>
 
 # All tested domains
 declare -a domains=(

tests/builtins/Longinit_sequencer.i

 /* run.config*
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
-OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -eva-show-progress -res-file @PTEST_RESULT@
+   EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+   OPT: @EVA_OPTIONS@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -res-file @PTEST_RESULT@
 */

tests/builtins/big_local_array.i

 /* run.config*
-EXECNOW: make -s @PTEST_DIR@/big_local_array_script.cmxs
-OPT: -eva-show-progress -print -journal-disable -eva -report
-OPT: -load-module @PTEST_DIR@/big_local_array_script -then-on prj -print -report
-OPT: -eva-show-progress -print -journal-disable -no-initialized-padding-locals -eva
+   EXECNOW: make -s @PTEST_DIR@/big_local_array_script.cmxs
+   OPT: @EVA_OPTIONS@ -print -journal-disable -eva -report
+   OPT: @EVA_OPTIONS@ -load-module @PTEST_DIR@/big_local_array_script -then-on prj -print -report
+   OPT: @EVA_OPTIONS@ -print -journal-disable -no-initialized-padding-locals -eva
 */
 
 struct S {

tests/builtins/diff_apron

 diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_apron/Longinit_sequencer.res.oracle
-323c323
+62,65c62,81
+< [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
+153,154c169,216
+< [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
+327c389
 <   tests/builtins/result/Longinit_sequencer.sav
 ---
 >   tests/builtins/result_apron/Longinit_sequencer.sav
-562c562
+421,424c483,498
+< [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
+568c642
 <   tests/builtins/result/Longinit_sequencer.sav
 ---
 >   tests/builtins/result_apron/Longinit_sequencer.sav
+658,661c732,747
+< [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

tests/builtins/diff_bitwise

 diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_bitwise/Longinit_sequencer.res.oracle
-323c323
+153,154c153,188
+< [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] 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 <- 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
+327c361
 <   tests/builtins/result/Longinit_sequencer.sav
 ---
 >   tests/builtins/result_bitwise/Longinit_sequencer.sav
-562c562
+568c602
 <   tests/builtins/result/Longinit_sequencer.sav
 ---
 >   tests/builtins/result_bitwise/Longinit_sequencer.sav

tests/builtins/diff_equalities

 diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_equalities/Longinit_sequencer.res.oracle
-323c323
+327c327
 <   tests/builtins/result/Longinit_sequencer.sav
 ---
 >   tests/builtins/result_equalities/Longinit_sequencer.sav
-562c562
+568c568
 <   tests/builtins/result/Longinit_sequencer.sav
 ---
 >   tests/builtins/result_equalities/Longinit_sequencer.sav

tests/builtins/diff_gauges

 diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_gauges/Longinit_sequencer.res.oracle
-323c323
+327c327
 <   tests/builtins/result/Longinit_sequencer.sav
 ---
 >   tests/builtins/result_gauges/Longinit_sequencer.sav
-562c562
+568c568
 <   tests/builtins/result/Longinit_sequencer.sav
 ---
 >   tests/builtins/result_gauges/Longinit_sequencer.sav

tests/builtins/diff_symblocs

 diff tests/builtins/oracle/Longinit_sequencer.res.oracle tests/builtins/oracle_symblocs/Longinit_sequencer.res.oracle
-323c323
+327c327
 <   tests/builtins/result/Longinit_sequencer.sav
 ---
 >   tests/builtins/result_symblocs/Longinit_sequencer.sav
-562c562
+568c568
 <   tests/builtins/result/Longinit_sequencer.sav
 ---
 >   tests/builtins/result_symblocs/Longinit_sequencer.sav

tests/builtins/from_result.c

 /* run.config*
-   OPT:  @VALUECONFIG@ -eva-no-builtins-auto -deps -journal-disable
+   OPT:  @EVA_CONFIG@ -eva-no-builtins-auto -deps -journal-disable
 */
 #define malloc(n) Frama_C_malloc_fresh(n)
 #include "../../share/libc/stdlib.c"

tests/builtins/malloc-deps.i

 /* run.config*
-   OPT: -eva @VALUECONFIG@ -deps -calldeps -inout -slevel 5 -eva-msg-key malloc
+   OPT: -eva @EVA_CONFIG@ -deps -calldeps -inout -slevel 5 -eva-msg-key malloc
 */
 //@ assigns \result \from \nothing;
 void *Frama_C_malloc_fresh(unsigned long n);

tests/builtins/malloc-size-zero.c

 /* run.config*
-   OPT: -eva @VALUECONFIG@ -eva-mlevel 3
-   OPT: -eva @VALUECONFIG@ -eva-malloc-functions my_calloc
+   OPT: -eva @EVA_CONFIG@ -eva-mlevel 3
+   OPT: -eva @EVA_CONFIG@ -eva-malloc-functions my_calloc
 */
 
 #include <stdlib.h>

tests/builtins/malloc.c

 /* run.config*
-   OPT: -eva @VALUECONFIG@ -slevel 10 -eva-mlevel 0
+   OPT: -eva @EVA_CONFIG@ -slevel 10 -eva-mlevel 0
 */
 
 void *Frama_C_malloc_by_stack(unsigned long i);

tests/builtins/malloc_bug_tr.c

 /* run.config*
-   OPT: -eva @VALUECONFIG@
+   OPT: -eva @EVA_CONFIG@
 */
 
 #include <stdlib.h>

tests/builtins/malloc_memexec.c

 /* run.config*
-   OPT: -eva @VALUECONFIG@ -eva-memexec -deps -inout -eva-mlevel 0
+   OPT: -eva @EVA_CONFIG@ -eva-memexec -deps -inout -eva-mlevel 0
 */
 
 //@ assigns \result;

tests/builtins/malloc_multiple.c

 /* run.config*
-   OPT: -eva @VALUECONFIG@ -slevel 50 -eva-mlevel 5
+   OPT: -eva @EVA_CONFIG@ -slevel 50 -eva-mlevel 5
 */
 #include<stdlib.h>
 #define MAX 10

tests/builtins/memcpy_invalid.c

 /* run.config*
-   OPT: -eva @VALUECONFIG@ -journal-disable -calldeps
+   OPT: -eva @EVA_CONFIG@ -journal-disable -calldeps
 */
 
 /*@ assigns \result \from min, max;

tests/builtins/oracle/Longinit_sequencer.res.oracle

@@ -79,6 +79,8 @@
 [eva] tests/builtins/long_init.c:77: Call to builtin free
 [eva] tests/builtins/long_init.c:77: 
   function free: precondition 'freeable' got status valid.
+[eva:malloc] tests/builtins/long_init.c:77: 
+  strong free on bases: {__malloc_init_inner_l75}
 [eva] Recording results for init_inner
 [eva] Done for function init_inner
 [eva:locals-escaping] tests/builtins/long_init.c:85: Warning: 
@@ -161,6 +163,8 @@
 [eva] tests/builtins/long_init.c:103: Call to builtin free
 [eva] tests/builtins/long_init.c:103: 
   function free: precondition 'freeable' got status valid.
+[eva:malloc] tests/builtins/long_init.c:103: 
+  strong free on bases: {__malloc_init_inner_l73}
 [eva] tests/builtins/long_init.c:104: 
   Call to builtin Frama_C_malloc_fresh for function malloc
 [eva] tests/builtins/long_init.c:104: allocating variable __malloc_main_l104
@@ -435,6 +439,8 @@ Values at end of function main:
 [eva] tests/builtins/long_init2.c:103: Call to builtin free
 [eva] tests/builtins/long_init2.c:103: 
   function free: precondition 'freeable' got status valid.
+[eva:malloc] tests/builtins/long_init2.c:103: 
+  strong free on bases: {__malloc_init_inner_l73}
 [eva] tests/builtins/long_init2.c:104: 
   Call to builtin Frama_C_malloc_fresh for function malloc
 [eva] tests/builtins/long_init2.c:104: allocating variable __malloc_main_l104
@@ -670,6 +676,8 @@ Values at end of function main:
 [eva] tests/builtins/long_init3.c:103: Call to builtin free
 [eva] tests/builtins/long_init3.c:103: 
   function free: precondition 'freeable' got status valid.
+[eva:malloc] tests/builtins/long_init3.c:103: 
+  strong free on bases: {__malloc_init_inner_l73}
 [eva] tests/builtins/long_init3.c:104: 
   Call to builtin Frama_C_malloc_fresh for function malloc
 [eva] tests/builtins/long_init3.c:104: allocating variable __malloc_main_l104

tests/builtins/test_config

-MACRO: VALUECONFIG -eva-show-progress  -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps

tests/builtins/test_config_apron

-MACRO: VALUECONFIG -eva-show-progress  -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-apron-oct -eva-msg-key experimental-ok
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-apron-oct -eva-msg-key experimental-ok
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps

tests/builtins/test_config_bitwise

-MACRO: VALUECONFIG -eva-show-progress  -no-autoload-plugins -load-module from,inout,eva,scope,variadic -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-bitwise-domain
-OPT: -eva @VALUECONFIG@ -journal-disable -out -input -deps
+MACRO: EVA_OPTIONS @EVA_OPTIONS@ -eva-msg-key malloc -eva-warn-key malloc:weak=feedback -eva-no-alloc-returns-null -eva-bitwise-domain
+MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic
+OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps