From 304a52cfcf2c8d6e4cc7e0076705f8a030b8e09a Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Fri, 25 Jan 2019 08:58:09 +0100
Subject: [PATCH] [tests] fix a few more -load-module *.ml
---
tests/misc/filepath.i | 3 ++-
tests/misc/log-file.i | 3 ++-
tests/misc/oracle/log-file-feedback.txt | 6 +++---
tests/misc/oracle/log-file-kernel-warnings.txt | 2 +-
tests/misc/oracle/log-file-value-all.txt | 8 ++++----
tests/misc/oracle/log-file-value-default.txt | 2 +-
tests/misc/oracle/log-file.0.res.oracle | 10 +++++-----
tests/rte/threefunc.c | 2 +-
8 files changed, 19 insertions(+), 17 deletions(-)
diff --git a/tests/misc/filepath.i b/tests/misc/filepath.i
index eb178f82246..f5c0183704f 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 661521ddb7c..833ee51da34 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 36ffb1f22e5..941d344dc0a 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 3ab2fc7cdc3..4e35b1c74ce 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 258754c1f7f..c19d8ff15fa 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 9d4908aa0b4..93553049c30 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 75c688457ba..83288a2ea51 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 6220079b7fe..03b2ad3b373 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
*/
--
GitLab