diff --git a/share/analysis-scripts/analysis.mk b/share/analysis-scripts/analysis.mk index 0e4910e1acfeb82f018a68576adfdc200fdaa988..a1319e9756817f674bcc22cb0d64debcc23810d2 100644 --- a/share/analysis-scripts/analysis.mk +++ b/share/analysis-scripts/analysis.mk @@ -84,7 +84,7 @@ else SED_UNBUFFERED:=sed --unbuffered ifneq (,$(wildcard /usr/bin/time)) define time_with_output - /usr/bin/time --format='user_time=%U\nmemory=%M' --output="$(1)" + /usr/bin/time -f 'user_time=%U\nmemory=%M' -o "$(1)" endef else define time_with_output @@ -143,7 +143,7 @@ clean-backups: HR_TIMESTAMP := $(shell date +"%H:%M:%S %d/%m/%Y")# Human readable DIR := $(dir $(lastword $(MAKEFILE_LIST))) -SHELL := /bin/bash +SHELL := $(shell which bash) .SHELLFLAGS := -eu -o pipefail -c .ONESHELL: diff --git a/share/analysis-scripts/make_wrapper.py b/share/analysis-scripts/make_wrapper.py index ed72df096223334ce385db07fc050376f49d21b6..07c314b9d8a8679b51f13c03973d15e36091395e 100755 --- a/share/analysis-scripts/make_wrapper.py +++ b/share/analysis-scripts/make_wrapper.py @@ -32,6 +32,7 @@ import re import subprocess import sys from functools import partial +import tempfile MIN_PYTHON = (3, 6) # for automatic Path conversions if sys.version_info < MIN_PYTHON: @@ -40,7 +41,7 @@ if sys.version_info < MIN_PYTHON: parser = argparse.ArgumentParser(description=""" Builds the specified target, parsing the output to identify and recommend actions in case of failure.""") -parser.add_argument('--make-dir', metavar='DIR', default=".frama-c", nargs=1, +parser.add_argument('--make-dir', metavar='DIR', default=".frama-c", help='directory containing the makefile (default: .frama-c)') (make_dir_arg, args) = parser.parse_known_args() @@ -52,10 +53,19 @@ if not framac_bin: sys.exit("error: FRAMAC_BIN not in environment (set by frama-c-script)") framac_script = f"{framac_bin}/frama-c-script" -out = subprocess.Popen(['make', "-C", make_dir] + args, - stdout=subprocess.PIPE, stderr=subprocess.STDOUT) - -output = out.communicate()[0].decode('utf-8') +output_lines = [] +cmd_list = ['make', "-C", make_dir] + args +with subprocess.Popen(cmd_list, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE) as proc: + while True: + line = proc.stdout.readline() + if line: + sys.stdout.buffer.write(line) + sys.stdout.flush() + output_lines.append(line.decode('utf-8')) + else: + break re_missing_spec = re.compile("Neither code nor specification for function ([^,]+),") re_recursive_call_start = re.compile("detected recursive call") @@ -63,9 +73,8 @@ re_recursive_call_end = re.compile("Use -eva-ignore-recursive-calls to ignore") tips = [] -lines = iter(output.splitlines()) +lines = iter(output_lines) for line in lines: - print(line) match = re_missing_spec.search(line) if match: fname = match.group(1) 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..cc36eead6f02ea799797df57409233db946e5658 --- /dev/null +++ b/tests/fc_script/make-wrapper.c @@ -0,0 +1,18 @@ +/* run.config + NOFRAMAC: testing frama-c-script + COMMENT: we must filter 'make:' output lines, since they differ when run by the CI (e.g. mention to jobserver) + EXECNOW: LOG make-wrapper.res LOG make-wrapper.err cd @PTEST_DIR@ && touch make-wrapper2.c && touch make-wrapper3.c && 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.*" > 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..9faa818ae65c5e1aa39fdd07142c63896fb6e6cc --- /dev/null +++ b/tests/fc_script/oracle/make-wrapper.res @@ -0,0 +1,26 @@ + +[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:17: 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-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