[analysis-scripts] Makefile simplification

Makefile

@@ -259,6 +259,8 @@ DISTRIB_FILES:=\
       share/analysis-scripts/concat-csv.sh                              \
       share/analysis-scripts/clone.sh                                   \
       share/analysis-scripts/creduce.sh                                 \
+      share/analysis-scripts/eva-prefix.mk                              \
+      share/analysis-scripts/eva-suffix.mk                              \
       $(wildcard share/analysis-scripts/examples/*)                     \
       share/analysis-scripts/fc_stubs.c                                 \
       share/analysis-scripts/find_fun.py                                \
@@ -1939,6 +1941,8 @@ install:: install-lib-$(OCAMLBEST)
 	  share/analysis-scripts/concat-csv.sh \
 	  share/analysis-scripts/clone.sh \
 	  share/analysis-scripts/creduce.sh \
+	  share/analysis-scripts/eva-prefix.mk \
+	  share/analysis-scripts/eva-suffix.mk \
 	  share/analysis-scripts/fc_stubs.c \
 	  share/analysis-scripts/find_fun.py \
 	  share/analysis-scripts/flamegraph.pl \

share/analysis-scripts/eva-prefix.mk

+# This Makefile is included by the template used for analyses with Frama-C/Eva.
+
+# For details and usage information, see the Frama-C User Manual.
+
+# Note: this variable must be defined before including any files
+makefile_dir := $(dir $(lastword $(MAKEFILE_LIST)))
+
+## Useful definitions (to be overridden later if needed)
+
+# Improves analysis time, at the cost of extra memory usage
+export FRAMA_C_MEMORY_FOOTPRINT = 8
+
+# frama-c-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 frama-c-path.mk
+
+# FRAMAC is defined in frama-c-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.
+FRAMAC ?= frama-c
+
+# frama-c.mk contains the main rules and targets
+include $(makefile_dir)/frama-c.mk
+
+# Default target
+all: eva
+ifeq ($(TARGETS),)
+	@echo "error: TARGETS is empty"
+endif

share/analysis-scripts/eva-suffix.mk

+# This Makefile is included by the template used for analyses with Frama-C/Eva.
+
+# For details and usage information, see the Frama-C User Manual.
+
+# Some targets provided for convenience
+# Note: they all depend on TARGETS having been properly set by the user
+eva: $(TARGETS)
+parse: $(TARGETS:%.eva=%.parse)
+# Opening one GUI for each target is cumbersome; we open only the first target
+gui: $(firstword $(TARGETS)).gui

share/analysis-scripts/template.mk

 # TEMPLATE FOR MAKEFILE TO USE IN FRAMA-C/EVA CASE STUDIES
 
-# DO NOT EDIT THE LINES BETWEEN THE '#'S
+# For details and usage information, see the Frama-C User Manual.
 
+# Do not modify the block below
 ###############################################################################
-# Improves analysis time, at the cost of extra memory usage
-export FRAMA_C_MEMORY_FOOTPRINT = 8
-#
-# frama-c-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 frama-c-path.mk
-#
-# FRAMAC is defined in frama-c-path.mk when it is included, so the
-# line below will be safely ignored if this is the case
 FRAMAC ?= frama-c
-#
-# frama-c.mk contains the main rules and targets
--include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/frama-c.mk
-#
+include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/eva-prefix.mk
 ###############################################################################
 
-# EDIT VARIABLES AND TARGETS BELOW AS NEEDED
-# The flags below are only suggestions to use with Eva, and can be removed
+# Edit below as needed. Suggested flags are optional.
 
-# (Optional) preprocessing flags, usually handled by -json-compilation-database
+## Preprocessing flags (for -cpp-extra-args)
 CPPFLAGS    +=
 
-# (Optional) Frama-C general flags (parsing and kernel)
+## General flags
 FCFLAGS     += \
   -kernel-warn-key annot:missing-spec=abort \
   -kernel-warn-key typing:implicit-function-declaration=abort \
 
-# (Optional) Eva-specific flags
+## Eva-specific flags
 EVAFLAGS    += \
   -eva-warn-key builtins:missing-spec=abort \
 
-# (MANDATORY) Name of the main target
-MAIN_TARGET :=
+## Analysis targets (suffixed with .eva)
+TARGETS = main.eva
 
-# Remove these lines after defining the main target
-ifeq ($(MAIN_TARGET),)
-$(error MAIN_TARGET not defined in $(firstword $(MAKEFILE_LIST)))
-endif
+### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
+main.parse: \
+  main.c \
 
-# Add other targets if needed
-TARGETS = $(MAIN_TARGET).eva
-
-# Default target
-all: $(TARGETS)
-
-# (MANDATORY) List of source files used by MAIN_TARGET.
-# If there is a JSON compilation database,
-# 'frama-c-script list-files' can help obtain it
-$(MAIN_TARGET).parse:
-
-
-# The following targets are optional and provided for convenience only
-parse: $(TARGETS:%.eva=%.parse)
-loop: $(TARGETS:%.eva=%.parse.loop) $(TARGETS:%=%.loop)
-gui: $(MAIN_TARGET).eva.gui
-
-# Run 'make <TARGET>.eva.loop' to obtain a .loop file, fine-tune it by hand,
-# then rename it to <TARGET>.slevel to prevent it from being overwritten.
-# If such file exists, use it to define per-function slevel values.
-ifneq (,$(wildcard $(MAIN_TARGET).slevel))
-$(MAIN_TARGET).eva: \
-  EVAFLAGS += $(shell cat $(MAIN_TARGET).slevel | tr -d '\n\\')
-endif
+# Do not modify the block below
+###############################################################################
+include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/eva-suffix.mk
+###############################################################################