From fb38eaffde77171bcc0858c9a3aff738f9b92318 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Fri, 5 Jun 2020 21:39:48 +0200
Subject: [PATCH] [Analyis-scripts] rename several files to avoid confusion
---
Makefile | 15 +++---
headers/header_spec.txt | 4 +-
.../{frama-c.mk => analysis.mk} | 28 +++++------
share/analysis-scripts/epilogue.mk | 37 ++++++++++++++
share/analysis-scripts/eva-prefix.mk | 31 ------------
share/analysis-scripts/eva-suffix.mk | 10 ----
share/analysis-scripts/prologue.mk | 49 +++++++++++++++++++
share/analysis-scripts/template.mk | 20 ++++----
8 files changed, 118 insertions(+), 76 deletions(-)
rename share/analysis-scripts/{frama-c.mk => analysis.mk} (90%)
create mode 100644 share/analysis-scripts/epilogue.mk
delete mode 100644 share/analysis-scripts/eva-prefix.mk
delete mode 100644 share/analysis-scripts/eva-suffix.mk
create mode 100644 share/analysis-scripts/prologue.mk
diff --git a/Makefile b/Makefile
index 0e163c8baef..9ed05f8df2f 100644
--- a/Makefile
+++ b/Makefile
@@ -254,24 +254,24 @@ DISTRIB_FILES:=\
Changelog config.h.in \
VERSION VERSION_CODENAME $(wildcard licenses/*) \
$(LIBC_FILES) \
+ share/analysis-scripts/analysis.mk \
share/analysis-scripts/benchmark_database.py \
share/analysis-scripts/cmd-dep.sh \
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/epilogue.mk \
$(wildcard share/analysis-scripts/examples/*) \
share/analysis-scripts/fc_stubs.c \
share/analysis-scripts/find_fun.py \
share/analysis-scripts/flamegraph.pl \
- share/analysis-scripts/frama-c.mk \
share/analysis-scripts/frama_c_results.py \
share/analysis-scripts/git_utils.py \
share/analysis-scripts/list_files.py \
share/analysis-scripts/make_template.py \
share/analysis-scripts/make_wrapper.py \
share/analysis-scripts/parse-coverage.sh \
+ share/analysis-scripts/prologue.mk \
share/analysis-scripts/README.md \
share/analysis-scripts/results_display.py \
share/analysis-scripts/summary.py \
@@ -1936,23 +1936,24 @@ install:: install-lib-$(OCAMLBEST)
share/configure.ac share/autocomplete_frama-c share/_frama-c \
$(FRAMAC_DATADIR)
$(MKDIR) $(FRAMAC_DATADIR)/analysis-scripts
- $(CP) share/analysis-scripts/benchmark_database.py \
+ $(CP) \
+ share/analysis-scripts/analysis.mk \
+ share/analysis-scripts/benchmark_database.py \
share/analysis-scripts/cmd-dep.sh \
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/epilogue.mk \
share/analysis-scripts/fc_stubs.c \
share/analysis-scripts/find_fun.py \
share/analysis-scripts/flamegraph.pl \
- share/analysis-scripts/frama-c.mk \
share/analysis-scripts/frama_c_results.py \
share/analysis-scripts/git_utils.py \
share/analysis-scripts/list_files.py \
share/analysis-scripts/make_template.py \
share/analysis-scripts/make_wrapper.py \
share/analysis-scripts/parse-coverage.sh \
+ share/analysis-scripts/prologue.mk \
share/analysis-scripts/README.md \
share/analysis-scripts/results_display.py \
share/analysis-scripts/summary.py \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 67258fcf5c5..7f8b3e31a97 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -111,11 +111,12 @@ ptests/.gitignore: .ignore
ptests/.merlin: .ignore
ptests/ptests.ml: CEA_LGPL
share/_frama-c: CEA_LGPL
+share/analysis-scripts/analysis.mk: CEA_LGPL
share/analysis-scripts/benchmark_database.py: .ignore
share/analysis-scripts/clone.sh: .ignore
share/analysis-scripts/creduce.sh: CEA_LGPL
+share/analysis-scripts/epilogue.mk: CEA_LGPL
share/analysis-scripts/fc_stubs.c: .ignore
-share/analysis-scripts/frama-c.mk: CEA_LGPL
share/analysis-scripts/frama_c_results.py: .ignore
share/analysis-scripts/cmd-dep.sh: .ignore
share/analysis-scripts/concat-csv.sh: .ignore
@@ -131,6 +132,7 @@ share/analysis-scripts/list_files.py: .ignore
share/analysis-scripts/make_template.py: .ignore
share/analysis-scripts/make_wrapper.py: .ignore
share/analysis-scripts/parse-coverage.sh: .ignore
+share/analysis-scripts/prologue.mk: CEA_LGPL
share/analysis-scripts/README.md: .ignore
share/analysis-scripts/results_display.py: .ignore
share/analysis-scripts/summary.py: .ignore
diff --git a/share/analysis-scripts/frama-c.mk b/share/analysis-scripts/analysis.mk
similarity index 90%
rename from share/analysis-scripts/frama-c.mk
rename to share/analysis-scripts/analysis.mk
index 32e09ef1365..442a2533434 100644
--- a/share/analysis-scripts/frama-c.mk
+++ b/share/analysis-scripts/analysis.mk
@@ -20,24 +20,19 @@
# #
##########################################################################
-# This file is intended to be included by a classic Makefile when doing
-# non-trivial analyses with Frama-C and its Eva plugin. For instance, you
-# can start your Makefile with the following line:
-#
-# include path/to/frama-c.mk
+# Makefile for Frama-C/Eva case studies.
+# This file is included by epilogue.mk, when using template.mk.
+# See the Frama-C User Manual for more details.
#
# This Makefile uses the following variables.
#
-# FRAMAC the frama-c binary
-# FRAMAC_GUI the frama-c gui binary
+# FRAMAC frama-c binary
+# FRAMAC_GUI frama-c gui binary
# CPPFLAGS preprocessing flags
-# MACHDEP machdep to use with frama-c
+# MACHDEP machdep
# FCFLAGS general flags to use with frama-c
# FCGUIFLAGS flags to use with frama-c-gui
# EVAFLAGS flags to use with the Eva plugin
-# SLEVEL the part of the frama-c command line concerning slevel
-# (you can use EVAFLAGS for this, if you don't intend
-# to use slevel-tweaker.sh)
# EVABUILTINS Eva builtins to be set (via -eva-builtin)
# EVAUSESPECS Eva functions to be overridden by specs (-eva-use-spec)
#
@@ -53,15 +48,14 @@
# With command line arguments:
# make FRAMAC=~/bin/frama-c
#
-# In your Makefile, when you want to change a parameter for all analyses :
+# In your Makefile, when you want to change a parameter for all analyses:
# FCFLAGS += -verbose 2
#
# In your Makefile, for a single target :
# target.eva: FCFLAGS += -main my_main
#
-# In order to define an analysis target named target, you must in addition
-# give the list of source files containing the code to be analyzed by adding
-# them as dependencies of target.parse, a in
+# For each analysis target, you must give the list of sources to be analyzed
+# by adding them as prerequisites of target.parse, as in:
#
# target.parse: file1.c file2.c file3.c...
#
@@ -72,6 +66,8 @@ ifneq (4.0,$(firstword $(sort $(MAKE_VERSION) 4.0)))
endif
# Test if on a Mac (and therefore sed has fewer options)
+# Also test if /usr/bin/time is available, otherwise use the shell builtin
+# (which has less options)
UNAME := $(shell uname -s)
ifeq ($(UNAME),Darwin)
SED_UNBUFFERED:=sed
@@ -147,7 +143,6 @@ clean-backups:
# --- Generic rules ---
-TIMESTAMP := $(shell date +"%Y-%m-%d_%H-%M-%S")
HR_TIMESTAMP := $(shell date +"%H:%M:%S %d/%m/%Y")# Human readable
DIR := $(dir $(lastword $(MAKEFILE_LIST)))
SHELL := /bin/bash
@@ -227,7 +222,6 @@ SHELL := /bin/bash
fi
mv $@/{running,command}
touch $@ # Update timestamp and prevents remake if nothing changes
- cp -r $@ $*_$(TIMESTAMP).eva
%.gui: %
$(FRAMAC_GUI) $(FCGUIFLAGS) -load $^/framac.sav &
diff --git a/share/analysis-scripts/epilogue.mk b/share/analysis-scripts/epilogue.mk
new file mode 100644
index 00000000000..5918ddd031b
--- /dev/null
+++ b/share/analysis-scripts/epilogue.mk
@@ -0,0 +1,37 @@
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2020 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+# Makefile template epilogue 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
+
+# Default target
+all: eva
+ifeq ($(TARGETS),)
+ @echo "error: TARGETS is empty"
+endif
diff --git a/share/analysis-scripts/eva-prefix.mk b/share/analysis-scripts/eva-prefix.mk
deleted file mode 100644
index cdefc9dba75..00000000000
--- a/share/analysis-scripts/eva-prefix.mk
+++ /dev/null
@@ -1,31 +0,0 @@
-# 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
diff --git a/share/analysis-scripts/eva-suffix.mk b/share/analysis-scripts/eva-suffix.mk
deleted file mode 100644
index 315463c057e..00000000000
--- a/share/analysis-scripts/eva-suffix.mk
+++ /dev/null
@@ -1,10 +0,0 @@
-# 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
diff --git a/share/analysis-scripts/prologue.mk b/share/analysis-scripts/prologue.mk
new file mode 100644
index 00000000000..c58dda47db1
--- /dev/null
+++ b/share/analysis-scripts/prologue.mk
@@ -0,0 +1,49 @@
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2020 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+# Makefile template prologue for Frama-C/Eva case studies.
+# 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
+
+# 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.
+FRAMAC ?= frama-c
+
+# analysis.mk contains the main rules and targets
+include $(makefile_dir)/analysis.mk
+
+# Default target
+all: eva
diff --git a/share/analysis-scripts/template.mk b/share/analysis-scripts/template.mk
index 650d75de6a5..63cc973ba42 100644
--- a/share/analysis-scripts/template.mk
+++ b/share/analysis-scripts/template.mk
@@ -1,15 +1,13 @@
-# TEMPLATE FOR MAKEFILE TO USE IN FRAMA-C/EVA CASE STUDIES
-
+# Makefile template for Frama-C/Eva case studies.
# For details and usage information, see the Frama-C User Manual.
-# Do not modify the block below
-###############################################################################
--include frama-c-path.mk
+### Prologue. Do not modify this block. #######################################
+-include path.mk
FRAMAC ?= frama-c
-include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/eva-prefix.mk
+include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/prologue.mk
###############################################################################
-# Edit below as needed. Suggested flags are optional.
+# Edit below as needed. MACHDEP is mandatory. Suggested flags are optional.
MACHDEP = x86_32
@@ -25,6 +23,9 @@ FCFLAGS += \
EVAFLAGS += \
-eva-warn-key builtins:missing-spec=abort \
+## GUI-only flags
+FCGUIFLAGS +=
+
## Analysis targets (suffixed with .eva)
TARGETS = main.eva
@@ -32,7 +33,6 @@ TARGETS = main.eva
main.parse: \
main.c \
-# Do not modify the block below
-###############################################################################
-include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/eva-suffix.mk
+### Epilogue. Do not modify this block. #######################################
+include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
###############################################################################
--
GitLab