Commit 5e9ed98e authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[ivette] merge with master

parent c87f8a06
......@@ -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
......
......@@ -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
......
......@@ -911,6 +911,7 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
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
......@@ -2339,7 +2340,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) $@
......@@ -2351,7 +2374,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 #
......
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
......@@ -1020,9 +1020,7 @@ 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.
operational yet).
As said in Section~\ref{ptests:configuration}, these directives can be
found in different places:
......
......@@ -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$
......
......@@ -1112,8 +1112,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 +1124,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
......@@ -1369,6 +1369,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
......@@ -1451,6 +1453,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,6 +2,7 @@
# --- Template .gitignore file for Dome
# --------------------------------------------------------------------------
.ivette
.dome-*.stamp
.dome-*.back
node_modules
......
......@@ -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
# --------------------------------------------------------------------------
......
/* --- Generated Frama-C Server API --- */
/**
Ast Services
@packageDocumentation
@module api/kernel/ast
*/
//@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';
//@ts-ignore
import { byTag } from 'api/kernel/data';
//@ts-ignore
import { byText } from 'api/kernel/data';
//@ts-ignore
import { jTag } from 'api/kernel/data';
//@ts-ignore
import { jTagSafe } from 'api/kernel/data';
//@ts-ignore
import { jText } from 'api/kernel/data';
//@ts-ignore
import { jTextSafe } from 'api/kernel/data';
//@ts-ignore
import { tag } from 'api/kernel/data';
//@ts-ignore
import { text } from 'api/kernel/data';
const compute_internal: Server.ExecRequest<null,null> = {
kind: Server.RqKind.EXEC,
name: 'kernel.ast.compute',
input: Json.jNull,
output: Json.jNull,
};
/** Ensures that AST is computed */
export const compute: Server.ExecRequest<null,null>= compute_internal;
/** Marker kind */
export enum markerKind {
/** Variable */
variable = 'variable',
/** Function */
function = 'function',
/** Expression */
expression = 'expression',
/** Lvalue */
lvalue = 'lvalue',
/** Declaration */
declaration = 'declaration',
/** Statement */
statement = 'statement',
/** Global */
global = 'global',
/** Term */
term = 'term',
/** Property */
property = 'property',
}
/** Loose decoder for `markerKind` */
export const jMarkerKind: Json.Loose<markerKind> = Json.jEnum(markerKind);
/** Safe decoder for `markerKind` */
export const jMarkerKindSafe: Json.Safe<markerKind> =
Json.jFail(Json.jEnum(markerKind),'kernel.ast.markerKind expected');
/** Natural order for `markerKind` */
export const byMarkerKind: Compare.Order<markerKind> =
Compare.byEnum(markerKind);
const markerKindTags_internal: Server.GetRequest<null,tag[]> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.markerKindTags',
input: Json.jNull,
output: Json.jList(jTag),
};
/** Registered tags for the above type. */
export const markerKindTags: Server.GetRequest<null,tag[]>= markerKindTags_internal;
/** Data for array rows [`markerInfo`](#markerinfo) */
export interface markerInfoData {
/** Entry identifier. */
key: Json.key<'#markerInfo'>;
/** Marker kind */
kind: markerKind;
/** Marker short name */
name: string;
/** Marker declaration or description */
descr: string;
}
/** Loose decoder for `markerInfoData` */
export const jMarkerInfoData: Json.Loose<markerInfoData> =
Json.jObject({
key: Json.jFail(Json.jKey<'#markerInfo'>('#markerInfo'),
'#markerInfo expected'),
kind: jMarkerKindSafe,
name: Json.jFail(Json.jString,'String expected'),
descr: Json.jFail(Json.jString,'String expected'),
});
/** Safe decoder for `markerInfoData` */
export const jMarkerInfoDataSafe: Json.Safe<markerInfoData> =
Json.jFail(jMarkerInfoData,'MarkerInfoData expected');
/** Natural order for `markerInfoData` */
export const byMarkerInfoData: Compare.Order<markerInfoData> =
Compare.byFields
<{ key: Json.key<'#markerInfo'>, kind: markerKind, name: string,
descr: string }>({
key: Compare.primitive,
kind: byMarkerKind,
name: Compare.alpha,
descr: Compare.primitive,
});
/** Signal for array [`markerInfo`](#markerinfo) */
export const signalMarkerInfo: Server.Signal = {
name: 'kernel.ast.signalMarkerInfo',
};
const reloadMarkerInfo_internal: Server.GetRequest<null,null> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.reloadMarkerInfo',
input: Json.jNull,
output: Json.jNull,
};
/** Force full reload for array [`markerInfo`](#markerinfo) */
export const reloadMarkerInfo: Server.GetRequest<null,null>= reloadMarkerInfo_internal;
const fetchMarkerInfo_internal: Server.GetRequest<
number,
{ pending: number, updated: markerInfoData[],
removed: Json.key<'#markerInfo'>[], reload: boolean }
> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.fetchMarkerInfo',
input: Json.jNumber,
output: Json.jObject({
pending: Json.jFail(Json.jNumber,'Number expected'),
updated: Json.jList(jMarkerInfoData),
removed: Json.jList(Json.jKey<'#markerInfo'>('#markerInfo')),
reload: Json.jFail(Json.jBoolean,'Boolean expected'),
}),
};
/** Data fetcher for array [`markerInfo`](#markerinfo) */
export const fetchMarkerInfo: Server.GetRequest<
number,
{ pending: number, updated: markerInfoData[],
removed: Json.key<'#markerInfo'>[], reload: boolean }
>= fetchMarkerInfo_internal;
const markerInfo_internal: State.Array<
Json.key<'#markerInfo'>,
markerInfoData
> = {