Skip to content
Snippets Groups Projects
Commit 304a52cf authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[tests] fix a few more -load-module *.ml

parent 693725d5
No related branches found
No related tags found
No related merge requests found
/* 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
*/
/* 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)
......
......@@ -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
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
......@@ -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 ======
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 ======
......@@ -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 ======
......
/* 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
*/
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment