Commit fb38eaff authored by Andre Maroneze's avatar Andre Maroneze Committed by Valentin Perrelle
Browse files

[Analyis-scripts] rename several files to avoid confusion

parent 13bfd49d
......@@ -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 \
......
......@@ -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
......
......@@ -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 &
......
##########################################################################
# #
# 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
# 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
# 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
##########################################################################
# #
# 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
# 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
###############################################################################
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment