From e9aad68373d3fa3fbb03aa93378edc42115c4272 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 10 May 2022 15:14:08 +0200
Subject: [PATCH] [tests] update tests according to removed journal
---
ptests/ptests.ml | 2 +-
share/Makefile.config.in | 2 +-
.../tests/sarif/oracle/cwe125.sarif | 15 ++++++---------
.../tests/sarif/oracle/std_string.sarif | 5 ++---
.../tests/sarif/oracle/with-libc.sarif | 5 ++---
.../tests/sarif/oracle/without-libc.sarif | 5 ++---
src/plugins/wp/tests/wp/wp_call_pre.c | 2 +-
src/plugins/wp/tests/wp/wp_strategy.c | 6 +++---
src/plugins/wp/tests/wp_acsl/struct_use_case.i | 8 ++++----
tests/sparecode/test_config | 2 +-
tests/spec/test_config | 2 +-
11 files changed, 24 insertions(+), 30 deletions(-)
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index cbd6875ae3d..d797d5076b8 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -355,7 +355,7 @@ let exclude s = exclude_suites := s :: !exclude_suites
let macro_post_options = ref "" (* value set to @PTEST_POST_OPTIONS@ macro *)
let macro_pre_options = ref "" (* value set to @PTEST_PRE_OPTIONS@ macro *)
let macro_options = ref "@PTEST_PRE_OPTIONS@ @PTEST_OPT@ @PTEST_POST_OPTIONS@"
-let macro_default_options = ref "-journal-disable -check -no-autoload-plugins"
+let macro_default_options = ref "-check -no-autoload-plugins"
let macro_frama_c_cmd = ref "@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@"
let macro_frama_c = ref "@frama-c-exe@ @PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@"
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index c6d808f04e9..cab716c2a97 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
@@ -163,7 +163,7 @@ HAVE_BUILTIN_VA_LIST ?=@HAVE_BUILTIN_VA_LIST@
# test directories for ptests configuration
# Non-plugin test directories containing some ML files to compile
TEST_DIRS_AS_PLUGIN:=\
- dynamic journal saveload spec misc syntax cil \
+ dynamic saveload spec misc syntax cil \
pretty_printing builtins libc value
ifeq ($(HAS_PYTHON36),yes)
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif b/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif
index 3769a8fc34c..24925531385 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif
@@ -16,10 +16,9 @@
"invocations": [
{
"commandLine":
- "frama-c -journal-disable -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report cwe125.c -save ./cwe125_parse.sav",
+ "frama-c -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report cwe125.c -save ./cwe125_parse.sav",
"arguments": [
- "-journal-disable", "-check", "-no-autoload-plugins",
- "-add-symbolic-path", ":.",
+ "-check", "-no-autoload-plugins", "-add-symbolic-path", ":.",
"-load-module=eva,from,scope,markdown_report", "cwe125.c",
"-save", "./cwe125_parse.sav"
],
@@ -28,10 +27,9 @@
},
{
"commandLine":
- "frama-c -journal-disable -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report -load ./cwe125_parse.sav -eva -save ./cwe125_eva.sav",
+ "frama-c -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report -load ./cwe125_parse.sav -eva -save ./cwe125_eva.sav",
"arguments": [
- "-journal-disable", "-check", "-no-autoload-plugins",
- "-add-symbolic-path", ":.",
+ "-check", "-no-autoload-plugins", "-add-symbolic-path", ":.",
"-load-module=eva,from,scope,markdown_report", "-load",
"./cwe125_parse.sav", "-eva", "-save", "./cwe125_eva.sav"
],
@@ -40,10 +38,9 @@
},
{
"commandLine":
- "frama-c -journal-disable -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report -load ./cwe125_eva.sav -then -mdr-out ./cwe125.sarif -mdr-gen sarif -mdr-no-print-libc -mdr-sarif-deterministic",
+ "frama-c -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report -load ./cwe125_eva.sav -then -mdr-out ./cwe125.sarif -mdr-gen sarif -mdr-no-print-libc -mdr-sarif-deterministic",
"arguments": [
- "-journal-disable", "-check", "-no-autoload-plugins",
- "-add-symbolic-path", ":.",
+ "-check", "-no-autoload-plugins", "-add-symbolic-path", ":.",
"-load-module=eva,from,scope,markdown_report", "-load",
"./cwe125_eva.sav", "-then", "-mdr-out", "./cwe125.sarif",
"-mdr-gen", "sarif", "-mdr-no-print-libc",
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
index 289318d160e..f5cfcd6dea5 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif
@@ -16,10 +16,9 @@
"invocations": [
{
"commandLine":
- "frama-c -journal-disable -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report std_string.c -eva -then -mdr-sarif-deterministic -mdr-gen sarif -mdr-out ./std_string.sarif",
+ "frama-c -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report std_string.c -eva -then -mdr-sarif-deterministic -mdr-gen sarif -mdr-out ./std_string.sarif",
"arguments": [
- "-journal-disable", "-check", "-no-autoload-plugins",
- "-add-symbolic-path", ":.",
+ "-check", "-no-autoload-plugins", "-add-symbolic-path", ":.",
"-load-module=eva,from,scope,markdown_report", "std_string.c",
"-eva", "-then", "-mdr-sarif-deterministic", "-mdr-gen", "sarif",
"-mdr-out", "./std_string.sarif"
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif b/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
index 959696dfba7..42708bf7537 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif
@@ -16,10 +16,9 @@
"invocations": [
{
"commandLine":
- "frama-c -journal-disable -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic libc.c -mdr-out ./with-libc.sarif",
+ "frama-c -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic libc.c -mdr-out ./with-libc.sarif",
"arguments": [
- "-journal-disable", "-check", "-no-autoload-plugins",
- "-add-symbolic-path", ":.",
+ "-check", "-no-autoload-plugins", "-add-symbolic-path", ":.",
"-load-module=eva,from,scope,markdown_report", "-eva",
"-eva-no-results", "-mdr-gen", "sarif",
"-mdr-sarif-deterministic", "libc.c", "-mdr-out",
diff --git a/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif b/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif
index 23babca6ce7..00f3d299424 100644
--- a/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif
+++ b/src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif
@@ -16,10 +16,9 @@
"invocations": [
{
"commandLine":
- "frama-c -journal-disable -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic libc.c -mdr-no-print-libc -mdr-out ./without-libc.sarif",
+ "frama-c -check -no-autoload-plugins -add-symbolic-path :. -load-module=eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic libc.c -mdr-no-print-libc -mdr-out ./without-libc.sarif",
"arguments": [
- "-journal-disable", "-check", "-no-autoload-plugins",
- "-add-symbolic-path", ":.",
+ "-check", "-no-autoload-plugins", "-add-symbolic-path", ":.",
"-load-module=eva,from,scope,markdown_report", "-eva",
"-eva-no-results", "-mdr-gen", "sarif",
"-mdr-sarif-deterministic", "libc.c", "-mdr-no-print-libc",
diff --git a/src/plugins/wp/tests/wp/wp_call_pre.c b/src/plugins/wp/tests/wp/wp_call_pre.c
index 857b5f62968..be7bf59d671 100644
--- a/src/plugins/wp/tests/wp/wp_call_pre.c
+++ b/src/plugins/wp/tests/wp/wp_call_pre.c
@@ -6,7 +6,7 @@ OPT: -wp-model Hoare -wp-no-simpl -wp-fct double_call
*/
/* run.config_qualif
-OPT: -journal-disable -wp -wp-par 1
+OPT: -wp -wp-par 1
*/
int G = 3;
diff --git a/src/plugins/wp/tests/wp/wp_strategy.c b/src/plugins/wp/tests/wp/wp_strategy.c
index 258fd478c99..d7e6a4845b0 100644
--- a/src/plugins/wp/tests/wp/wp_strategy.c
+++ b/src/plugins/wp/tests/wp/wp_strategy.c
@@ -1,10 +1,10 @@
/* run.config
-OPT: -journal-disable -wp-model Hoare -wp-verbose 2
-OPT: -journal-disable -wp-model Typed -wp-verbose 2 -wp-prop @assigns
+OPT: -wp-model Hoare -wp-verbose 2
+OPT: -wp-model Typed -wp-verbose 2 -wp-prop @assigns
*/
/* run.config_qualif
-OPT: -journal-disable -rte -wp -wp-model Hoare -wp-par 1 -wp-msg-key shell
+OPT: -rte -wp -wp-model Hoare -wp-par 1 -wp-msg-key shell
*/
/*----------------------------------------------------------------------------*/
diff --git a/src/plugins/wp/tests/wp_acsl/struct_use_case.i b/src/plugins/wp/tests/wp_acsl/struct_use_case.i
index e9839c540db..2707e0e0d25 100644
--- a/src/plugins/wp/tests/wp_acsl/struct_use_case.i
+++ b/src/plugins/wp/tests/wp_acsl/struct_use_case.i
@@ -3,8 +3,8 @@
*/
/* run.config_qualif
-OPT: -journal-disable -wp -wp-model Caveat -wp-par 1 -wp-prop="-ko"
-OPT: -journal-disable -wp -wp-model Caveat -wp-par 1 -wp-prop ko -wp-steps 50
+OPT: -wp -wp-model Caveat -wp-par 1 -wp-prop="-ko"
+OPT: -wp -wp-model Caveat -wp-par 1 -wp-prop ko -wp-steps 50
*/
/* run.config_qed
@@ -18,7 +18,7 @@ struct {
/*@ ensures ko: var == { \old(var) \with .b[1] = x } ;
@ ensures ok: var == { \old(var) \with .b[1] = x, .b[0] = y } ;
- @*/
+ @*/
void f(unsigned int x, unsigned int y){
var.b[0] = y;
var.b[1] = x;
@@ -26,7 +26,7 @@ void f(unsigned int x, unsigned int y){
/*@ ensures ko: var == { \old(var) \with .b[1] = x } ;
@ ensures ok: var == { \old(var) \with .b[1] = x, .a = y } ;
- @*/
+ @*/
void g(unsigned int x, unsigned int y){
var.a = y;
var.b[1] = x;
diff --git a/tests/sparecode/test_config b/tests/sparecode/test_config
index 40e3a32e114..f891b735a90 100644
--- a/tests/sparecode/test_config
+++ b/tests/sparecode/test_config
@@ -1,3 +1,3 @@
MACRO: SPARECODE_PLUGINS @EVA_PLUGINS@ sparecode
PLUGIN: @SPARECODE_PLUGINS@
-OPT: -journal-disable @EVA_OPTIONS@ -sparecode-debug 1
+OPT: @EVA_OPTIONS@ -sparecode-debug 1
diff --git a/tests/spec/test_config b/tests/spec/test_config
index 6f16db895cb..486cfa4b0f8 100644
--- a/tests/spec/test_config
+++ b/tests/spec/test_config
@@ -2,4 +2,4 @@ COMMENT: for now, this directory mainly tests the annotations syntax,
COMMENT: no analysis is performed.
COMMENT: we continue on annotation errors, as this allows to put
COMMENT: various variations of the same test in one file.
-OPT: -pp-annot -print -journal-disable -kernel-warn-key=annot-error=active -check -machdep x86_32
+OPT: -pp-annot -print -kernel-warn-key=annot-error=active -check -machdep x86_32
--
GitLab