From 02c586ee37ec13576ca2e690647bda1ea9c42464 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Thu, 4 Apr 2019 11:16:33 +0200 Subject: [PATCH] [Eva] Do not print the summary in Frama-C tests. As it is redundant with all the information displayed during the analysis. --- src/plugins/nonterm/tests/test_config | 2 +- src/plugins/variadic/tests/test_config | 2 +- tests/idct/ieee_1180_1990.c | 2 +- tests/test_config | 2 +- tests/test_config_apron | 2 +- tests/test_config_bitwise | 2 +- tests/test_config_equalities | 2 +- tests/test_config_gauges | 2 +- tests/test_config_symblocs | 2 +- 9 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/plugins/nonterm/tests/test_config b/src/plugins/nonterm/tests/test_config index 32af2023751..1d678ae3e1a 100644 --- a/src/plugins/nonterm/tests/test_config +++ b/src/plugins/nonterm/tests/test_config @@ -1 +1 @@ -OPT: -no-autoload-plugins -load-module from,inout,nonterm,scope -val -val-show-progress -then -nonterm -nonterm-verbose 2 +OPT: -no-autoload-plugins -load-module from,inout,nonterm,scope -val -val-show-progress -eva-msg-key=-summary -then -nonterm -nonterm-verbose 2 diff --git a/src/plugins/variadic/tests/test_config b/src/plugins/variadic/tests/test_config index 70aafaf12a6..9d83090791b 100644 --- a/src/plugins/variadic/tests/test_config +++ b/src/plugins/variadic/tests/test_config @@ -1 +1 @@ -OPT: -no-autoload-plugins -load-module from,inout,eva,variadic,scope -check -print -kernel-verbose 0 -variadic-verbose 2 -eva -slevel 10 -eva-msg-key=-initial-state -eva-no-show-progress -eva-print +OPT: -no-autoload-plugins -load-module from,inout,eva,variadic,scope -check -print -kernel-verbose 0 -variadic-verbose 2 -eva -slevel 10 -eva-msg-key=-initial-state,-summary -eva-no-show-progress -eva-print diff --git a/tests/idct/ieee_1180_1990.c b/tests/idct/ieee_1180_1990.c index 1f0f4325eeb..6c5b0285d74 100644 --- a/tests/idct/ieee_1180_1990.c +++ b/tests/idct/ieee_1180_1990.c @@ -1,6 +1,6 @@ /* run.config* GCC: - STDOPT: +"-load-module report,scope,variadic -float-normal -no-warn-signed-overflow tests/idct/idct.c -remove-redundant-alarms -eva-memexec -eva-builtin sqrt:Frama_C_sqrt,cos:Frama_C_cos -then -report -report-print-properties" + STDOPT: +"-eva-msg-key=summary -load-module report,scope,variadic -float-normal -no-warn-signed-overflow tests/idct/idct.c -remove-redundant-alarms -eva-memexec -eva-builtin sqrt:Frama_C_sqrt,cos:Frama_C_cos -then -report -report-print-properties" */ /* IEEE_1180_1990: a testbed for IDCT accuracy * Copyright (C) 2001 Renaud Pacalet diff --git a/tests/test_config b/tests/test_config index 10fa9a74e56..6efe608ac84 100644 --- a/tests/test_config +++ b/tests/test_config @@ -1,3 +1,3 @@ -MACRO: EVA_OPTIONS -eva-show-progress +MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary MACRO: EVA_CONFIG @EVA_OPTIONS@ -no-autoload-plugins -load-module from,inout,eva,scope,variadic OPT: -eva @EVA_CONFIG@ -journal-disable -out -input -deps diff --git a/tests/test_config_apron b/tests/test_config_apron index ccb5342259c..2d6cff1926f 100644 --- a/tests/test_config_apron +++ b/tests/test_config_apron @@ -1,3 +1,3 @@ -MACRO: EVA_OPTIONS -eva-show-progress -eva-apron-oct -eva-msg-key experimental-ok +MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -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 diff --git a/tests/test_config_bitwise b/tests/test_config_bitwise index 146e7721ea2..7e1be236655 100644 --- a/tests/test_config_bitwise +++ b/tests/test_config_bitwise @@ -1,3 +1,3 @@ -MACRO: EVA_OPTIONS -eva-show-progress -eva-bitwise-domain +MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -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 diff --git a/tests/test_config_equalities b/tests/test_config_equalities index 1e592c46e5c..d84a7e2a8b2 100644 --- a/tests/test_config_equalities +++ b/tests/test_config_equalities @@ -1,3 +1,3 @@ -MACRO: EVA_OPTIONS -eva-show-progress -eva-equality-domain +MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-equality-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 diff --git a/tests/test_config_gauges b/tests/test_config_gauges index 7e0fb7cbdac..b6a460ae1e4 100644 --- a/tests/test_config_gauges +++ b/tests/test_config_gauges @@ -1,3 +1,3 @@ -MACRO: EVA_OPTIONS -eva-show-progress -eva-gauges-domain +MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-gauges-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 diff --git a/tests/test_config_symblocs b/tests/test_config_symblocs index 77ad2e24740..47ce23088d4 100644 --- a/tests/test_config_symblocs +++ b/tests/test_config_symblocs @@ -1,3 +1,3 @@ -MACRO: EVA_OPTIONS -eva-show-progress -eva-symbolic-locations-domain +MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-symbolic-locations-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 -- GitLab