From 0016909eaf33375aa74d052f478faf11f5b40fae Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Fri, 5 Jun 2020 21:40:42 +0200
Subject: [PATCH] [Analysis-scripts] remove outdated documentation and
examples; userman will replace it
---
Makefile | 4 -
headers/header_spec.txt | 5 -
share/analysis-scripts/README.md | 208 +-----------------
share/analysis-scripts/examples/Makefile | 18 --
.../examples/example-multi.mk | 23 --
.../examples/example-slevel.mk | 37 ----
share/analysis-scripts/examples/example.c | 25 ---
share/analysis-scripts/examples/example.mk | 26 ---
8 files changed, 3 insertions(+), 343 deletions(-)
delete mode 100644 share/analysis-scripts/examples/Makefile
delete mode 100644 share/analysis-scripts/examples/example-multi.mk
delete mode 100644 share/analysis-scripts/examples/example-slevel.mk
delete mode 100644 share/analysis-scripts/examples/example.c
delete mode 100644 share/analysis-scripts/examples/example.mk
diff --git a/Makefile b/Makefile
index 9ed05f8df2f..c39e2faff05 100644
--- a/Makefile
+++ b/Makefile
@@ -261,7 +261,6 @@ DISTRIB_FILES:=\
share/analysis-scripts/clone.sh \
share/analysis-scripts/creduce.sh \
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 \
@@ -1959,9 +1958,6 @@ install:: install-lib-$(OCAMLBEST)
share/analysis-scripts/summary.py \
share/analysis-scripts/template.mk \
$(FRAMAC_DATADIR)/analysis-scripts
- $(MKDIR) $(FRAMAC_DATADIR)/analysis-scripts/examples
- $(CP) share/analysis-scripts/examples/* \
- $(FRAMAC_DATADIR)/analysis-scripts/examples
$(MKDIR) $(FRAMAC_DATADIR)/compliance
$(CP) share/compliance/c11_functions.json \
share/compliance/glibc_functions.json \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 7f8b3e31a97..ca66567d661 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -120,11 +120,6 @@ share/analysis-scripts/fc_stubs.c: .ignore
share/analysis-scripts/frama_c_results.py: .ignore
share/analysis-scripts/cmd-dep.sh: .ignore
share/analysis-scripts/concat-csv.sh: .ignore
-share/analysis-scripts/examples/example.c: .ignore
-share/analysis-scripts/examples/example.mk: .ignore
-share/analysis-scripts/examples/example-multi.mk: .ignore
-share/analysis-scripts/examples/example-slevel.mk: .ignore
-share/analysis-scripts/examples/Makefile: .ignore
share/analysis-scripts/find_fun.py: .ignore
share/analysis-scripts/flamegraph.pl: CDDL
share/analysis-scripts/git_utils.py: .ignore
diff --git a/share/analysis-scripts/README.md b/share/analysis-scripts/README.md
index 3e95700bb8e..a92f12365c5 100644
--- a/share/analysis-scripts/README.md
+++ b/share/analysis-scripts/README.md
@@ -1,206 +1,4 @@
-This directory contains a set of a Makefile and several bash scripts which
-can be used to simplify non-trivial analyses with Frama-C and some of its
-plugins, in particular Eva.
-This Makefile can be included in your own Makefile for the following advantages.
+# Analysis scripts
-1. It ensures that no unnecessary work is done. If you change the Makefile,
- targets that have their command line affected will be rebuilt, but any
- target for which the command line doesn't change won't be rebuilt.
-2. It provides commonly used default parameters for the analysis. Note that
- you can still append new parameters or completely redefine them.
-3. It splits between parsing and analysis, storing outputs in separate
- repositories: <target>.parse for parsing-related outputs, and
- <target>.eva for Eva-related outputs.
-4. It produces several additional outputs after parsing and after an Eva
- analysis:
- * `<target>.parse/parse.log`, or `<target>.eva/eva.log`:
- contain the entire output of the parsing/analysis command,
- * `warnings.log`: only the warnings emitted by Frama-C/Eva,
- * `alarms.csv`: list of emitted alarms in csv form,
- * `metrics.log`: various metrics about the analysis,
- * `stats.txt`: stats about the analysis, such as user time,
- memory consumption, the date of the analysis, coverage of the analysis,
- number of warnings and alarms, and the command line arguments.
-5. It keeps copies of all previous analyses you have done in timestamped
- directories.
-
-
-Getting started
-===============
-
-There is a ready-to-use Makefile skeleton at the end of this section. If you
-want explanations about this Makefile, read this entire section.
-
-Other usage examples are available in Frama-C's Github open-source-case-studies
-repository: https://github.com/Frama-C/open-source-case-studies
-
-(If you have access to Frama-C's development repositories, you can also use
-the examples in `analysis-scripts/examples`.)
-
-Including analysis-scripts
--------------------
-
-This folder contains several shell scripts and, most importantly,
-the `frama-c.mk` file. This file is intended to be included at the top of your
-`GNUmakefile`:
-
-````
-include $(shell frama-c -print-share-path)/analysis-scripts/frama-c.mk
-````
-
-The file is named `GNUmakefile` instead of `Makefile` for pragmatic reasons:
-in GNU Make, the file `GNUmakefile`, if it exists, takes precedence over a
-`Makefile`, which avoid having to rename existing Makefiles and having to
-manually specify the Makefile to use when running make (e.g. via `-f`).
-The analysis-scripts Makefile relies on GNU-specific features anyway.
-
-By default, the scripts use the frama-c binaries located in your `$PATH`
-environment variable. You may want to specify different binaries, but, if you
-want to version your analysis, this path will depend on the computer it is run
-on. So, we recommend you use an unversioned file `frama-c-path.mk`. Add this
-file to your `.gitignore` and define the `FRAMAC` and `FRAMAC_GUI`
-variables there. For instance:
-
-````
-FRAMAC_DIR=frama-c/bin
-FRAMAC=$(FRAMAC_DIR)/frama-c
-FRAMAC_GUI=$(FRAMAC_DIR)/frama-c-gui
-````
-
-And include this file before `frama-c.mk` in your Makefile. As this file
-is computer dependent and unversioned, it will not always be present. Prefix
-the include command with a minus sign `-` to tell `make` to ignore missing
-files:
-
-````
--include frama-c-path.mk
-````
-
-Then, to handle both cases when Frama-C is in the path, and when it is not,
-use the following conditional definition of `FRAMAC` followed by the
-inclusion of `frama-c.mk`:
-
-```
-FRAMAC ?= frama-c
-include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/frama-c.mk
-```
-
-
-Defining analysis global parameters
------------------------------------
-
-Once `frama-c.mk` is included, you may change default values of variables.
-Most usual variables you may want to change are `CPPFLAGS`, `FCFLAGS`
-and `EVAFLAGS`. For example:
-
-````
-CPPFLAGS = -D__I586__
-FCFLAGS += -verbose 0
-EVAFLAGS += -plevel 100
-````
-
-Some arguments are passed to Frama-C from the environment. This is the
-case of the `FRAMA_C_MEMORY_FOOTPRINT` variable. You can set it in your
-Makefile with the following line:
-
-````
-export FRAMA_C_MEMORY_FOOTPRINT = 8
-````
-
-The two steps of the analysis
------------------------------
-
-Parsing might be long on some analyses. The analysis scripts save the result
-of the parsing phase so that it is not redone when modifying only analysis
-parameters but not parsing parameters.
-
-The parsing result is saved in a `<target>.parse` directory while the result
-of the analysis is saved in a `<target>.eva` directory.
-The second automatically depends on the first.
-Thus, each time you require that make build the `.eva` target,
-it will build the `.parse` one first.
-
-````
-all: example.eva
-````
-
-
-Defining analysis sources
--------------------------
-
-To define the set of sources to analyze, you must define them as dependencies
-of your `.parse` target.
-
-````
-example.parse: file1.c file2.c file3.c ...
-````
-
-As they are dependencies, parsing will be remade if the sources change.
-
-
-Defining project-specific parameters
-------------------------------------
-
-You can describe several analyses with the same Makefile. We call these
-analyses "projects". Projects are not likely to share the exact same
-parameters. Thus, it is useful to define these parameters project wise.
-`make` allows this by putting the variable definition after the target. For
-instance:
-
-````
-example.parse: CPPFLAGS += -D__FRAMAC__
-example.eva: FCFLAGS += -main my_main
-example.eva: EVAFLAGS += -slevel 500
-````
-
-
-Full example
-------------
-
-### `GNUmakefile`
-
-````
-# optional include, in case frama-c-path.mk does not exist (frama-c in the PATH)
--include frama-c-path.mk
-# frama-c-config is used to find the analysis scripts and frama-c.mk
-include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/frama-c.mk
-
-# Global parameters
-CPPFLAGS = -D__I586__
-FCFLAGS += -verbose 0
-EVAFLAGS += -plevel 100
-
-export FRAMA_C_MEMORY_FOOTPRINT = 8
-
-# Default targets
-all: example.eva
-
-# Input files
-example.parse: example.c
-
-# Project-specific parameters
-example.parse: CPPFLAGS += -D__FRAMAC__
-example.eva: FCFLAGS += -main my_main
-example.eva: EVAFLAGS += -slevel 500
-````
-
-### `frama-c-path.mk`
-
-````
-FRAMAC_DIR=frama-c/bin
-FRAMAC=$(FRAMAC_DIR)/frama-c
-FRAMAC_GUI=$(FRAMAC_DIR)/frama-c-gui
-````
-
-### `.gitignore`
-
-````
-*.parse*
-*.eva*
-*.crash
-command
-parse.log
-eva.log
-stats.txt
-frama-c-path.mk
-````
+Documentation related to the contents of this directory is available in the
+Frama-C User Manual, chapter "Analysis scripts".
diff --git a/share/analysis-scripts/examples/Makefile b/share/analysis-scripts/examples/Makefile
deleted file mode 100644
index 5aca1b89933..00000000000
--- a/share/analysis-scripts/examples/Makefile
+++ /dev/null
@@ -1,18 +0,0 @@
-TARGETS=example example-multi example-slevel
-
-.PHONY: all update-submodules clean $(TARGETS)
-
-all: $(TARGETS)
-
-update-submodules:
- git submodule update --init --recursive --remote
-
-clean:
- @for f in $(TARGETS); \
- do \
- $(MAKE) --no-print-directory --file $$f.mk clean; \
- done
-
-$(TARGETS): %: %.mk
- @$(MAKE) --no-print-directory --file $<
-
diff --git a/share/analysis-scripts/examples/example-multi.mk b/share/analysis-scripts/examples/example-multi.mk
deleted file mode 100644
index fa25003a712..00000000000
--- a/share/analysis-scripts/examples/example-multi.mk
+++ /dev/null
@@ -1,23 +0,0 @@
--include frama-c-path.mk
-FRAMAC ?= frama-c
--include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/frama-c.mk
-
-# Global parameters
-CPPFLAGS = -D__I586__
-FCFLAGS += -verbose 0
-EVAFLAGS += -plevel 100
-EVABUILTINS += memset:Frama_C_memset memcpy:Frama_C_memcpy
-
-export FRAMA_C_MEMORY_FOOTPRINT = 8
-
-# Default targets
-all: example1.val example2.val
-
-# Input files
-example1.parse example2.parse: example.c
-
-# Project specific parameters
-example1.parse: CPPFLAGS += -D__FRAMAC__
-example1.val: FCFLAGS += -main my_main
-example2.val: EVAFLAGS += -slevel 500
-example2.val: FCFLAGS += -main main
diff --git a/share/analysis-scripts/examples/example-slevel.mk b/share/analysis-scripts/examples/example-slevel.mk
deleted file mode 100644
index d623a913abb..00000000000
--- a/share/analysis-scripts/examples/example-slevel.mk
+++ /dev/null
@@ -1,37 +0,0 @@
-# This example is the same as example-multi.mk but pay attention to the
-# following changes :
-# 1. slevel is set inside SLEVEL variable instead of EVAFLAGS to allow
-# overriding when testing specific slevels
-# 2. A percent (%) is used in example1.% and example2.% so that
-# options are used also for instance for example1.5000.val which
-# is the same target as example1.val but with 5000 slevel.
-# 3. The all rule invoke the script
-
--include frama-c-path.mk
-FRAMAC ?= frama-c
--include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/frama-c.mk
-
-# Global parameters
-CPPFLAGS = -D__I586__
-FCFLAGS += -verbose 0
-EVAFLAGS += -plevel 100
-EVABUILTINS += memset:Frama_C_memset memcpy:Frama_C_memcpy
-
-export FRAMA_C_MEMORY_FOOTPRINT = 8
-
-# Default targets
-all:
- $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/slevel-tweaker.sh -f example-slevel.mk example1 example2
-
-# Clean
-clean::
- $(RM) slevel-tweaker.log
-
-# Input files
-example1.parse example2.parse: example.c
-
-# Project specific parameters
-example1.parse: CPPFLAGS += -D__FRAMAC__
-example1.%: FCFLAGS += -main my_main
-example2.%: SLEVEL += -slevel 500
-example2.%: FCFLAGS += -main main
diff --git a/share/analysis-scripts/examples/example.c b/share/analysis-scripts/examples/example.c
deleted file mode 100644
index ed7983016f1..00000000000
--- a/share/analysis-scripts/examples/example.c
+++ /dev/null
@@ -1,25 +0,0 @@
-#include <string.h>
-
-char s[10], t[10];
-
-int f()
-{
- memset(s, 0, 10);
- memcpy(t, s, 10);
- return 42;
-}
-
-void main(void)
-{
- f();
-}
-
-
-#ifdef __FRAMAC__
-
-int my_main(void)
-{
- return f();
-}
-
-#endif
diff --git a/share/analysis-scripts/examples/example.mk b/share/analysis-scripts/examples/example.mk
deleted file mode 100644
index 4a6130de5b3..00000000000
--- a/share/analysis-scripts/examples/example.mk
+++ /dev/null
@@ -1,26 +0,0 @@
-# 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 should be included at the top of your Makefile, right below
-# the inclusion of frama-c-path.mk
--include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/frama-c.mk
-
-# Define global parameters
-CPPFLAGS += -D__I586__ -D__FRAMAC__
-FCFLAGS += -verbose 0 -main my_main
-EVAFLAGS += -plevel 611
-EVABUILTINS += memset:Frama_C_memset memcpy:Frama_C_memcpy
-
-# Export environment variable for Frama-C
-export FRAMA_C_MEMORY_FOOTPRINT = 8
-
-# Default target
-all: example.val
-
-# List input files
-example.parse: example.c
--
GitLab