diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index cbd6875ae3dfa21c5c8fb22eafd9e53097703f1e..d797d5076b8c73de467757745cc1896a91b2452c 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 c6d808f04e906cb195778fae19e2a20e7a9070a1..cab716c2a9744582c940695436017801e308f71c 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 3769a8fc34c9937c920179b4cc011f400febe713..2492553138546f46918a6768c6ba357925416d2d 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 289318d160e25da79dfcb8918643ebccb0bd5b0c..f5cfcd6dea5dc27f0acfa63b9387f2f4b924a661 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 959696dfba7c771680aa1d287e4cf7e9b4fd3d3f..42708bf75372a88ed5ac6e0dd75257c9dd2f3dd1 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 23babca6ce70631edc4076a7a4ee4f1705e533c4..00f3d299424eb204322729e64d0831c86c96458c 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 857b5f629686bc3537b9b3eb40c6692caae44d76..be7bf59d67146f3d3d65471808eca4672969106a 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 258fd478c999f79a898eb2077da01abdc6ee063a..d7e6a4845b0fe23c8bfc8154f30b84e718bf7dcf 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 e9839c540db66f3c0f415e8d452163fbcbbee579..2707e0e0d25fd6cfac29632876df3613e6698d11 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 40e3a32e1141194ae21aebe0470c76bca948bc06..f891b735a90856bbb735f6c53a50fef19542b9f6 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 6f16db895cb99190e93d744819de7c21e7358ebe..486cfa4b0f8caaaad2e1e03e663d2df6e32f5563 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