From 45002bc77cd211c2bd586a30e1ccc085672a4f33 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 27 Jul 2020 18:38:28 +0200
Subject: [PATCH] [analysis-scripts] several fixes after review

---
 share/analysis-scripts/analysis.mk | 4 +---
 share/analysis-scripts/prologue.mk | 6 ------
 share/analysis-scripts/template.mk | 9 ++++++---
 tests/fc_script/oracle/GNUmakefile | 9 ++++++---
 4 files changed, 13 insertions(+), 15 deletions(-)

diff --git a/share/analysis-scripts/analysis.mk b/share/analysis-scripts/analysis.mk
index fa832425b12..8a4d48e462d 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 c58dda47db1..f1cca3d3888 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 b5f1566cb46..114d2cd6f80 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 22642475059..5b9a464e26f 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
 
-- 
GitLab