[analysis-scripts] several fixes after review

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 $@

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.

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
 

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