...
 
Commits (238)
......@@ -55,6 +55,7 @@ autom4te.cache
/tests/journal/intra.byte
/tests/misc/my_visitor_plugin/my_visitor.opt
/tests/misc/my_visitor.sav
/tests/spec/preprocess_dos.c
/tests/*/*.opt
/tests/pdg/*.dot
......@@ -92,6 +93,8 @@ autom4te.cache
/doc/acsl/
/doc/aorai/aorai-example.tgz
/doc/aorai/aorai-example/
/doc/aorai/frama-c-aorai-example.tgz
/doc/aorai/frama-c-aorai-example
/doc/aorai/main.pdf
......
......@@ -140,21 +140,16 @@ internal_nightly:
tags:
- nix
frama-c-ocaml-4.06:
frama-c-ocaml-4.09:
variables:
OCAML: "4_06"
OCAML: "4_09"
<<: *frama-c-ocaml
only:
- schedules
frama-c-ocaml-4.07:
frama-c-ocaml-4.10:
variables:
OCAML: "4_07"
<<: *frama-c-ocaml
frama-c-ocaml-4.05:
variables:
OCAML: "4_05"
OCAML: "4_10"
<<: *frama-c-ocaml
......
......@@ -41,7 +41,7 @@ macOS has opam through Homebrew.
Windows users can install opam via WSL (Windows Subsystem for Linux).
If your system does not have an opam package >= 2.0.0, you can
[compile it from source]((#compiling-from-source)),
[compile it from source](#compiling-from-source),
or use the provided opam binaries available at:
http://opam.ocaml.org/doc/Install.html
......
......@@ -254,22 +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 \
$(wildcard share/analysis-scripts/examples/*) \
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/function_finder.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 \
......@@ -827,7 +829,7 @@ $(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
PLUGIN_ENABLE:=$(ENABLE_EVA)
PLUGIN_NAME:=Eva
PLUGIN_DIR:=src/plugins/value
PLUGIN_EXTRA_DIRS:=engine values domains domains/cvalue domains/apron \
PLUGIN_EXTRA_DIRS:=engine values domains api domains/cvalue domains/apron \
domains/gauges domains/equality legacy partitioning utils gui_files \
values/numerors domains/numerors
PLUGIN_TESTS_DIRS+=value/traces
......@@ -910,10 +912,12 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
partitioning/partitioning_index partitioning/trace_partitioning \
engine/mem_exec engine/iterator engine/initialization \
engine/compute_functions engine/analysis register \
api/general_requests \
utils/unit_tests \
$(APRON_CMO) $(NUMERORS_CMO)
PLUGIN_CMI:= values/abstract_value values/abstract_location \
domains/abstract_domain domains/simpler_domains
PLUGIN_DEPENDENCIES:=Callgraph LoopAnalysis RteGen
PLUGIN_DEPENDENCIES:=Callgraph LoopAnalysis RteGen Server
# These files are used by the GUI, but do not depend on Lablgtk
VALUE_GUI_AUX:=gui_files/gui_types gui_files/gui_eval \
......@@ -1501,11 +1505,11 @@ endif
$(DOC_DIR)/docgen.cmo: $(DOC_DIR)/docgen.ml
$(PRINT_OCAMLC) $@
$(OCAMLC) -c -I +ocamldoc -I $(CONFIG_DIR) $(DOC_DIR)/docgen.ml
$(OCAMLC) -c -I +ocamldoc -I +compiler-libs -I $(CONFIG_DIR) $(DOC_DIR)/docgen.ml
$(DOC_DIR)/docgen.cmxs: $(DOC_DIR)/docgen.ml
$(PRINT_PACKING) $@
$(OCAMLOPT) -o $@ -shared -I +ocamldoc -I $(CONFIG_DIR) \
$(OCAMLOPT) -o $@ -shared -I +ocamldoc -I +compiler-libs -I $(CONFIG_DIR) \
$(DOC_DIR)/docgen.ml
clean-doc::
......@@ -1935,29 +1939,30 @@ 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/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/function_finder.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 \
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 \
......@@ -2338,7 +2343,29 @@ PTESTS_SRC=ptests/ptests_config.ml ptests/ptests.ml
# that does not contain a 'tests' dir
PTESTS_CONFIG:= $(shell if test -d tests; then echo tests/ptests_config; fi)
ptests: bin/ptests.$(OCAMLBEST)$(EXE) $(PTESTS_CONFIG)
ifneq ("$(PTESTS_CONFIG)","")
GENERATED_TESTS:=tests/spec/preprocess_dos.c
else
GENERATED_TESTS:=
endif
tests/spec/preprocess_dos.c: tests/spec/preprocess_dos.c.in \
Makefile share/Makefile.config
$(RM) $@
$(SED) -e "s|@UNIX2DOS@|$(PP_DOS_UNIX2DOS)|g" \
-e "s|@DONTRUN@|$(PP_DOS_DONTRUN)|g" \
$< > $@
$(CHMOD_RO) $@
ifneq ("$(HAS_UNIX2DOS)","no")
tests/spec/preprocess_dos.c: PP_DOS_UNIX2DOS=$(UNIX2DOS)
tests/spec/preprocess_dos.c: PP_DOS_DONTRUN=
else
tests/spec/preprocess_dos.c: PP_DOS_UNIX2DOS=unix2dos
tests/spec/preprocess_dos.c: PP_DOS_DONTRUN=DONTRUN: no unix2dos found
endif
ptests: bin/ptests.$(OCAMLBEST)$(EXE) $(PTESTS_CONFIG) $(GENERATED_TESTS)
bin/ptests.byte$(EXE): $(PTESTS_SRC)
$(PRINT_LINKING) $@
......@@ -2350,7 +2377,7 @@ bin/ptests.opt$(EXE): $(PTESTS_SRC)
$(OCAMLOPT) -I ptests -dtypes -thread -o $@ \
unix.cmxa threads.cmxa str.cmxa dynlink.cmxa $^
GENERATED+=ptests/ptests_config.ml tests/ptests_config
GENERATED+=ptests/ptests_config.ml tests/ptests_config $(GENERATED_TESTS)
#######################
# Source distribution #
......
......@@ -35,27 +35,27 @@ usage() {
echo " Display this help message and exit."
echo ""
echo " - make-template [dir]"
echo " Interactively prepares a template for running analysis scripts,"
echo " writing it to [dir/GNUmakefile]. [dir] is [.] if omitted."
echo " Interactively prepares a template for analyses,"
echo " writing it to dir/GNUmakefile [default: .frama-c]."
echo ""
echo " - make-path"
echo " - make-path [dir]"
echo " [for Frama-C developers and advanced users without Frama-C in the path]"
echo " Creates a frama-c-path.mk file in the current working directory."
echo " Creates a path.mk file in dir [default: .frama-c]."
echo ""
echo " - list-files [path/to/compile_commands.json]"
echo " Lists all sources in the given compile_commands.json"
echo " (defaults to './compile_commands.json' if omitted)."
echo " [default: ./compile_commands.json]."
echo " Also lists files defining a 'main' function"
echo " (heuristics-based; neither correct nor complete)."
echo ""
echo " - flamegraph <flamegraph.txt> [dir]"
echo " Generates flamegraph.svg and flamegraph.html in [dir]"
echo " (or in the FRAMAC_SESSION directory by default)."
echo " - flamegraph flamegraph.txt [dir]"
echo " Generates flamegraph.svg and flamegraph.html in dir"
echo " [default: FRAMAC_SESSION]."
echo " Also opens it in a browser, unless variable NOGUI is set."
echo ""
echo " - find-fun <function-name> [dirs]"
echo " Lists files in [dirs] declaring or defining <function-name>"
echo " (defaults to PWD + /usr/include)."
echo " - find-fun function-name [dir...]"
echo " Lists files in dir... declaring or defining function-name"
echo " [default: PWD /usr/include]."
echo " Heuristics-based: neither correct nor complete."
echo ""
echo " - summary [options]"
......@@ -63,20 +63,20 @@ usage() {
echo " in the current PWD."
echo " Use $0 summary --help for more informations."
echo ""
echo " - configure <machdep>"
echo " - configure machdep"
echo " Runs an existing configure script to only consider files"
echo " in Frama-C's libc; this will hopefully disable non-essential"
echo " and non-POSIX external libraries."
echo " <machdep> is necessary to define a required preprocessor symbol"
echo " (run 'frama-c -machdep' help to get the list of machdeps)."
echo " (run 'frama-c -machdep help' to get the list of machdeps)."
echo ""
echo " - make-wrapper <target> <args>"
echo " Runs 'make <target> <args>', parsing the output to suggest"
echo " - make-wrapper target arg..."
echo " Runs 'make target arg...', parsing the output to suggest"
echo " useful commands in case of failure."
echo ""
echo " - normalize-jcdb [path/to/compile_commands.json]"
echo " Applies some transformations to an existing compile_commands.json"
echo " (such as relativizing paths) to improve portability"
echo " (such as relativizing paths) to improve portability."
echo " [default: ./compile_commands.json]"
exit $1
}
......@@ -85,7 +85,7 @@ if [ $# -lt 1 ]; then
fi
DIR="$( cd "$( dirname "$0" )" && pwd )"
FRAMAC_SHARE=$("${DIR}/frama-c-config" -print-share-path)
FRAMAC_SHARE=$("${DIR}/frama-c-config" -share)
if [ -z ${FRAMAC_SESSION+x} ]; then
FRAMAC_SESSION="./.frama-c";
fi
......@@ -121,17 +121,31 @@ open_file() {
}
make_path() {
cat <<EOF > frama-c-path.mk
dir=".frama-c"
if [ "$#" -gt 0 ]; then
dir="$1"
fi
if [ ! -d "$dir" ]; then
read -p "Directory '$dir' does not exist. Create it? [y/N] " yn
case $yn in
[Yy])
mkdir -p "$dir"
;;
*)
echo "Exiting without creating."
exit 0;;
esac
fi
cat <<EOF > "${dir}/path.mk"
FRAMAC_DIR=${DIR}
ifeq (\$(wildcard \$(FRAMAC_DIR)),)
# Frama-C not installed locally; using the version in the PATH
else
FRAMAC=\$(FRAMAC_DIR)/frama-c
FRAMAC_GUI=\$(FRAMAC_DIR)/frama-c-gui
FRAMAC_CONFIG=\$(FRAMAC_DIR)/frama-c-config
endif
EOF
echo "Wrote to: frama-c-path.mk"
echo "Wrote to: ${dir}/path.mk"
}
flamegraph() {
......@@ -232,11 +246,12 @@ case "$command" in
;;
"make-template")
shift;
${FRAMAC_SHARE}/analysis-scripts/make_template.py "$0" "$@";
export FRAMAC="${DIR}/frama-c"
${FRAMAC_SHARE}/analysis-scripts/make_template.py "$@";
;;
"make-path")
shift;
make_path;
make_path "$@";
;;
"list-files")
shift;
......
export FRAMAC_WP_CACHE=update
export FRAMAC_WP_CACHEDIR=$WP_QUALIF_CACHE
......@@ -657,14 +657,6 @@ REQUIRE_LABLGTK=
USE_LABLGTK=
HAS_LABLGTK=
# Tool declarations
####################
DOT=
REQUIRE_DOT=
USE_DOT=
HAS_DOT=
### Now plugin declarations
PLUGINS_FORCE_LIST=
......@@ -957,6 +949,11 @@ configure_library([LABLGTK],
configure_tool([DOT],[dot],[dot not found: you should install GraphViz],no)
configure_tool([UNIX2DOS],[unix2dos],
[unix2dos not found: you should install tofrodos],no)
plugin_use_external(tests,unix2dos)
########################
# Plug-in dependencies #
########################
......@@ -974,8 +971,6 @@ EXTERNAL_PLUGINS="${EXTERNAL_PLUGINS} ${EXTRA_EXTERNAL_PLUGINS}"
AC_SUBST(PLATFORM)
AC_SUBST(VERBOSEMAKE)
AC_SUBST(DEVELOPMENT)
AC_SUBST(DOT)
AC_SUBST(HAS_DOT)
AC_SUBST(HAS_APRON)
AC_SUBST(HAS_MPFR)
AC_SUBST(HAS_LANDMARKS)
......
Docker images for Frama-C
=========================
- To build a new image (slim, without Frama-C sources nor tests):
cd <tag>
docker build . --target base -t framac/frama-c:<tag>
- To run an interactive shell:
docker run -it framac/frama-c:<tag>
- To push to Docker Hub (requires access to the `framac/frama-c` repository):
docker push framac/frama-c:<tag>
- To build an image containing Frama-C sources (downloaded from the .tar.gz, in
directory `/root`):
cd <tag>
docker build . --build-arg with_source=yes \
-t framac/frama-c:<tag>-with-source
- To run Frama-C tests (and remove unnecessary image later):
cd <tag>
docker build . --build-arg with_source=yes --build-arg with_test=yes \
-t framac/frama-c:<tag>-with-test
docker image rm framac/frama-c:<tag>-with-test
FROM debian:sid as base
RUN apt update
RUN apt install opam -y
RUN opam init --disable-sandboxing --compiler=ocaml-base-compiler.4.05.0 -y
# "RUN eval $(opam env)" does not work, so we manually set its variables
ENV OPAM_SWITCH_PREFIX "/root/.opam/ocaml-base-compiler.4.05.0"
ENV CAML_LD_LIBRARY_PATH "/root/.opam/ocaml-base-compiler.4.05.0/lib/stublibs:/root/.opam/ocaml-base-compiler.4.05.0/lib/ocaml/stublibs:/root/.opam/ocaml-base-compiler.4.05.0/lib/ocaml"
ENV OCAML_TOPLEVEL_PATH "/root/.opam/ocaml-base-compiler.4.05.0/lib/toplevel"
ENV MANPATH "$MANPATH:/root/.opam/ocaml-base-compiler.4.05.0/man"
ENV PATH "/root/.opam/ocaml-base-compiler.4.05.0/bin:$PATH"
RUN opam update -y
RUN opam install depext -y
# Install packages from reference configuration
RUN opam depext --install -y \
alt-ergo.2.0.0 \
apron.20160125 \
conf-graphviz.0.1 \
mlgmpidl.1.2.11 \
ocamlfind.1.8.0 \
ocamlgraph.1.8.8 \
ppx_deriving_yojson.3.5.2 \
why3.1.2.0 \
yojson.1.7.0 \
zarith.1.9.1 \
--verbose # intentionally left as last line in this RUN command
RUN why3 config --detect-provers
# with_source: keep Frama-C sources
ARG with_source=no
RUN cd /root && \
wget http://frama-c.com/download/frama-c-20.0-Calcium.tar.gz && \
tar xvf frama-c-*.tar.gz && \
(cd frama-c-* && \
./configure --disable-gui && \
make -j && \
make install \
) && \
rm -f frama-c-*.tar.gz && \
[ "${with_source}" != "no" ] || rm -rf frama-c-*
# with_test: run Frama-C tests; requires "with_source=yes"
ARG with_test=no
RUN if [ "${with_test}" != "no" ]; then \
opam depext --install -y \
conf-python-3.1.0.0 \
conf-time.1 \
--verbose \
&& \
apt install python -y && \
cd /root/frama-c-* && \
make tests; \
fi
FROM debian:sid as base
RUN apt update
RUN apt install opam -y
RUN opam init --disable-sandboxing --compiler=ocaml-base-compiler.4.07.1 -y
# "RUN eval $(opam env)" does not work, so we manually set its variables
ENV OPAM_SWITCH_PREFIX "/root/.opam/ocaml-base-compiler.4.07.1"
ENV CAML_LD_LIBRARY_PATH "/root/.opam/ocaml-base-compiler.4.07.1/lib/stublibs:/root/.opam/ocaml-base-compiler.4.07.1/lib/ocaml/stublibs:/root/.opam/ocaml-base-compiler.4.07.1/lib/ocaml"
ENV OCAML_TOPLEVEL_PATH "/root/.opam/ocaml-base-compiler.4.07.1/lib/toplevel"
ENV MANPATH "$MANPATH:/root/.opam/ocaml-base-compiler.4.07.1/man"
ENV PATH "/root/.opam/ocaml-base-compiler.4.07.1/bin:$PATH"
RUN opam update -y
RUN opam install depext -y
# Install packages from reference configuration
RUN opam depext --install -y \
alt-ergo.2.0.0 \
apron.v0.9.12 \
conf-graphviz.0.1 \
mlgmpidl.1.2.12 \
ocamlfind.1.8.0 \
ocamlgraph.1.8.8 \
ppx_deriving_yojson.3.5.2 \
why3.1.3.1 \
yojson.1.7.0 \
zarith.1.9.1 \
zmq.5.1.3 \
--verbose # intentionally left as last line in this RUN command
RUN why3 config --full-config
# with_source: keep Frama-C sources
ARG with_source=no
RUN cd /root && \
wget http://frama-c.com/download/frama-c-21.0-Scandium.tar.gz && \
tar xvf frama-c-*.tar.gz && \
(cd frama-c-* && \
./configure --disable-gui && \
make -j && \
make install \
) && \
rm -f frama-c-*.tar.gz && \
[ "${with_source}" != "no" ] || rm -rf frama-c-*
# with_test: run Frama-C tests; requires "with_source=yes"
ARG with_test=no
RUN if [ "${with_test}" != "no" ]; then \
opam depext --install -y \
conf-python-3.1.0.0 \
conf-time.1 \
--verbose \
&& \
cd /root/frama-c-* && \
make tests; \
fi
FROM debian:sid as base
RUN apt update
RUN apt install opam -y
RUN opam init --disable-sandboxing --compiler=ocaml-base-compiler.4.07.1 -y
# "RUN eval $(opam env)" does not work, so we manually set its variables
ENV OPAM_SWITCH_PREFIX "/root/.opam/ocaml-base-compiler.4.07.1"
ENV CAML_LD_LIBRARY_PATH "/root/.opam/ocaml-base-compiler.4.07.1/lib/stublibs:/root/.opam/ocaml-base-compiler.4.07.1/lib/ocaml/stublibs:/root/.opam/ocaml-base-compiler.4.07.1/lib/ocaml"
ENV OCAML_TOPLEVEL_PATH "/root/.opam/ocaml-base-compiler.4.07.1/lib/toplevel"
ENV MANPATH "$MANPATH:/root/.opam/ocaml-base-compiler.4.07.1/man"
ENV PATH "/root/.opam/ocaml-base-compiler.4.07.1/bin:$PATH"
RUN opam update -y
RUN opam install depext -y
# Install packages from reference configuration
RUN opam depext --install -y \
alt-ergo.2.0.0 \
apron.v0.9.12 \
conf-graphviz.0.1 \
mlgmpidl.1.2.12 \
ocamlfind.1.8.0 \
ocamlgraph.1.8.8 \
ppx_deriving_yojson.3.5.2 \
why3.1.3.1 \
yojson.1.7.0 \
zarith.1.9.1 \
zmq.5.1.3 \
--verbose # intentionally left as last line in this RUN command
RUN why3 config --full-config
# with_source: keep Frama-C sources
ARG with_source=no
RUN cd /root && \
wget http://frama-c.com/download/frama-c-21.1-Scandium.tar.gz && \
tar xvf frama-c-*.tar.gz && \
(cd frama-c-* && \
./configure --disable-gui && \
make -j && \
make install \
) && \
rm -f frama-c-*.tar.gz && \
[ "${with_source}" != "no" ] || rm -rf frama-c-*
# with_test: run Frama-C tests; requires "with_source=yes"
ARG with_test=no
RUN if [ "${with_test}" != "no" ]; then \
opam depext --install -y \
conf-python-3.1.0.0 \
conf-time.1 \
--verbose \
&& \
cd /root/frama-c-* && \
make tests; \
fi
......@@ -130,11 +130,11 @@ struct
match_s
rel
in
if StringSet.mem match_s known_types_names then
if String.Set.mem match_s known_types_names then
"<a href=\"" ^ self#path match_s ^ Naming.complete_target Naming.mark_type
match_s ^"\">" ^ s_final ^ "</a>"
else
if StringSet.mem match_s known_classes_names then
if String.Set.mem match_s known_classes_names then
let (html_file, _) = Naming.html_files match_s in
"<a href=\""^ self#path html_file ^ html_file^"\">"^s_final^"</a>"
else
......@@ -158,7 +158,7 @@ struct
match_s
rel
in
if StringSet.mem match_s known_modules_names then
if String.Set.mem match_s known_modules_names then
let (html_file, _) = Naming.html_files match_s in
"<a href=\"" ^ self#path match_s ^ html_file^"\">"^s_final^"</a>"
else
......@@ -287,7 +287,7 @@ struct
let types = Odoc_info.Search.types module_list in
known_types_names <-
List.fold_left
(fun acc t -> StringSet.add t.Odoc_type.ty_name acc)
(fun acc t -> String.Set.add t.Odoc_type.ty_name acc)
known_types_names
types ;
......@@ -296,12 +296,12 @@ struct
let class_types = Odoc_info.Search.class_types module_list in
known_classes_names <-
List.fold_left
(fun acc c -> StringSet.add c.Odoc_class.cl_name acc)
(fun acc c -> String.Set.add c.Odoc_class.cl_name acc)
known_classes_names
classes ;
known_classes_names <-
List.fold_left
(fun acc ct -> StringSet.add ct.Odoc_class.clt_name acc)
(fun acc ct -> String.Set.add ct.Odoc_class.clt_name acc)
known_classes_names
class_types ;
......@@ -310,12 +310,12 @@ struct
let modules = Odoc_info.Search.modules module_list in
known_modules_names <-
List.fold_left
(fun acc m -> StringSet.add m.m_name acc)
(fun acc m -> String.Set.add m.m_name acc)
known_modules_names
modules ;
known_modules_names <-
List.fold_left
(fun acc mt -> StringSet.add mt.mt_name acc)
(fun acc mt -> String.Set.add mt.mt_name acc)
known_modules_names
module_types ;
......
......@@ -990,6 +990,15 @@ file, run it only once.
test
& \textit{None}
\\
& \texttt{TIMEOUT}\nscodeidxdef{Test!Directive}{TIMEOUT}
& kill the test after the given duration and report a failure
& \textit{None}
\\
& \texttt{NOFRAMAC}\nscodeidxdef{Test!Directive}{NOFRAMAC}
& empty the list of frama-c commands to be launched
(\texttt{EXEC} and \texttt{EXECNOW} directives are still executed).
& \textit{None}
\\
\hline \multirow{2}{23mm}{\centering{Test suite}}
& \texttt{DONTRUN}\nscodeidxdef{Test!Directive}{DONTRUN}
& Do not execute this test
......@@ -1017,12 +1026,16 @@ test
Any directive can identify a file using a relative path.
The default directory considered for \texttt{.} is always the parent
directory of directory \texttt{tests}\codeidx{tests}. The
\texttt{DONTRUN} directive does not need to have any content, but it
is useful to provide an explanation of why the test should not be run
({\it e.g} test of a feature that is currently developed and not fully
operational yet). If a test file is explicitly given on the command
line of \ptests, it is always executed, regardless of the presence of
a \texttt{DONTRUN} directive.
\texttt{DONTRUN} and \texttt{NOFRAMAC} directives
do not need to have any content, but it might be
useful to provide an explanation of why the test should not be run
({\it e.g} test of a feature that is under development and not fully
operational yet).
If there are \texttt{OPT}/\texttt{STDOPT} directives \textit{after} a
\texttt{NOFRAMAC} directive, they will be executed, unless
they are themselves discarded by another subsequent \texttt{NOFRAMAC}
directive.
As said in Section~\ref{ptests:configuration}, these directives can be
found in different places:
......
......@@ -5,6 +5,12 @@
This chapter summarizes the major changes in this documentation between each
\framac release, from newest to oldest.
\section*{Frama-C+dev}
\begin{itemize}
\item \textbf{Testing}: Document new directives \texttt{TIMEOUT} and
\texttt{NOFRAMAC}
\end{itemize}
\section*{21.0 Scandium}
\begin{itemize}
\item \textbf{Configure}: Documentation of \texttt{configure\_pkg},
......@@ -13,13 +19,13 @@ This chapter summarizes the major changes in this documentation between each
\section*{20.0 Calcium}
\begin{itemize}
\item \textbf{Ptests}: Documentation of the new directive \texttt{MODULE}.
\item \textbf{Testing}: Documentation of the new directive \texttt{MODULE}.
\end{itemize}
\section*{19.0 Potassium}
\begin{itemize}
\item \textbf{ACSL Extension}: Document new \texttt{status} flag for registration functions
\item \textbf{Testing}: Document of usage \texttt{@@} in a directive
\item \textbf{Testing}: Document usage of \texttt{@@} in a directive
\item \textbf{Profiling with Landmarks}: New section
\end{itemize}
......
......@@ -548,11 +548,11 @@ For this tutorial, there will be no such source code. A file
\texttt{./tests/hello/hello\_test.c} is then created:
\listingname{./tests/hello/hello\_test.c}
\sscodeidx{Test}{Directive}{OPT}
\nscodeidx{Test!Directive}{OPT}
\lstinputlisting[style=c]{./tutorial/hello/generated/with_test/tests/hello/hello_test.c}
In this file, there is only one directive
\texttt{OPT: -hello}\sscodeidx{Test}{Directive}{OPT} which requires
\texttt{OPT: -hello}\nscodeidx{Test!Directive}{OPT} which requires
to run \framac on this test with the \texttt{-hello} option.
A look at Section~\ref{ptests:directives} gives you an idea of the kind of
directives which can be used to test plug-ins.
......
......@@ -88,7 +88,7 @@ body {
#NAVIGATION a.root {
display: block;
font-family: "Optima", "Verdana", "Arial", sans;
font-size: 10pt;
font-size: 16pt;
margin-top: 1cm;
margin-bottom: 6mm;
}
......@@ -105,13 +105,23 @@ body {
}
#NAVIGATION ul {
width: 6cm ;
width: 8cm ;
margin: 0px ;
padding: 0px ;
}
#NAVIGATION li {
list-style-type: none;
margin: 0px;
padding-left: 8px;
}
#NAVIGATION ul > ul {
margin-left: 0px ;
padding-top: 2px ;
padding-bottom: 2px ;
#TOC > a {
font-weight: bold;
}
.TOC > ul > li > a {
font-weight: bold;
}
/* -------------------------------------------------------------------------- */
......
......@@ -23,7 +23,7 @@
$if(toc)$
$for(link)$
$if(link.toc)$
$table-of-contents$
<div class="TOC">$table-of-contents$</div>
$else$
<li><a href="$link.href$.html">$link.title$</a></li>
$endif$
......
......@@ -111,26 +111,24 @@ 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
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/function_finder.py: .ignore
share/analysis-scripts/git_utils.py: .ignore
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
......@@ -1112,8 +1110,6 @@ src/plugins/server/Server.mli: .ignore
src/plugins/server/configure.ac: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/data.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/data.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/doc.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/doc.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/jbuffer.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/jbuffer.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/kernel_ast.ml: CEA_LGPL_OR_PROPRIETARY
......@@ -1126,16 +1122,18 @@ src/plugins/server/kernel_properties.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/kernel_properties.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/main.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/main.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/package.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/package.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/request.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/request.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/server_doc.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/server_doc.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/server_parameters.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/server_parameters.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/server_batch.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/server_zmq.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/states.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/states.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/syntax.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/syntax.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/scope/Scope.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/scope/datascope.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/scope/datascope.mli: CEA_LGPL_OR_PROPRIETARY
......@@ -1208,6 +1206,8 @@ src/plugins/value/Changelog_non_free: .ignore
src/plugins/value/Eva.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/alarmset.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/alarmset.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/general_requests.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/general_requests.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/abstract_domain.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/printer_domain.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/printer_domain.mli: CEA_LGPL_OR_PROPRIETARY
......@@ -1367,6 +1367,8 @@ src/plugins/value/utils/state_import.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/state_import.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/structure.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/structure.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/unit_tests.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/unit_tests.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/value_perf.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/value_perf.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/value_results.ml: CEA_LGPL_OR_PROPRIETARY
......@@ -1449,6 +1451,8 @@ src/plugins/wp/.gitignore: .ignore
src/plugins/wp/.ocp-indent: .ignore
src/plugins/wp/Auto.ml: CEA_WP
src/plugins/wp/Auto.mli: CEA_WP
src/plugins/wp/Cache.ml: CEA_WP
src/plugins/wp/Cache.mli: CEA_WP
src/plugins/wp/Cfloat.ml: CEA_WP
src/plugins/wp/Cfloat.mli: CEA_WP
src/plugins/wp/Changelog: .ignore
......
react@^16.8 react-dom source-map-support lodash react-virtualized react-draggable codemirror
react@^16.8 react-dom source-map-support lodash react-virtualized react-draggable react-fast-compare codemirror
......@@ -2,10 +2,10 @@
# --- Template .gitignore file for Dome
# --------------------------------------------------------------------------
.ivette
.dome-*.stamp
.dome-*.back
node_modules
yarn.lock
yarn-error.log
/bin
/dist
......
......@@ -30,6 +30,18 @@ fixlint: dome-pkg dome-templ
tsc: typecheck fixlint
# --------------------------------------------------------------------------
# --- Frama-C API
# --------------------------------------------------------------------------
.PHONY: api
api:
@echo "[Ivette] Generating TypeScript API"
@find api -name "*.ts" -exec rm -f {} \;
../bin/frama-c.byte -load-module api/server_tsc.ml -server-tsc
@find api -name "*.ts" -exec chmod a-w {} \;
# --------------------------------------------------------------------------
# --- Ivette Documentation
# --------------------------------------------------------------------------
......
This diff is collapsed.
/* --- Generated Frama-C Server API --- */
/**
Informations
@packageDocumentation
@module api/kernel/data
*/
//@ts-ignore
import * as Json from 'dome/data/json';
//@ts-ignore
import * as Compare from 'dome/data/compare';
//@ts-ignore
import * as Server from 'frama-c/server';
//@ts-ignore
import * as State from 'frama-c/states';
/** Markdown (inlined) text. */
export type markdown = string;
/** Loose decoder for `markdown` */
export const jMarkdown: Json.Loose<markdown> = Json.jString;
/** Safe decoder for `markdown` */
export const jMarkdownSafe: Json.Safe<markdown> =
Json.jFail(Json.jString,'String expected');
/** Natural order for `markdown` */
export const byMarkdown: Compare.Order<markdown> = Compare.string;
/** Rich text format uses `[tag; …text ]` to apply the tag `tag` to the enclosed text. Empty tag `""` can also used to simply group text together. */
export type text = null | string | text[];
/** Loose decoder for `text` */
export const jText: Json.Loose<text> =
(_x: any) => Json.jUnion<null | string | text[]>(
Json.jNull,
Json.jString,
Json.jList(jText),
)(_x);
/** Safe decoder for `text` */
export const jTextSafe: Json.Safe<text> =
(_x: any) => Json.jFail(jText,'Text expected')(_x);
/** Natural order for `text` */
export const byText: Compare.Order<text> =
(_x: any, _y: any) => Compare.structural(_x,_y);
/** Enum Tag Description */
export type tag = { name: string, label: markdown, descr: markdown };
/** Loose decoder for `tag` */
export const jTag: Json.Loose<tag> =
Json.jObject({
name: Json.jFail(Json.jString,'String expected'),
label: jMarkdownSafe,
descr: jMarkdownSafe,
});
/** Safe decoder for `tag` */
export const jTagSafe: Json.Safe<tag> = Json.jFail(jTag,'Tag expected');
/** Natural order for `tag` */
export const byTag: Compare.Order<tag> =
Compare.byFields
<{ name: string, label: markdown, descr: markdown }>({
name: Compare.alpha,
label: byMarkdown,
descr: byMarkdown,
});
/* ------------------------------------- */
/* --- Generated Frama-C Server API --- */
/**
Project Management
@packageDocumentation
@module api/kernel/project
*/
//@ts-ignore
import * as Json from 'dome/data/json';
//@ts-ignore
import * as Compare from 'dome/data/compare';
//@ts-ignore
import * as Server from 'frama-c/server';
//@ts-ignore
import * as State from 'frama-c/states';
/** Project informations */
export type projectInfo =
{ id: Json.key<'#project'>, name: string, current: boolean };
/** Loose decoder for `projectInfo` */
export const jProjectInfo: Json.Loose<projectInfo> =
Json.jObject({
id: Json.jFail(Json.jKey<'#project'>('#project'),'#project expected'),
name: Json.jFail(Json.jString,'String expected'),
current: Json.jFail(Json.jBoolean,'Boolean expected'),
});
/** Safe decoder for `projectInfo` */
export const jProjectInfoSafe: Json.Safe<projectInfo> =
Json.jFail(jProjectInfo,'ProjectInfo expected');
/** Natural order for `projectInfo` */
export const byProjectInfo: Compare.Order<projectInfo> =
Compare.byFields
<{ id: Json.key<'#project'>, name: string, current: boolean }>({
id: Compare.string,
name: Compare.alpha,
current: Compare.boolean,
});
/** Request to be executed on the specified project. */
export type projectRequest =
{ project: Json.key<'#project'>, request: string, data: Json.json };
/** Loose decoder for `projectRequest` */
export const jProjectRequest: Json.Loose<projectRequest> =
Json.jObject({
project: Json.jFail(Json.jKey<'#project'>('#project'),
'#project expected'),
request: Json.jFail(Json.jString,'String expected'),
data: Json.jAny,
});
/** Safe decoder for `projectRequest` */
export const jProjectRequestSafe: Json.Safe<projectRequest> =
Json.jFail(jProjectRequest,'ProjectRequest expected');
/** Natural order for `projectRequest` */
export const byProjectRequest: Compare.Order<projectRequest> =
Compare.byFields
<{ project: Json.key<'#project'>, request: string, data: Json.json }>({
project: Compare.string,
request: Compare.string,
data: Compare.structural,
});
const getCurrent_internal: Server.GetRequest<null,projectInfo> = {
kind: Server.RqKind.GET,
name: 'kernel.project.getCurrent',
input: Json.jNull,
output: jProjectInfo,
};
/** Returns the current project */
export const getCurrent: Server.GetRequest<null,projectInfo>= getCurrent_internal;
const setCurrent_internal: Server.SetRequest<Json.key<'#project'>,null> = {
kind: Server.RqKind.SET,
name: 'kernel.project.setCurrent',
input: Json.jKey<'#project'>('#project'),
output: Json.jNull,
};
/** Switches the current project */
export const setCurrent: Server.SetRequest<Json.key<'#project'>,null>= setCurrent_internal;
const getList_internal: Server.GetRequest<null,projectInfo[]> = {
kind: Server.RqKind.GET,
name: 'kernel.project.getList',
input: Json.jNull,
output: Json.jList(jProjectInfo),
};
/** Returns the list of all projects */
export const getList: Server.GetRequest<null,projectInfo[]>= getList_internal;
const getOn_internal: Server.GetRequest<projectRequest,Json.json> = {
kind: Server.RqKind.GET,
name: 'kernel.project.getOn',
input: jProjectRequest,
output: Json.jAny,
};
/** Execute a GET request within the given project */
export const getOn: Server.GetRequest<projectRequest,Json.json>= getOn_internal;