diff --git a/tests/misc/log-file.i b/tests/misc/log-file.i index e017b52fb8b56ebba6ef12e0af66442f6850bb71..661521ddb7c8d6f929fc18396167c8510f561b67 100644 --- a/tests/misc/log-file.i +++ b/tests/misc/log-file.i @@ -8,6 +8,7 @@ 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 + DONTRUN: test disabled due to non-deterministic errors in CI */ int f(void); // generates kernel warning (missing spec)