diff --git a/share/analysis-scripts/make_wrapper.py b/share/analysis-scripts/make_wrapper.py index 5574816cf1355f0365b1666d845c6cb1f69520ce..25cb2b838ae9f87897c396656cd2b7ccf77f9a96 100755 --- a/share/analysis-scripts/make_wrapper.py +++ b/share/analysis-scripts/make_wrapper.py @@ -54,7 +54,8 @@ if not framac_bin: framac_script = f"{framac_bin}/frama-c-script" _logfd, logname = tempfile.mkstemp(prefix="make_wrapper_tmp_") -with subprocess.Popen(['make', "-C", make_dir] + args, +cmd_list = ['make', "-C", make_dir] + args +with subprocess.Popen(cmd_list, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) as proc, \ open (logname, "bw") as logfile: diff --git a/tests/fc_script/make-for-make-wrapper.mk b/tests/fc_script/make-for-make-wrapper.mk new file mode 100644 index 0000000000000000000000000000000000000000..983f2a16d9f1be8dcaaaa332626afa7c6c54ffee --- /dev/null +++ b/tests/fc_script/make-for-make-wrapper.mk @@ -0,0 +1,22 @@ +# Customized makefile template for testing 'frama-c-script make-wrapper'. + +include $(shell $(FRAMAC) -no-autoload-plugins -print-share-path)/analysis-scripts/prologue.mk + +FCFLAGS += \ + -kernel-warn-key annot:missing-spec=abort \ + -kernel-warn-key typing:implicit-function-declaration=abort \ + +EVAFLAGS += \ + -eva-warn-key builtins:missing-spec=abort \ + +## Analysis targets (suffixed with .eva) +TARGETS = make-for-make-wrapper.eva + +make-for-make-wrapper.parse: \ + make-wrapper.c \ + make-wrapper2.c \ + # make-wrapper3.c is deliberately absent of this list + +### Epilogue. Do not modify this block. ####################################### +include $(shell $(FRAMAC) -no-autoload-plugins -print-share-path)/analysis-scripts/epilogue.mk +############################################################################### diff --git a/tests/fc_script/make-wrapper.c b/tests/fc_script/make-wrapper.c new file mode 100644 index 0000000000000000000000000000000000000000..4375eef42f72d0369f18425e99d760f91bd2f72d --- /dev/null +++ b/tests/fc_script/make-wrapper.c @@ -0,0 +1,17 @@ +/* run.config + NOFRAMAC: testing frama-c-script + EXECNOW: LOG make-wrapper.res LOG make-wrapper.err cd @PTEST_DIR@ && FRAMAC=../../bin/frama-c ../../bin/frama-c-script make-wrapper --make-dir . -f make-for-make-wrapper.mk | sed -e "s:$PWD:PWD:g" | grep -v "make:.*Error" > result/make-wrapper.res 2> result/make-wrapper.err && rm -rf make-for-make-wrapper.parse make-for-make-wrapper.eva +*/ + +int defined(int a); + +int specified(int a); + +int external(int a); + +int main() { + int a = 42; + a = defined(a); + a = specified(a); + a = external(a); +} diff --git a/tests/fc_script/make-wrapper2.c b/tests/fc_script/make-wrapper2.c new file mode 100644 index 0000000000000000000000000000000000000000..0f97864c1b8f7a6192590aa232ac04e7e4ca3090 --- /dev/null +++ b/tests/fc_script/make-wrapper2.c @@ -0,0 +1,16 @@ +/* run.config + DONTRUN: part of the test in make-wrapper.c +*/ + +int defined(int a) { + return a + 1; +} + +/*@ + assigns \result \from a; + ensures \result == a + 2; + */ +int specified(int a); + +// defined in another, non-included, file +int external(int a); diff --git a/tests/fc_script/make-wrapper3.c b/tests/fc_script/make-wrapper3.c new file mode 100644 index 0000000000000000000000000000000000000000..83ed541f1db724dc886d6bb865491c47d866d0e2 --- /dev/null +++ b/tests/fc_script/make-wrapper3.c @@ -0,0 +1,9 @@ +/* run.config + DONTRUN: part of the test in make-wrapper.c +*/ + +// This file contains a definition for function 'external', but it is _not_ +// included when parsing 'make-wrapper.c'. This triggers a make-wrapper message. +int external(int a) { + return a + 3; +} diff --git a/tests/fc_script/oracle/find_fun1.res b/tests/fc_script/oracle/find_fun1.res index a846b6beb54f9a0245507e35df7567e3d48e9245..3e35782af42a6f5546e034e026a63d09df5ac934 100644 --- a/tests/fc_script/oracle/find_fun1.res +++ b/tests/fc_script/oracle/find_fun1.res @@ -1,4 +1,4 @@ -Looking for 'main2' inside 5 file(s)... +Looking for 'main2' inside 8 file(s)... Possible declarations for function 'main2' in the following file(s): tests/fc_script/for-find-fun.c Possible definitions for function 'main2' in the following file(s): diff --git a/tests/fc_script/oracle/find_fun2.res b/tests/fc_script/oracle/find_fun2.res index 273cc015b4ef5f5ef497533511f083c50c2c63fe..e9f42fdf76a5d227ee458abdc59e3370a26d57d1 100644 --- a/tests/fc_script/oracle/find_fun2.res +++ b/tests/fc_script/oracle/find_fun2.res @@ -1,4 +1,4 @@ -Looking for 'main3' inside 5 file(s)... +Looking for 'main3' inside 8 file(s)... Possible declarations for function 'main3' in the following file(s): tests/fc_script/for-find-fun2.c Possible definitions for function 'main3' in the following file(s): diff --git a/tests/fc_script/oracle/find_fun3.res b/tests/fc_script/oracle/find_fun3.res index a7059bd1c963ad064b030a17ef9782873c397b0d..65fc349325d2406ea212025ed38e51347b09217f 100644 --- a/tests/fc_script/oracle/find_fun3.res +++ b/tests/fc_script/oracle/find_fun3.res @@ -1,2 +1,2 @@ -Looking for 'false_positive' inside 5 file(s)... +Looking for 'false_positive' inside 8 file(s)... No declaration/definition found for function 'false_positive' diff --git a/tests/fc_script/oracle/make-wrapper.err b/tests/fc_script/oracle/make-wrapper.err new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/tests/fc_script/oracle/make-wrapper.res b/tests/fc_script/oracle/make-wrapper.res new file mode 100644 index 0000000000000000000000000000000000000000..d2d19765aa4019ee9073e2fc23e25a43efe4e9a5 --- /dev/null +++ b/tests/fc_script/oracle/make-wrapper.res @@ -0,0 +1,28 @@ +make: Entering directory 'PWD' + +[34mCommand: ../../bin/frama-c -kernel-warn-key annot:missing-spec=abort -kernel-warn-key typing:implicit-function-declaration=abort -cpp-extra-args="" make-wrapper.c make-wrapper2.c(B[m + +[kernel] Parsing make-wrapper.c (with preprocessing) +[kernel] Parsing make-wrapper2.c (with preprocessing) + +[34mCommand: ../../bin/frama-c -kernel-warn-key annot:missing-spec=abort -kernel-warn-key typing:implicit-function-declaration=abort -eva -eva-no-print -eva-no-show-progress -eva-msg-key=-initial-state -eva-print-callstacks -eva-warn-key alarm=inactive -no-deps-print -no-calldeps-print -eva-warn-key garbled-mix -calldeps -from-verbose 0 -eva-warn-key builtins:missing-spec=abort (B[m + +[eva] Analyzing a complete application starting at main +[eva] Computing initial state +[eva] Initial state computed +[eva] using specification for function specified +[kernel:annot:missing-spec] make-wrapper.c:16: Warning: + Neither code nor specification for function external, generating default assigns from the prototype +[kernel] User Error: warning annot:missing-spec treated as fatal error. +[kernel] Frama-C aborted: invalid user input. +[kernel] Warning: attempting to save on non-zero exit code: modifying filename into `PWD/make-for-make-wrapper.eva/framac.sav.error'. +make: Leaving directory 'PWD' + +***** make-wrapper recommendations ***** + +*** recommendation #1 *** + +1. Found function with missing spec: external + Looking for files defining it... +Add the following file to the list of sources to be parsed: + make-wrapper3.c