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

[Analysis-scripts] remove outdated documentation and examples; userman will replace it

parent fb38eaff
......@@ -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 \
......
......@@ -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
......
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".
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 $<
-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
# 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
#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
# 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
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