diff --git a/share/analysis-scripts/analysis.mk b/share/analysis-scripts/analysis.mk index fa832425b124f1fffdf77927c28a43b654db73fc..8a4d48e462d499bb3ac3a400946be46e61efe86f 100644 --- a/share/analysis-scripts/analysis.mk +++ b/share/analysis-scripts/analysis.mk @@ -113,8 +113,6 @@ fc_list = $(subst $(space),$(comma),$(strip $1)) FRAMAC ?= frama-c FRAMAC_SCRIPT = $(FRAMAC)-script FRAMAC_GUI ?= frama-c-gui -MACHDEP ?= x86_32 -SLEVEL ?= EVAFLAGS ?= \ -eva-no-print -eva-no-show-progress -eva-msg-key=-initial-state \ -eva-print-callstacks -eva-warn-key alarm=inactive \ @@ -158,7 +156,7 @@ SHELL := /bin/bash @# %.parse: SOURCES = $(filter-out %/command,$^) -%.parse: PARSE = $(FRAMAC) $(FCFLAGS) -machdep $(MACHDEP) -cpp-extra-args="$(CPPFLAGS)" $(SOURCES) +%.parse: PARSE = $(FRAMAC) $(FCFLAGS) $(if $(value MACHDEP),-machdep $(MACHDEP),) -cpp-extra-args="$(CPPFLAGS)" $(SOURCES) %.parse: $$(if $$^,,.IMPOSSIBLE) $$(shell $(DIR)cmd-dep.sh $$@/command $$(PARSE)) @$(call display_command,$(PARSE)) mkdir -p $@ diff --git a/share/analysis-scripts/prologue.mk b/share/analysis-scripts/prologue.mk index c58dda47db15fb1a3e412e9b83c0112ab23a3b0c..f1cca3d38888a266e2f049084e8aa4a227af99fa 100644 --- a/share/analysis-scripts/prologue.mk +++ b/share/analysis-scripts/prologue.mk @@ -31,12 +31,6 @@ makefile_dir := $(dir $(lastword $(MAKEFILE_LIST))) # Improves analysis time, at the cost of extra memory usage export FRAMA_C_MEMORY_FOOTPRINT = 8 -# path.mk contains variables which are specific to each -# user and should not be versioned, such as the path to the -# frama-c binaries (e.g. FRAMAC and FRAMAC_GUI). -# It is an optional include, unnecessary if frama-c is in the PATH --include path.mk - # FRAMAC is defined in path.mk when it is included, so the # line below will be safely ignored if this is the case. # Otherwise, the user may supply it to indicate which Frama-C binary to use. diff --git a/share/analysis-scripts/template.mk b/share/analysis-scripts/template.mk index b5f1566cb467421cfbf207e4a8b7b3e8ff5d5e10..114d2cd6f80d6b624ece1a7f0478979eeac81036 100644 --- a/share/analysis-scripts/template.mk +++ b/share/analysis-scripts/template.mk @@ -2,12 +2,15 @@ # For details and usage information, see the Frama-C User Manual. ### Prologue. Do not modify this block. ####################################### --include path.mk -FRAMAC ?= frama-c +-include path.mk # path.mk contains variables specific to each user + # (e.g. FRAMAC, FRAMAC_GUI) and should not be versioned. It is + # an optional include, unnecessary if frama-c is in the PATH. +FRAMAC ?= frama-c # FRAMAC is defined in path.mk when it is included, but the + # user can override it in the command-line. include $(shell $(FRAMAC)-config -scripts)/prologue.mk ############################################################################### -# Edit below as needed. MACHDEP is mandatory. Suggested flags are optional. +# Edit below as needed. Suggested flags are optional. MACHDEP = x86_32 diff --git a/tests/fc_script/oracle/GNUmakefile b/tests/fc_script/oracle/GNUmakefile index 226424750590969d2d27fc8ad92564a803735b43..5b9a464e26fd809740a93a417ee458e204eb115c 100644 --- a/tests/fc_script/oracle/GNUmakefile +++ b/tests/fc_script/oracle/GNUmakefile @@ -2,12 +2,15 @@ # For details and usage information, see the Frama-C User Manual. ### Prologue. Do not modify this block. ####################################### --include path.mk -FRAMAC ?= frama-c +-include path.mk # path.mk contains variables specific to each user + # (e.g. FRAMAC, FRAMAC_GUI) and should not be versioned. It is + # an optional include, unnecessary if frama-c is in the PATH. +FRAMAC ?= frama-c # FRAMAC is defined in path.mk when it is included, but the + # user can override it in the command-line. include $(shell $(FRAMAC)-config -scripts)/prologue.mk ############################################################################### -# Edit below as needed. MACHDEP is mandatory. Suggested flags are optional. +# Edit below as needed. Suggested flags are optional. MACHDEP = x86_64