diff --git a/tests/misc/filepath.i b/tests/misc/filepath.i index eb178f8224607c8dce90532cc9b037ff562b16f4..f5c0183704fb0f14aba28d804eb133137365c870 100644 --- a/tests/misc/filepath.i +++ b/tests/misc/filepath.i @@ -1,3 +1,4 @@ /* run.config - OPT: -no-autoload-plugins -load-module @PTEST_DIR@/filepath_test.ml + EXECNOW: make -s @PTEST_DIR@/filepath_test.cmxs + OPT: -no-autoload-plugins -load-module @PTEST_DIR@/filepath_test */ diff --git a/tests/misc/log-file.i b/tests/misc/log-file.i index 661521ddb7c8d6f929fc18396167c8510f561b67..833ee51da34f8228cc4ab373fe8573b430b7ca3f 100644 --- a/tests/misc/log-file.i +++ b/tests/misc/log-file.i @@ -1,4 +1,5 @@ /* run.config + EXECNOW: make -s @PTEST_DIR@/plugin_log.cmxs LOG: log-file-kernel-warnings.txt LOG: log-file-kernel-results.txt LOG: log-file-feedback.txt @@ -7,7 +8,7 @@ LOG: plugin-log-all.txt FILTER: sed 's|Your Frama-C version is.*|Your Frama-C version is VERSION|' STDOPT: #"-kernel-log w:@PTEST_RESULT@/log-file-kernel-warnings.txt,r:@PTEST_RESULT@/log-file-kernel-results.txt -eva-log f:@PTEST_RESULT@/log-file-feedback.txt,afewr:@PTEST_RESULT@/log-file-value-all.txt -eva-log :@PTEST_RESULT@/log-file-value-default.txt -then -kernel-log f:@PTEST_RESULT@/log-file-feedback.txt" - OPT: -load-module tests/misc/plugin_log.ml -kernel-msg-key foo-category -kernel-log=a:@PTEST_RESULT@/plugin-log-all.txt + OPT: -load-module tests/misc/plugin_log -kernel-msg-key foo-category -kernel-log=a:@PTEST_RESULT@/plugin-log-all.txt DONTRUN: test disabled due to non-deterministic errors in CI */ int f(void); // generates kernel warning (missing spec) diff --git a/tests/misc/oracle/log-file-feedback.txt b/tests/misc/oracle/log-file-feedback.txt index 36ffb1f22e57f630e6be7ebd23b2467ab31370ea..941d344dc0af8f47c2ec0f194933b87cdb04c53a 100644 --- a/tests/misc/oracle/log-file-feedback.txt +++ b/tests/misc/oracle/log-file-feedback.txt @@ -3,13 +3,13 @@ [eva] Computing initial state [eva] Initial state computed [eva] computing for function f <- main. -Called from tests/misc/log-file.i:18. +Called from tests/misc/log-file.i:20. [eva] using specification for function f [eva] Done for function f [eva] computing for function g <- main. -Called from tests/misc/log-file.i:19. +Called from tests/misc/log-file.i:21. [eva] using specification for function g [eva] Done for function g -tests/misc/log-file.i:20:[eva] starting to merge loop iterations +tests/misc/log-file.i:22:[eva] starting to merge loop iterations [eva] Recording results for main [eva] done for function main diff --git a/tests/misc/oracle/log-file-kernel-warnings.txt b/tests/misc/oracle/log-file-kernel-warnings.txt index 3ab2fc7cdc3e703ae681512fcc3dfe307c4e2042..4e35b1c74cec91a3ba4e36c94232ff1ccbbf3e6e 100644 --- a/tests/misc/oracle/log-file-kernel-warnings.txt +++ b/tests/misc/oracle/log-file-kernel-warnings.txt @@ -1 +1 @@ -tests/misc/log-file.i:18:[kernel:annot:missing-spec] warning: Neither code nor specification for function f, generating default assigns from the prototype +tests/misc/log-file.i:20:[kernel:annot:missing-spec] warning: Neither code nor specification for function f, generating default assigns from the prototype diff --git a/tests/misc/oracle/log-file-value-all.txt b/tests/misc/oracle/log-file-value-all.txt index 258754c1f7f836687e390ddb4e262f18960c866d..c19d8ff15faac9301d00a3f1878c008f2c7ef9fe 100644 --- a/tests/misc/oracle/log-file-value-all.txt +++ b/tests/misc/oracle/log-file-value-all.txt @@ -2,15 +2,15 @@ [eva] Computing initial state [eva] Initial state computed [eva] computing for function f <- main. -Called from tests/misc/log-file.i:18. +Called from tests/misc/log-file.i:20. [eva] using specification for function f [eva] Done for function f [eva] computing for function g <- main. -Called from tests/misc/log-file.i:19. +Called from tests/misc/log-file.i:21. [eva] using specification for function g -tests/misc/log-file.i:15:[eva] warning: no 'assigns \result \from ...' clause specified for function g +tests/misc/log-file.i:17:[eva] warning: no 'assigns \result \from ...' clause specified for function g [eva] Done for function g -tests/misc/log-file.i:20:[eva] starting to merge loop iterations +tests/misc/log-file.i:22:[eva] starting to merge loop iterations [eva] Recording results for main [eva] done for function main [eva] ====== VALUES COMPUTED ====== diff --git a/tests/misc/oracle/log-file-value-default.txt b/tests/misc/oracle/log-file-value-default.txt index 9d4908aa0b45d572c09498784aaebc250f71a300..93553049c30efa17102275ef8c4b8187d04efeea 100644 --- a/tests/misc/oracle/log-file-value-default.txt +++ b/tests/misc/oracle/log-file-value-default.txt @@ -1,2 +1,2 @@ -tests/misc/log-file.i:15:[eva] warning: no 'assigns \result \from ...' clause specified for function g +tests/misc/log-file.i:17:[eva] warning: no 'assigns \result \from ...' clause specified for function g [eva] ====== VALUES COMPUTED ====== diff --git a/tests/misc/oracle/log-file.0.res.oracle b/tests/misc/oracle/log-file.0.res.oracle index 75c688457ba46f7f783c6fa33d20957f376a068f..83288a2ea513c05a7125a26eea8b5a4cee999871 100644 --- a/tests/misc/oracle/log-file.0.res.oracle +++ b/tests/misc/oracle/log-file.0.res.oracle @@ -5,18 +5,18 @@ [eva:initial-state] Values of globals at initialization [eva] computing for function f <- main. - Called from tests/misc/log-file.i:18. -[kernel:annot:missing-spec] tests/misc/log-file.i:18: Warning: + Called from tests/misc/log-file.i:20. +[kernel:annot:missing-spec] tests/misc/log-file.i:20: Warning: Neither code nor specification for function f, generating default assigns from the prototype [eva] using specification for function f [eva] Done for function f [eva] computing for function g <- main. - Called from tests/misc/log-file.i:19. + Called from tests/misc/log-file.i:21. [eva] using specification for function g -[eva] tests/misc/log-file.i:15: Warning: +[eva] tests/misc/log-file.i:17: Warning: no 'assigns \result \from ...' clause specified for function g [eva] Done for function g -[eva] tests/misc/log-file.i:20: starting to merge loop iterations +[eva] tests/misc/log-file.i:22: starting to merge loop iterations [eva] Recording results for main [eva] done for function main [eva] ====== VALUES COMPUTED ====== diff --git a/tests/rte/threefunc.c b/tests/rte/threefunc.c index 6220079b7feaa8713e5d861840c7887d26a65abb..03b2ad3b373fd5dcc26253574999f9bccfa59a30 100644 --- a/tests/rte/threefunc.c +++ b/tests/rte/threefunc.c @@ -1,6 +1,6 @@ /* run.config EXECNOW: make -s @PTEST_DIR@/my_annotation/my_annotation.cmxs -OPT: -load-module @PTEST_DIR@/my_annotation/my_annotation.ml +OPT: -load-module @PTEST_DIR@/my_annotation/my_annotation */