diff --git a/share/analysis-scripts/analysis.mk b/share/analysis-scripts/analysis.mk index 4e545c9e747b46328d15a067ded5540408252f66..752b274ab34d4195704e00f0dbb084f522741b3f 100644 --- a/share/analysis-scripts/analysis.mk +++ b/share/analysis-scripts/analysis.mk @@ -35,6 +35,7 @@ # EVAFLAGS flags to use with the Eva plugin # EVABUILTINS Eva builtins to be set (via -eva-builtin) # EVAUSESPECS Eva functions to be overridden by specs (-eva-use-spec) +# WPFLAGS flags to use with the WP plugin # # FLAMEGRAPH If set (to any value), running an analysis will produce an # SVG + HTML flamegraph at the end. @@ -115,6 +116,7 @@ EVAFLAGS ?= \ -calldeps -from-verbose 0 \ $(if $(EVABUILTINS), -eva-builtin=$(call fc_list,$(EVABUILTINS)),) \ $(if $(EVAUSESPECS), -eva-use-spec $(call fc_list,$(EVAUSESPECS)),) +WPFLAGS ?= FCFLAGS ?= FCGUIFLAGS ?= @@ -145,7 +147,7 @@ SHELL := $(shell which bash) .FORCE: .SUFFIXES: # Disable make builtins -%.parse/command %.eva/command: +%.parse/command %.eva/command %.wp/command: @# %.parse: SOURCES = $(filter-out %/command,$^) @@ -172,7 +174,7 @@ SHELL := $(shell which bash) printf 'cmd_args=%q\n' "$(subst ",\",$(wordlist 2,999,$(PARSE)))" } >> $@/stats.txt mv $@/{running,command} - touch $@ # Update timestamp and prevents remake if nothing changes + touch $@ # Update timestamp and prevent remake if nothing changes %.eva: EVA = $(FRAMAC) $(FCFLAGS) -eva $(EVAFLAGS) %.eva: PARSE_RESULT = $(word 1,$(subst ., ,$*)).parse @@ -214,6 +216,34 @@ SHELL := $(shell which bash) mv $@/{running,command} touch $@ # Update timestamp and prevents remake if nothing changes +%.wp: WP = $(FRAMAC) $(FCFLAGS) -wp $(WPFLAGS) +%.wp: PARSE_RESULT = $(word 1,$(subst ., ,$*)).parse +%.wp: $$(PARSE_RESULT) $$(shell $(DIR)cmd-dep.sh $$@/command $$(WP)) $(if $(BENCHMARK),.FORCE,) + @$(call display_command,$(WP)) + mkdir -p $@ + mv -f $@/{command,running} + { + $(call time_with_output,$@/stats.txt) \ + $(WP) \ + -load $(PARSE_RESULT)/framac.sav -save $@/framac.sav \ + -kernel-log w:$@/warnings.log \ + -wp-log w:$@/warnings.log \ + -then \ + -report-csv $@/alarms.csv -report-no-proven \ + -report-log w:$@/warnings.log \ + || ($(RM) $@/stats.txt && false) # Prevents having error code reporting in stats.txt + } 2>&1 | + tee $@/wp.log + { + printf 'timestamp=%q\n' "$(HR_TIMESTAMP)"; + printf 'warnings=%s\n' "`cat $@/warnings.log | grep ':\[\(wp\|kernel\)\]' | wc -l`"; + printf 'alarms=%s\n' "`expr $$(cat $@/alarms.csv | wc -l) - 1`"; + printf 'cmd_args=%q\n' "$(subst ",\",$(wordlist 2,999,$(WP)))"; + printf 'benchmark_tag=%s' "$(BENCHMARK)" + } >> $@/stats.txt + mv $@/{running,command} + touch $@ # Update timestamp and prevent remake if nothing changes + %.gui: % $(FRAMAC_GUI) $(FCGUIFLAGS) -load $^/framac.sav & diff --git a/share/analysis-scripts/template.mk b/share/analysis-scripts/template.mk index 8c85db2151c454fc319cb21fa14b821e3fc2c07c..689b9eab61ccedee46cb8637eaaa9a51e3ad3f09 100644 --- a/share/analysis-scripts/template.mk +++ b/share/analysis-scripts/template.mk @@ -30,6 +30,9 @@ FCFLAGS += \ EVAFLAGS += \ -eva-warn-key builtins:missing-spec=abort \ +## WP-specific flags +WPFLAGS += \ + ## GUI-only flags FCGUIFLAGS += \ diff --git a/tests/fc_script/oracle/GNUmakefile b/tests/fc_script/oracle/GNUmakefile index 7ea16dfa4466c6227e0eae0e9287b39576187f26..96158431b8b158ab4119ef716b8ba0b3c2e61f6c 100644 --- a/tests/fc_script/oracle/GNUmakefile +++ b/tests/fc_script/oracle/GNUmakefile @@ -32,6 +32,9 @@ FCFLAGS += \ EVAFLAGS += \ -eva-warn-key builtins:missing-spec=abort \ +## WP-specific flags +WPFLAGS += \ + ## GUI-only flags FCGUIFLAGS += \