diff --git a/Makefile b/Makefile
index 6b917cf38ef061f06e297d00a414b01557f93c12..a75258ec1333bfce384a7762ad4fef0e04a75926 100644
--- a/Makefile
+++ b/Makefile
@@ -79,6 +79,7 @@ PLUGIN_TYPES_CMX_LIST :=
PLUGIN_DEP_LIST:=
PLUGIN_DOC_LIST :=
PLUGIN_DOC_DIRS :=
+PLUGIN_DOC_DUMP_LIST :=
PLUGIN_DISTRIBUTED_LIST:=
PLUGIN_DIST_TARGET_LIST:=
PLUGIN_DIST_DOC_LIST:=
@@ -1241,7 +1242,9 @@ FILES_FOR_OCAMLDEP+= $(addsuffix /*.mli,$(FRAMAC_SRC_DIRS)) \
MODULES_TODOC+=$(filter-out $(MODULES_NODOC),\
$(MLI_ONLY) \
- $(filter-out $(PLUGIN_TYPES_CMO_LIST:.cmo=.mli),$(CMO:.cmo=.mli)))
+ $(filter-out $(PLUGIN_TYPES_CMO_LIST:.cmo=.mli),$(CMO:.cmo=.mli)) \
+ $(STARTUP_CMO:.cmo=.mli) \
+)
################################
# toplevel.{byte,opt} binaries #
@@ -1707,26 +1710,32 @@ $(CHECK_API_DIR)/check_code.cmo: $(CHECK_API_DIR)/check_code.ml
$(CHECK_API_DIR)/check_code.cmxs: $(CHECK_API_DIR)/check_code.ml
$(PRINT_PACKING) $@
- $(OCAMLOPT) -o $@ -shared -I +ocamldoc \
- str.cmxa $(CHECK_API_DIR)/check_code.ml
+ $(OCAMLOPT) -package ocamldoc -o $@ -shared \
+ $(CHECK_API_DIR)/check_code.ml
CHECK_CODE=$(CHECK_API_DIR)/check_code.cmxs
-.PHONY: check-devguide
-check-devguide: $(CHECK_CODE) $(DOC_DEPEND) $(DOC_DIR)/kernel-doc.ocamldoc
+.PHONY: check-devguide devguide
+devguide: byte $(OCAMLBEST)
+ $(MAKE) FRAMAC_INTERNAL=no -C $(DOC_DEV_DIR)
+
+check-devguide: $(CHECK_CODE) $(DOC_DEPEND) $(DOC_DIR)/kernel-doc.ocamldoc plugins-doc devguide
$(PRINT) 'Checking developer guide consistency'
$(MKDIR) $(CHECK_API_DIR)/html
+ $(RM) $(CHECK_API_DIR)/code_file
+ $(foreach doc_dump, \
+ $(DOC_DIR)/kernel-doc.ocamldoc $(PLUGIN_DOC_DUMP_LIST), \
$(OCAMLDOC) $(DOC_FLAGS) -I $(OCAMLLIB) \
-g $(CHECK_CODE) \
-passopt -docdevpath -passopt "`pwd`/$(CHECK_API_DIR)" \
- -load $(DOC_DIR)/kernel-doc.ocamldoc \
- -d $(CHECK_API_DIR)/html
+ -load $(doc_dump) \
+ -d $(CHECK_API_DIR)/html; )
$(RM) -r $(CHECK_API_DIR)/html
$(MAKE) --silent -C $(CHECK_API_DIR) main.idx
$(MAKE) --silent -C $(CHECK_API_DIR) >$(CHECK_API_DIR)/summary.txt
$(ECHO) see all the information displayed here \
in $(CHECK_API_DIR)/summary.txt
- $(RM) code_file
+
################################
# Code prettyfication and lint #
################################
diff --git a/doc/developer/Makefile b/doc/developer/Makefile
index eb5f0c6b5a53b6139548bf6d9ca0565bf0d57c2d..1cbfb017507f9121e986f180d1f76ece692b5e36 100644
--- a/doc/developer/Makefile
+++ b/doc/developer/Makefile
@@ -34,15 +34,18 @@ DEPENDENCIES= $(FRAMAC_MODERN) $(GENERATED) frama-c-book.cls
all: developer.pdf check
-FRAMAC := $(shell command -v frama-c 2> /dev/null)
+FC_BINDIR:=$(FRAMAC_ROOT_SRCDIR)/bin
+
+.PHONY: clean-tuto
+clean-tuto:
+ $(RM) ../../lib/plugins/META.frama-c-hello ../../lib/plugins/META.frama-c-viewcfg
+ $(RM) ../../lib/plugins/top/Hello.* ../../lib/plugins/top/Viewcfg.*
# local plugin.cmi (if any) is in conflict with the one of Frama-C
check: $(GENERATED)
-ifndef FRAMAC
- $(ECHO) frama-c is not installed in the PATH, nothing to check!
-else
+ $(MAKE) clean-tuto
$(ECHO) Checking compilation of example scripts
- ../../bin/frama-c \
+ $(FC_BINDIR)/frama-c \
-load-script ./examples/syntactic_check \
-load-script ./examples/callstack \
-load-script ./examples/use_callstack \
@@ -56,17 +59,21 @@ else
exit 1; \
fi
for i in value value_gui_options visitor ; \
- do ../../bin/frama-c -load-script ./tutorial/viewcfg/generated/$$i/cfg_print.ml ; \
+ do $(FC_BINDIR)/frama-c -load-script ./tutorial/viewcfg/generated/$$i/cfg_print.ml ; \
done
for i in with_options with_log with_registration ; \
- do ../../bin/frama-c -load-script ./tutorial/hello/generated/$$i/hello_world.ml ; \
+ do $(FC_BINDIR)/frama-c -load-script ./tutorial/hello/generated/$$i/hello_world.ml ; \
done
$(ECHO) compilation ok
- $(MAKE) -C tutorial/hello/generated/with_test
- $(MAKE) -C tutorial/hello/generated/makefile_multiple
- $(MAKE) -C tutorial/hello/generated/makefile_single
- $(MAKE) -C tutorial/viewcfg/generated/split
-endif
+ $(MAKE) clean-tuto
+ PATH=$(FC_BINDIR):$$PATH; $(MAKE) DEVELOPMENT=no PTESTS_OPTS=-error-code -C tutorial/hello/generated/with_test byte opt tests
+ $(MAKE) clean-tuto
+ PATH=$(FC_BINDIR):$$PATH; $(MAKE) DEVELOPMENT=no PTESTS_OPTS=-error-code -C tutorial/hello/generated/makefile_multiple opt
+ $(MAKE) clean-tuto
+ PATH=$(FC_BINDIR):$$PATH; $(MAKE) DEVELOPMENT=no PTESTS_OPTS=-error-code -C tutorial/hello/generated/makefile_single opt
+ $(MAKE) clean-tuto
+ PATH=$(FC_BINDIR):$$PATH; $(MAKE) DEVELOPMENT=no PTESTS_OPTS=-error-code -C tutorial/viewcfg/generated/split opt
+ $(MAKE) clean-tuto
check-all: developer.pdf
$(MAKE) -C ../.. check-devguide
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 73cc5d5d77990e09a6e63e77a6b78ace38cdbd80..2411abb40fa31470341b7d1219e21d06f43dbd80 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -131,7 +131,7 @@ lexicographic ordering.
For instance, Section \emph{Wished Plug-in} introduces a new sub-section for
the plug-in \texttt{occurrence} in the following way.
-\codeidxdef{check\_plugin}
+\scodeidxdef{configure.in}{check\_plugin}
\begin{configurecode}
# occurrence
############
@@ -1593,9 +1593,10 @@ that can be used instead of the basic ones:
debugging level are sufficient.
%%item
- \logprintf{with\_log}{ f ?kind}%
- Emits a message like \texttt{log}, and finally pass the generated
- message to the continuation $f$, and returns its result.
+ \logprintf{logwith}{ f ?wkey ?emitwith ?once}%
+ Emits a message like \texttt{warning}, and finally pass the generated
+ \texttt{event} (or \texttt{None}) to the continuation $f$,
+ and returns its result.
\end{description}
The default kind is \lstinline{Result}, but all the other kind of
@@ -1643,9 +1644,6 @@ own, in addition to the one automatically created for your plug-in.
\logroutine{log\_channel}{ channel ?kind ?prefix}%
This routine is similar to the \lstinline{log} one.
-%%item
- \logroutine{with\_log\_channel}{ channel f ?kind ?prefix}%
- This routine is similar to the \lstinline{with_log} one.
\end{description}
With both logging routines, you may specify a prefix to be used during
@@ -1784,8 +1782,9 @@ module implements a datastructure, it usually implements
\begin{example}
The following line of code pretty prints whether two statements are equal.
-\sscodeidx{Cil\_datatype}{Stmt}{pretty}
-\sscodeidx{Cil\_datatype}{Stmt}{equal}
+\scodeidx{Cil\_datatype}{Stmt}
+\sscodeidx{Datatype}{S\_no\_copy}{equal}
+\sscodeidx{Datatype}{S\_no\_copy}{pretty}
\begin{ocamlcode}
(* assuming the type of [stmt1] and [stmt2] is Cil_types.stmt *)
Format.fprintf
@@ -1801,7 +1800,8 @@ Format.fprintf
Module \texttt{Datatype.String}\scodeidx{Datatype}{String} implements
\texttt{Datatype.S\_with\_collections}. Thus you can initialize a set of strings
in the following way.
-\sscodeidx{Datatype}{String}{Set}
+\scodeidx{Datatype}{String}
+\sscodeidx{Datatype}{S\_with\_collections}{Set}
\begin{ocamlcode}
let string_set =
List.fold_left
@@ -1957,7 +1957,8 @@ Here is how to apply \texttt{Datatype.Polymorphic} corresponding to the type
\scodeidx{Structural\_descr}{pack}
\scodeidx{Structural\_descr}{p\_int}
\scodeidx{Datatype}{Int}
-\sscodeidx{Datatype}{String}{Hashtbl}
+\scodeidx{Datatype}{String}
+\sscodeidx{Datatype}{S\_with\_collections}{Hashtbl}
\scodeidx{Datatype}{List}
\scodeidx{Type}{par}
\begin{ocamlcode}
@@ -2308,13 +2309,12 @@ plug-in-defined types in an abstract way through the functor
There is no current example in the \framac open-source part, but consider a
plug-in which provides a dynamic API for callstacks as follows.
\scodeidx{Plugin}{Register}
-\scodeidx{Kernel\_function}{t}
-\scodeidx{Kernel\_function}{ty}
-\scodeidx{Kernel\_function}{pretty}
+\codeidx{Kernel\_function}
+\sscodeidx{Datatype}{Ty}{t}
+\sscodeidx{Datatype}{Ty}{ty}
+\sscodeidx{Datatype}{S\_no\_copy}{pretty}
\scodeidx{Kernel\_function}{dummy}
-\sscodeidx{Cil\_datatype}{Stmt}{t}
-\sscodeidx{Cil\_datatype}{Stmt}{ty}
-\sscodeidx{Cil\_datatype}{Stmt}{pretty}
+\scodeidx{Cil\_datatype}{Stmt}
\scodeidx{Cil}{dummyStmt}
\scodeidx{Datatype}{Serializable\_undefined}
\ocamlinput{./examples/generated/callstack.ml}
@@ -2322,8 +2322,10 @@ plug-in which provides a dynamic API for callstacks as follows.
You have to use the functor \texttt{Type.Abstract} to access to the type value
corresponding to the type of callstacks (and thus to access to the above
dynamically registered functions).
-\scodeidx{Kernel\_function}{ty}
-\sscodeidx{Cil\_datatype}{Stmt}{ty}
+\codeidx{Kernel\_function}
+\sscodeidx{Datatype}{Ty}{ty}
+\scodeidx{Cil\_datatype}{Stmt}
+\sscodeidx{Datatype}{Ty}{t}
\scodeidx{Type}{Abstract}
\scodeidx{Dynamic}{get}
\scodeidx{Datatype}{func}
@@ -2448,7 +2450,10 @@ following.
value analysis would not be consistent anymore with the current entry point,
leading to incorrect results.
\begin{example}
-\sscodeidx{Db}{Value}{is\_computed}
+\scodeidx{Analysis}{is\_computed}
+\sscodeidx{Eva}{Analysis}{is\_computed}
+\scodeidx{Analysis}{compute}
+\sscodeidx{Eva}{Analysis}{compute}
~
\begin{ocamlcode}
@@ -2503,8 +2508,10 @@ In most non-\framac applications, a state is a global mutable value. One can use
it to store results of analyses. For example, using this mechanism inside
\framac to create a \texttt{state} which would memoize\index{Memoization} some
information attached to statements would result in the following piece of code.
-\scodeidx{Kernel\_function}{t} \scodeidx{Cil\_types}{varinfo}
-\sscodeidx{Cil\_datatype}{Stmt}{Hashtbl} \sscodeidx{Db}{Value}{compute}
+\codeidx{Kernel\_function}\sscodeidx{Datatype}{Ty}{t}
+\scodeidx{Cil\_types}{varinfo}
+\scodeidx{Cil\_datatype}{Stmt}\sscodeidx{Datatype}{S\_with\_collections}{Hashtbl}
+\sscodeidx{Db}{Value}{compute}
\begin{ocamlcode}
open Cil_datatype
type info = Kernel_function.t * Cil_types.varinfo
@@ -2961,8 +2968,9 @@ code.
\subsection{Definition}\label{options:definition}
In \framac, a parameter is represented by a value of type
-\texttt{Typed\_parameter.t}\scodeidxdef{Typed\_parameter}{t} and by a module
-implementing the signature
+\texttt{Typed\_parameter.t}\codeidxdef{Typed\_parameter}
+\sscodeidx{Datatype}{Ty}{t}
+and by a module implementing the signature
\texttt{Parameter\_sig.S}\scodeidxdef{Parameter\_sig}{S}. The first
representation is a low-level one required by emitters\index{Emitter} (see
Section~\ref{adv:annotations}) and the GUI. The second one provides a high-level
@@ -3786,10 +3794,10 @@ risk sharing\index{Sharing} the same AST\index{AST!Sharing|see{Sharing}}).
\index{Visitor!Behavior|bfit}
The visitors take as argument a
-\verb+visitor_behavior+\scodeidx{Cil}{visitor\_behavior}, which comes in two
-flavors: \verb+inplace_visit+\scodeidx{Cil}{inplace\_visit}%
-\index{Visitor!In-Place|bfit} and \verb+copy_visit+%
-\scodeidx{Cil}{copy\_visit}\index{Visitor!Copy|bfit}. In the in-place mode,
+\verb+Visitor_behavior.t+\scodeidx{Visitor\_behavior}{t}, which comes in two
+flavors: \verb+inplace+\scodeidx{Visitor\_behavior}{inplace}%
+\index{Visitor!In-Place|bfit} and \verb+copy+%
+\scodeidx{Visitor\_behavior}{copy}\index{Visitor!Copy|bfit}. In the in-place mode,
nodes are visited in place, while in the copy mode, nodes are copied and the
visit is done on the copy\index{AST!Copying}. For the nodes
shared\index{Sharing} across the AST
@@ -3802,32 +3810,37 @@ shared\index{Sharing} across the AST
\verb+logic_info+\scodeidx{Cil\_types}{logic\_info} and
\verb+fieldinfo+\scodeidx{Cil\_types}{fieldinfo}), sharing is of course
preserved, and the mapping between the old nodes and their copy can be
-manipulated explicitly through the following functions:
+manipulated explicitly through the following modules, which define a function
+for each of the types above.
\begin{itemize}
\item
- \verb+reset_behavior_+\emph{name}
- \scodeidxdef{Cil}{reset\_behavior\_varinfo}
- resets the mapping corresponding to the type \emph{name}.
-\item \verb+get_original_+\emph{name}\scodeidxdef{Cil}{get\_original\_varinfo}
- gets the original value corresponding to a copy (and behaves as the identity
- if the given value is not known).
-\item \verb+get_+\emph{name}\scodeidxdef{Cil}{get\_varinfo} gets the copy
+ \verb+Reset+\scodeidxdef{Visitor\_behavior}{Reset}
+ allows to reset the mappings.
+\item \verb+Get+\scodeidxdef{Visitor\_behavior}{Get} gets the copy
corresponding to an old value. If the given value is not known, it behaves as
the identity.
-\item \verb+set_+\emph{name}\scodeidxdef{Cil}{set\_varinfo} sets a copy for a
+\item \verb+Memo+\scodeidxdef{Visitor\_behavior}{Memo} is similar to
+ \verb+Get+, except that if the given value is not known, a new binding is
+ created.
+\item \verb+Get_orig+\scodeidxdef{Visitor\_behavior}{Get\_orig}
+ gets the original value corresponding to a copy (and behaves as the identity
+ if the given value is not known).
+\item \verb+Set+\emph{name}\scodeidxdef{Visitor\_behavior}{Set} sets a copy for a
given value. Be sure to use it before any occurrence of the old value has
been copied, or sharing will be lost.
+\item \verb+Set_orig+\scodeidxdef{Visitor\_behavior}{Set\_orig} sets the original
+ value corresponding to a given copy.
\end{itemize}
\begin{important}
- \verb+get_original_+\emph{name} functions allow to retrieve additional
+ Functions from the \verb+Get_orig+\emph{name} modules allow to retrieve additional
information tied to the original AST nodes. Its result must not be modified
in place\index{AST!Modification} (this would defeat the purpose of operating
on a copy to leave the original AST untouched). Moreover, note that whenever
the index used for \emph{name} is modified in the copy, the internal state of
the visitor behavior\index{Visitor!Behavior} must be updated accordingly
- (\emph{via} the \verb+set_+\emph{name} function) for
- \verb+get_original_+\emph{name} to give correct results.\index{Consistency}
+ (\emph{via} the \verb+Set.+\emph{name} function) for
+ \verb+Get_orig.+\emph{name} to give correct results.\index{Consistency}
\end{important}
The list of such indices is given Figure~\ref{fig:idx-visitor}.
@@ -3903,7 +3916,7 @@ whether the table entries are visited before or after the children in the AST.
Here is a small copy visitor that adds an assertion for each
division in the program, stating that the divisor is not zero:
\scodeidx{Visitor}{generic\_frama\_c\_visitor}
-\scodeidx{Cil}{copy\_visit}
+\scodeidx{Visitor\_behavior}{copy}
\scodeidx{Cil}{lzero}
\sscodeidx{Cil}{cilVisitor}{vexpr}
\sscodeidx{Cil\_types}{exp\_node}{BinOp}
@@ -3917,8 +3930,8 @@ division in the program, stating that the divisor is not zero:
\scodeidx{File}{create\_project\_from\_visitor}
\scodeidx{Annotations}{add\_assert}
\sscodeidx{Db}{Main}{extend}
-\scodeidx{Cil}{get\_stmt}
-\scodeidx{Cil}{get\_kernel\_function}
+\sscodeidx{Visitor\_behavior}{Get}{stmt}
+\sscodeidx{Visitor\_behavior}{Get}{kernel\_function}
\sscodeidx{Cil}{cilVisitor}{behavior}
\scodeidx{Ast}{self}
\sscodeidx{Cil}{cilVisitor}{current\_kinstr}
@@ -3977,12 +3990,13 @@ Such clauses can be of different categories, as described by
\scodeidx{Cil\_types}{ext\_category}\texttt{Cil\_types.ext\_category}.
\begin{itemize}
\item A contract extension will be
-stored in the \texttt{b\_extended}\sscodeidx{Cil\_types}{behavior}{b\_extended} field of
+stored in the \texttt{b\_extended}\scodeidx{Cil\_types}{behavior}{b\_extended} field of
\texttt{Cil\_types.behavior}\scodeidx{Cil\_types}{behavior}.
\item A global extension will be found as a global ACSL annotation in the form of a
-\scodeidx{Cil\_types}{Dextended}\texttt{Cil\_types.Dextended} constructor.
-\item A code annotation extension will be stored with an
-\scodeidx{Cil\_types}{AExtended}\texttt{Cil\_types.AExtended} constructor. Such an extension has itself
+\sscodeidx{Cil\_types}{global\_annotation}{Dextended}\texttt{Cil\_types.Dextended} constructor.
+\item A code annotation extension will be stored with the
+\sscodeidx{Cil\_types}{code\_annotation\_node}{AExtended}\texttt{Cil\_types.AExtended}
+constructor. Such an extension has itself
different flavors, determined by the \scodeidx{Cil\_types}{ext\_code\_annot\_context} type:
\begin{itemize}
\item it can be meant to be evaluated exactly at the current program point
@@ -4009,8 +4023,9 @@ Similarly, in a loop annotation, \verb|loop kw e1, ..., en;| will be treated as
\verb|kw| extension. In case the loop annotation has a \verb|loop variant|, the extension must
occur before. Otherwise, there is no ordering constraint with other loop annotations clauses.
-Global extensions can appear either alone in a global annotation, or as part of an axiomatic with
-a set of other global annotations.
+Global extensions can either be a standalone global annotation, or a whole block
+of global extensions, the latter case following the syntax of
+\texttt{axiomatic} blocks.
Finally, a code annotation extension must appear as a single code annotation, like any code annotation.
@@ -4048,6 +4063,8 @@ registered by one of the following functions, depending on its category.
\scodeidx{Acsl\_extension}{register\_behavior}
\item \texttt{Acsl\_extension.register\_global}%
\scodeidx{Acsl\_extension}{register\_global}
+\item \texttt{Acsl\_extension.register\_global\_block}%
+\scodeidx{Acsl\_extension}{register\_global\_block}
\item \texttt{Acsl\_extension.register\_code\_annot}%
\scodeidx{Acsl\_extension}{register\_code\_annot}
\item \texttt{Acsl\_extension.register\_code\_annot\_next\_stmt}%
@@ -4236,7 +4253,7 @@ for details about the provided operations on these types.
As join operators are provided for these types, they can be easily used in
abstract interpretation analyses\index{Abstract Interpretation} (which can
themselves be implemented thanks to one of functors of module
-\texttt{Dataflow2}\codeidx{Dataflow}.
+\texttt{Dataflow2}\codeidx{Dataflow2}.
\subsection{Map Indexed by Locations}\label{memory:map}
@@ -4383,55 +4400,6 @@ documentation with \texttt{make doc}, you must have generated the documentation
of Frama-C's kernel (\texttt{make doc}, see above) and installed it with the
\texttt{make install-doc-code}\codeidx{install-doc-code} command.
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%% \section{License Policy}\label{adv:copyright}\index{License|bfit}
-
-%% \begin{target}developers with a SVN access.\end{target}
-
-%% \begin{prereq}
-%% knowledge of \make.
-%% \end{prereq}
-
-%% If you want to redistribute a plug-in inside \framac, you have to define a
-%% proper license policy\index{Plug-in!License}. For this purpose, some help is
-%% provided in the \texttt{Makefile}\codeidx{Makefile}. Mainly we distinguish two
-%% cases described below.
-%% \begin{itemize}
-%% \item \textbf{If the wished license is already used inside \framac}, just
-%% extend the variable corresponding to the wished license in order to include
-%% files of your plug-in. Next run \texttt{make headers}\index{Header}.
-%% \begin{example}
-%% Plug-in \texttt{slicing}\index{Slicing}\index{Plug-in!Slicing|see{Slicing}}
-%% is released under LGPL\index{LGPL} and is proprietary of both CEA and
-%% INRIA\index{Copyright}. Thus, in the \texttt{Makefile}, there is the following line.
-%% \codeidx{CEA\_INRIA\_LGPL}
-%% \begin{makefilecode}
-%% CEA_INRIA_LGPL= ... €
-%% src/plugins/slicing/*.ml*
-%% \end{makefilecode}
-%% \end{example}
-%% \item \textbf{If the wished license is unknown inside \framac}, you have to:
-%% \begin{enumerate}
-%% \item Add a new variable $v$ corresponding to it and assign files of your
-%% plug-in;
-%% \item Extend variable \texttt{LICENSES}\codeidx{LICENSES} with
-%% this variable;
-%% \item Add a text file in directory \texttt{licenses}\codeidx{licenses}
-%% containing your licenses
-%% \item Add a text file in directory \texttt{headers}\codeidx{headers}
-%% containing the headers\index{Header} to add into files of your plug-in
-%% (those assigned by $v$).
-
-%% \begin{important}
-%% The filename must be the same than the variable name $v$. Moreover this
-%% file should contain a reference to the file containing the whole license
-%% text.
-%% \end{important}
-%% \item Run \texttt{make headers}.
-%% \end{enumerate}
-%% \end{itemize}
-
% Local Variables:
% ispell-local-dictionary: "english"
% TeX-master: "main"
diff --git a/doc/developer/check_api/.merlin b/doc/developer/check_api/.merlin
new file mode 100644
index 0000000000000000000000000000000000000000..5812a793959381fa1ba594fcd25cb54484910929
--- /dev/null
+++ b/doc/developer/check_api/.merlin
@@ -0,0 +1 @@
+PKG ocamldoc
diff --git a/doc/developer/check_api/Makefile b/doc/developer/check_api/Makefile
index e2219705a5916e3457881ef319d1a7be13d26059..6f6e94d6df445d3266a02ce6edbb4adea3b076ff 100644
--- a/doc/developer/check_api/Makefile
+++ b/doc/developer/check_api/Makefile
@@ -23,10 +23,10 @@ DEPENDENCIES= $(FRAMAC_MODERN) \
all: check_and_compare main.idx
./check_and_compare
-main.idx: ../developer.idx $(wildcard ../*.pretex)
+main.idx: ../developer.idx $(wildcard ../*.tex)
cp ../developer.idx main.idx
-check_and_compare: check_index_grammar.cmi check_index_grammar.cmx \
+check_and_compare: check_index_grammar.cmi check_index_lexer.cmi check_index_grammar.cmx \
check_index_lexer.cmx check_and_compare.cmx
$(OCAMLOPT) -o check_and_compare str.cmxa check_index_grammar.cmx \
check_index_lexer.cmx check_and_compare.cmx
diff --git a/doc/developer/check_api/check_and_compare.ml b/doc/developer/check_api/check_and_compare.ml
index e767939d391a8f5760b5239aa1627a82f05f6718..155c3001dc99172829058c1fd1637d6fcc38a596 100644
--- a/doc/developer/check_api/check_and_compare.ml
+++ b/doc/developer/check_api/check_and_compare.ml
@@ -11,20 +11,55 @@
(* *)
(**************************************************************************)
-let replace_space_by_dot s = Str.global_replace (Str.regexp " ") "." s
+let repair_word s = Str.global_replace (Str.regexp_string "\\") "" s
-let repair_word s =
- let rec repair_word_aux st =
- try let d1 = String.index st '$'
- in
- try let d2 = String.index_from st d1 '$'
- in (Str.string_before st d1)^
- (repair_word_aux (Str.string_after st (d2+1)))
- with Not_found -> st
- with Not_found -> st
+let index_entry = Str.regexp {|^\\indexentry{\(.*\)}{[0-9]*}|}
+
+let index_subentry = Str.regexp {|^.*@texttt *{\(fontsize {8}{10}selectfont \)?\([A-Za-z0-9_]+\)}$|}
+
+let all_caps = Str.regexp "^[A-Z0-9_]+$"
+
+let is_lower s = 'a' <= s.[0] && s.[0] <= 'z'
+let is_upper s = 'A' <= s.[0] && s.[0] <= 'Z'
+
+(* We have a prefix composed of module names, then maybe a lower case
+ symbol, possibly followed by a single symbol (in the case of a
+ type constructor or record field).
+*)
+let is_ocaml_symbol l =
+ let rec aux = function
+ | [] | [_] -> true
+ | [ t; _ ] when is_lower t -> true
+ | x :: l -> is_upper x && aux l
in
- Str.global_replace (Str.regexp "\\") "" (repair_word_aux s)
-
+ match l with
+ | [] -> false
+ | x :: l -> is_upper x && aux l
+
+let inspect_subentry l =
+ let check_one_entry e =
+ let e = repair_word e in
+ if Str.string_match index_subentry e 0 then begin
+ let word = Str.matched_group 2 e in
+ if Str.string_match all_caps word 0 then raise Exit else word
+ end else raise Exit
+ in
+ try
+ let l = List.map check_one_entry l in
+ if is_ocaml_symbol l then
+ (String.concat "." l) ^ "\n"
+ else ""
+ with Exit -> ""
+
+let inspect_entry line =
+ if Str.string_match index_entry line 0 then begin
+ let content = Str.matched_group 1 line in
+ match Str.split (Str.regexp_string "|") content with
+ | [ entry; _ ] -> inspect_subentry (Str.split (Str.regexp_string "!") entry)
+ | _ -> ""
+ end else ""
+
+let external_names = [ "Landmarks"; "Makefile" ]
(** [fill_tbl] takes a file containing data which is
as "element_name/type/comment/" or "element_name".
@@ -34,53 +69,23 @@ let repair_word s =
let fill_tbl tbl file_name =
try
let c = open_in file_name in
- try
- while true do
- let s = input_line c
- in
- if not (Str.string_match (Str.regexp "Command.Line") s 0)
- && not ( Hashtbl.mem tbl s)
- then match (Str.split (Str.regexp "/") s) with
- | [] -> ()
- | h::[] -> Hashtbl.add tbl h []
- | h::q -> Hashtbl.add tbl h q
+ let add_if_needed name infos =
+ if not (Hashtbl.mem tbl name || List.mem name external_names) then
+ Hashtbl.add tbl name infos
+ in
+ try
+ while true do
+ let s = input_line c in
+ match (Str.split (Str.regexp "/") s) with
+ | [] -> ()
+ | h::[] -> add_if_needed h []
+ | h::q -> add_if_needed h q
done
with End_of_file -> close_in c
with Sys_error _ as exn ->
Format.eprintf "cannot handle file %s: %s" file_name
(Printexc.to_string exn)
-(** [fill_list] takes a file containing data which is
- as "element_name/type/comment/" if (has_type=true) or
- "element_name" if (has_type=false). It fills the list [li]
- with all the element names and alphabetically sorts them. *)
-let fill_list li name ~has_type =
- let fill_list_no_sorting l file_name =
- try let c = open_in file_name in
- try
- while true do
- let s = input_line c in
- if not (Str.string_match
- (Str.regexp "Command.Line") s 0)&& not ( List.mem s !l)
- then begin
- if has_type then
- try let t =(Str.string_before s
- (String.index_from s 0 '/' )) in
- match t with
- |"" -> ()
- | _ -> if not( List.mem t !l)
- then l := t::!l
- with Not_found ->()
- else l := s::!l
- end
- done
- with End_of_file -> close_in c
- with Sys_error _ as exn ->
- Format.eprintf "cannot handle file %s: %s" file_name
- (Printexc.to_string exn) in
- fill_list_no_sorting li name ;
- li := List.sort String.compare !li
-
(** [run_oracle] takes two hashtables [t1] and [t2] when called.
It first tests if the file "run.oracle" is already existing.
If this file exists, it uses the function [w_tbl] and creates
@@ -117,14 +122,14 @@ let run_oracle t1 t2 =
then h ^ "\n" ^ (string_of_info_list q)
else (string_of_info_list q)
in
- let wo_tbl t k d =
+ let wo_tbl t k _d =
try let element_info = Hashtbl.find t k
in
to_fill :=
!to_fill ^ "\n" ^ k ^ "/" ^ (string_of_list element_info)
with Not_found -> ()
in
- let w_tbl t k d =
+ let w_tbl t k _d =
let tbl: (string,string list) Hashtbl.t = Hashtbl.create 197
in
fill_tbl tbl "run.oracle";
@@ -180,6 +185,9 @@ let compare t1 t2 name1 name2 =
name2 name1;
List.iter (compare_aux t1) t2
+let sort_keys tbl =
+ let l = Hashtbl.fold (fun k _ l -> k :: l) tbl [] in
+ List.sort String.compare l
(** here are used the lexer and parser "check_index_lexer" and
"check_index_grammar" to create the file "index_file".
@@ -187,27 +195,23 @@ let compare t1 t2 name1 name2 =
let () =
let index_hstbl: (string,string list) Hashtbl.t = Hashtbl.create 197 in
let code_hstbl: (string,string list) Hashtbl.t = Hashtbl.create 197 in
- let index_list = ref [] in
- let code_list = ref [] in
try
let chan_out = open_out ( "index_file") in
try
let chan_in = open_in ( "main.idx") in
- let lexbuf = Lexing.from_channel chan_in in
- let temp =
- repair_word (Check_index_grammar.main Check_index_lexer.token lexbuf)
- in
- let lexbuf_2 =Lexing.from_string temp in
- let result =
- Check_index_grammar.main Check_index_lexer.token_2 lexbuf_2
- in
- output_string chan_out (replace_space_by_dot result);
+ try
+ while true do
+ let line = input_line chan_in in
+ let res = inspect_entry line in
+ output_string chan_out res;
+ done
+ with End_of_file -> ();
close_out chan_out ; close_in chan_in;
fill_tbl code_hstbl "code_file";
fill_tbl index_hstbl "index_file";
- fill_list code_list "code_file" ~has_type:true;
- fill_list index_list "index_file" ~has_type:false;
- compare !index_list !code_list "THE INDEX \
+ let code_list = sort_keys code_hstbl in
+ let index_list = sort_keys index_hstbl in
+ compare index_list code_list "THE INDEX \
OF THE DEVELOPER GUIDE" "THE CODE";
run_oracle index_hstbl code_hstbl ;
with Sys_error _ as exn ->
diff --git a/doc/developer/check_api/check_code.ml b/doc/developer/check_api/check_code.ml
index 72539005fc293e584338f9333afe0a5eb4b47072..6f312d6779f257b9333206e744a5799d8595818c 100644
--- a/doc/developer/check_api/check_code.ml
+++ b/doc/developer/check_api/check_code.ml
@@ -11,8 +11,6 @@
(* *)
(**************************************************************************)
-(* do not work with OCaml 4 or higher *)
-
open Odoc_html
open Odoc_module
open Odoc_info
@@ -29,7 +27,7 @@ let print_in_file l =
in
let file_path = !doc_dev_path ^ "/code_file" in
try
- let chan_out = open_out file_path in
+ let chan_out = open_out_gen [Open_append; Open_creat] 0o644 file_path in
output_string chan_out (string_of_list l) ;
flush chan_out ;
close_out chan_out
@@ -225,26 +223,14 @@ module Generator (G : Odoc_html.Html_generator) = struct
super#html_of_exception b e
method private print_record b father l =
- last_type <- last_type ^ "{";
let print_one r =
- if last_type <> "" &&
- String.get last_type ((String.length last_type) -1) = '{'
- then begin
- if r.Type.rf_mutable then last_type <- last_type ^ "mutable "
- end else begin
- if r.Type.rf_mutable then last_type <- last_type ^ "; mutable "
- else last_type <- last_type ^ "; "
- end;
- last_type <- last_type ^ r.Type.rf_name ;
- self#html_of_type_expr_3 b father r.Type.rf_type;
+ last_name <- father ^ "." ^ r.Type.rf_name;
+ last_type <- father ^ " -> " ^ Odoc_info.string_of_type_expr r.Type.rf_type;
self#html_of_info b r.Type.rf_text
in
print_concat b "\n" print_one l;
- last_type <- last_type ^ "}"
method html_of_type b t =
- last_name <- t.Type.ty_name;
- last_type <- "";
Odoc_info.reset_type_names ();
let father = Name.father t.Type.ty_name in
self#html_of_type_expr_param_list_1 b father t;
@@ -252,7 +238,8 @@ module Generator (G : Odoc_html.Html_generator) = struct
| Type.Type_abstract -> ()
| Type.Type_variant l ->
let print_one constr =
- last_type <- last_type ^ " | " ^ constr.Type.vc_name ;
+ last_type <- "";
+ last_name <- t.Type.ty_name ^ "." ^ constr.Type.vc_name;
(match constr.Type.vc_args with
| Odoc_type.Cstr_tuple [] -> ()
| Odoc_type.Cstr_tuple l ->
@@ -265,6 +252,8 @@ module Generator (G : Odoc_html.Html_generator) = struct
print_concat b "\n" print_one l;
| Type.Type_record l -> self#print_record b father l
| _ -> ());
+ last_name <- t.Type.ty_name;
+ last_type <- "";
self#html_of_info b t.Type.ty_info;
method html_of_attribute b a =
diff --git a/doc/developer/check_api/check_index_lexer.mll b/doc/developer/check_api/check_index_lexer.mll
index 54b59cfa6be25912d6f34a3a804ed1b7606ad881..d2ebd852e2a67e4157a1ec4da29d5840dffe8959 100644
--- a/doc/developer/check_api/check_index_lexer.mll
+++ b/doc/developer/check_api/check_index_lexer.mll
@@ -13,6 +13,14 @@
{
}
+
+let alphanum = ['A'-'Z''a'-'z''0'-'9''_']
+let lower_name = ['a'-'z'] alphanum*
+(* in order to discriminate with other code keywords, we assume that an
+ OCaml module referenced in the LaTeX index is either a single letter
+ or has a lower case letter or an underscore as second character. *)
+let upper_name = ['A'-'Z'] ['a'-'z''_'] alphanum*
+
rule token = parse
| "\\texttt" { Check_index_grammar.KWD_WITH_ARG }
| "\\see" { Check_index_grammar.KWD_WITH_ARG }
@@ -35,6 +43,8 @@ rule token = parse
and token_2 = parse
| '\n'* ' '* [ 'a'-'z' '-' '.' ]+[ ^ '\n' ]* { token_2 lexbuf }
| '\n'* ' '* ([ 'A'-'Z' ][ 'a'-'z' '-' '_' '.' ]+ ' '* )+ ['A'-'Z'][^ 'a'-'z' '\n']+ { token_2 lexbuf }
- | '\n'* ' '* ([ 'A'-'Z' ][ 'a'-'z' ]+[ ^ '\n' ' ' ]* ' '* )+ ([ 'a'-'z' ]+[ ^ '\n' ' ' ]* ' '* )* as s { if not (String.contains s '.') then Check_index_grammar.STRING (Lexing.lexeme lexbuf) else token_2 lexbuf}
+ | '\n'* ' '* ((upper_name ' '*)+ lower_name ' '* (upper_name ' '*)?) {
+ Check_index_grammar.STRING (Lexing.lexeme lexbuf)
+ }
| '\n'* ' '* [ 'A'-'Z' '_' '-' ]+ [ ^ '\n' ]* { token_2 lexbuf }
| '\n'* eof { Check_index_grammar.EOF }
diff --git a/doc/developer/check_api/run.oracle b/doc/developer/check_api/run.oracle
index c5b9bea960a39741875927a46cfaee4c321bb3ec..ba68feb385aac8edab41a50849c4f352998e7268 100644
--- a/doc/developer/check_api/run.oracle
+++ b/doc/developer/check_api/run.oracle
@@ -1,157 +1,193 @@
Cil.cilVisitor.fill_global_tables/unit/fill the global environment tables at the end of a full copy in a new project./
-Project.load/?selection:State_selection.t -> ?name:string -> string -> t/Load a file into a new project given by its name. More precisely, load only except name file: 1. creates a new project;2. performs all the registered before_load actions;3. loads the (specified) states of the project according to its description; and4. performs all the registered after_load actions. raised exception: IOError./
+Project.load/?selection:State_selection.t -> ?name:string -> Filepath.Normalized.t -> t/Load a file into a new project given by its name. More precisely, load only except name file: 1. creates a new project;2. performs all the registered before_load actions;3. loads the (specified) states of the project according to its description; and4. performs all the registered after_load actions. raised exception: IOError./
Log.Messages.error/'a Log.pretty_printer/user error: syntax/typing error, bad expected input, etc./
-Log.with_log_channel/Log.channel -> (Log.event -> 'b) -> ?kind:Log.kind -> ?prefix:Log.prefix -> ('a, 'b) Log.pretty_aborter/logging function to user-created channel./
Cil.visitCilFile/Cil.cilVisitor -> Cil_types.file -> unit/Same thing, but the result is ignored. The given visitor must thus be an inplace visitor. Nothing is done if the visitor is a copy visitor./
-Type.t/parameters: 'a, constructors: /Type of type values. For each monomorphic type ty, a value of type ty t dynamically represents the type ty. Such a value is called a type value and should be unique for each static monomorphic type./
-Globals.Functions.get/Cil_types.varinfo -> Cil_types.kernel_function/Globals variables. raised exception: Not_found./
-Log.add_listener/?plugin:string -> ?kind:Log.kind list -> (Log.event -> unit) -> unit/Register a hook that is called each time an event is emitted. Applies to all channel unless specified, and all kind of messages unless specified./
+Type.t//Type of type values. For each monomorphic type ty, a value of type ty t dynamically represents the type ty. Such a value is called a type value and should be unique for each static monomorphic type./
+Dgraph_helper.graph_window/parent:GWindow.window -> title:string -> (packing:(GObj.widget -> unit) -> unit -> < adapt_zoom : unit -> unit; .. >) -> unit/Create a new window displaying a graph./
+Globals.Functions.get/Cil_types.varinfo -> Cil_types.kernel_function/Functions. The AST should be computed before using this module (cf. Ast.compute). raised exception: Not_found./
+Log.add_listener/?plugin:string -> ?kind:Log.kind list -> (Log.event -> unit) -> unit/Register a hook that is called each time an event is emitted. Applies to all channel unless specified, and all kind of messages unless specified. Warning: when executing the listener, all listeners will be temporarily deactivated in order to avoid infinite recursion./
State_builder.Register/string end ) -> State_builder.S with module Datatype = Datatype/Register(Datatype)(State)(Info) registers a new state. Datatype represents the datatype of a state, Local_state explains how to deal with the client-side state and Info are additional required information./
Parameter_sig.Builder.Zero/functor (X : Parameter_sig.Input_with_arg ) -> Parameter_sig.Int/What is the possible range of values for this parameter./
+Log.Messages.set_warn_status/Log.Messages.warn_category -> Log.warn_status -> unit/returns the warning category name as a string./
Datatype.Ref/functor (T : Datatype.S ) -> Datatype.S with type t = T.t ref/Deep copy: no possible sharing between x and copy x./
+Datatype.S_with_collections.Hashtbl/Datatype.Hashtbl with type key = t/Deep copy: no possible sharing between x and copy x./
+Cil.visitAction.DoChildren//Continue with the children of this node. Rebuild the node on return if any of the children changes (use == test)./
Cil/Cil_types.stmt -> Cil_types.stmt * Cil_types.stmtend /CIL main API. CIL original API documentation is available as an html version at http://manju.cs.berkeley.edu/cil./
-Cil_types.logic_ctor_info/{ctor_name: string; ctor_type: Cil_types.logic_type_info; ctor_params: Cil_types.logic_type list}/Description of a constructor of a logic sum-type./
+Cil_types.stmtkind.Goto/ of Cil_types.stmt Stdlib.ref * Cil_types.location/A goto statement. Appears from actual goto's in the code or from goto's that have been inserted during elaboration. The reference points to the statement that is the target of the Goto. This means that you have to update the reference whenever you replace the target statement. The target statement MUST have at least a label./
+Cil_types.logic_ctor_info//Description of a constructor of a logic sum-type./
Cil.cilVisitor.vlogic_var_use/Cil_types.logic_var -> Cil_types.logic_var Cil.visitAction//
Cmdline.nop/Cmdline.exit//
State_selection.t//Type of a state selection./
-Cil.register_behavior_extension/string -> (Cil.cilVisitor -> Cil_types.acsl_extension_kind -> Cil_types.acsl_extension_kind Cil.visitAction) -> unit/Indicates how an extended behavior clause is supposed to be visited. The default behavior is DoChildren, which ends up visiting each identified predicate in the list and leave the id as is./
+Boot/sig end /Main entry point of Frama-C. Nothing is exported./
+Cil_types.stmtkind.UnspecifiedSequence/ of (Cil_types.stmt * Cil_types.lval list * Cil_types.lval list * Cil_types.lval list * Cil_types.stmt Stdlib.ref list)list/statements whose order of execution is not specified by ISO/C. This is important for the order of side effects during evaluation of expressions. Each statement comes together with three list of lval, in this order.- lvals that are written during the sequence and whose future value depends upon the statement (it is legal to read from them, but not to write to them)- lvals that are written during the evaluation of the statement itself- lval that are read.- Function calls in the corresponding statement Note that this include only a subset of the affectations of the statement. Namely, the temporary variables generated by cil are excluded (i.e. it is assumed that the "compilation" is correct). In addition, side effects caused by function applications are not taken into account in the list. For a single statement, the written lvals are supposed to be ordered (or their order of evaluation doesn't matter), so that an alarm should be emitted only if the lvals read by a statement overlap with the lvals written (or read) by another statement of the sequence. At this time this feature is experimental and may miss some unspecified sequences. In case you do not care about this feature just handle it like a block (see Cil.block_from_unspecified_sequence)./
+Cil_types.stmtkind.Break/ of Cil_types.location/A break to the end of the nearest enclosing Loop or Switch./
Datatype.unit/unit Type.t/Add sets, maps and hashtables modules to an existing datatype, provided the equal, compare and hash functions are not Datatype.undefined./
-Globals/(Cil_types.stmt -> Cil_types.block) Pervasives.refend /Operations on globals./
-Db.Main/(unit -> unit) Pervasives.refend /Frama-C main interface./
+Globals/(Cil_types.stmt -> Cil_types.kernel_function) Stdlib.refend /Operations on globals./
+Db.Main/(unit -> unit) Stdlib.refend /Frama-C main interface./
+Visitor_behavior.Get/Visitor_behavior.Get/Get operations on behaviors, allows to get the representative of an AST element in the current state of the visitor. Get.ast_element vis e with e of type ast_element gets the representative of e in vis. For example for Cil_types.varinfo: Get.varinfo vis vi./
+Visitor_behavior.Set/Visitor_behavior.Set/Set operations on behaviors, allows to change the representative of a given AST element in the current state of the visitor. Use with care (i.e. makes sure that the old one is not referenced anywhere in the AST, or sharing will be lost). Set.ast_element vis e s with e and s of type ast_element changes the representative of e to s in vis. For example, for Cil_types.varinfo: Set.varinfo vis vi new_representative./
Db.Properties/Emitter.t -> Cil_types.kernel_function -> Cil_types.stmt -> string -> unitend /Dealing with logical properties./
-Cil_types.enuminfo/{eorig_name: string; mutable ename: string; mutable eitems: Cil_types.enumitem list; mutable eattr: Cil_types.attributes; mutable ereferenced: bool; mutable ekind: Cil_types.ikind}/Information about an enumeration./
+Visitor_behavior.Reset/Visitor_behavior.t -> unitend /Reset operations on behaviors, allows to reset the tables associated to a given kind of AST elements. If you use fresh instances of visitor for each round of transformation, you should not need this module. In place modifications do not need this at all. Reset.ast_element vis resets the tables associated to the considered type of AST elements in vis. For example for Cil_types.varinfo: Reset.varinfo vis./
+Cil_types.enuminfo//Information about an enumeration./
Datatype.Polymorphic/((Project_skeleton.t -> bool) -> 'a -> bool) -> (Project_skeleton.t -> bool) -> 'a Datatype.t -> bool end ) -> Datatype.Polymorphic with type 'a poly = 'a P.t/Functor for polymorphic types with only 1 type variable./
+Log.Messages.register_warn_category/string -> Log.Messages.warn_category/Returns currently active keys/
+Cil.visitAction.JustCopy//visit the children, but only to make the necessary copies (only useful for copy visitor)./
+Cil_datatype.Stmt/Stdlib.Format.formatter -> t -> unitend /Pretty print the sid of the statement/
Datatype.Polymorphic3/((Project_skeleton.t -> bool) -> 'a -> bool) -> ((Project_skeleton.t -> bool) -> 'b -> bool) -> ((Project_skeleton.t -> bool) -> 'c -> bool) -> (Project_skeleton.t -> bool) -> ('a, 'b, 'c) Datatype.t -> bool end ) -> Datatype.Polymorphic3 with type ('a, 'b, 'c) poly = ('a, 'b, 'c) P.t/Functor for polymorphic types with 3 type variables./
Datatype.string/string Type.t//
+Visitor_behavior.Set_orig/Visitor_behavior.Set/Set operations on behaviors related to original representatives, allows to change the reference of an element of the new AST in the current state of the visitor. Use with care. Set.ast_element vis e s with e and s of type ast_element changes the original representative of e to s in vis. For example, for Cil_types.varinfo: Set_orig.varinfo vis vi new_original_repr./
+Cmdline.stage.Extended//The stage where plug-ins are loaded. It is also the first stage each time the Frama-C main loop is run (e.g. after each "-then")./
+Pretty_source.localizable.PVDecl/ of (Cil_types.kernel_function option * Cil_types.kinstr * Cil_types.varinfo)/Declaration and definition of variables and function. Check the type of the varinfo to distinguish between the various possibilities. If the varinfo is a global or a local, the kernel_function is the one in which the variable is declared. The kinstr argument is given for local variables with an explicit initializer./
Locations.Location/Datatype.S with type t = location/Misc/
Parameter_sig.Builder.Int/int end ) -> Parameter_sig.Int/To be used by the plugin to output the results of the option in a controlled way. See set_output_dependencies details./
Db.Main.extend/(unit -> unit) -> unit/Register a function to be called by the Frama-C main entry point./
Annotations/State.tend /Annotations in the AST. The AST should be computed before calling functions of this module./
-Gtk_helper.graph_window/parent:GWindow.window -> title:string -> (packing:(GObj.widget -> unit) -> unit -> < adapt_zoom : unit -> unit; .. >) -> unit/Create a new window displaying a graph./
-Cmdline.run_after_exiting_stage/(unit -> Cmdline.exit) -> unit/Register an action to be executed at the end of the exiting stage. The guarded action must finish by exit n./
+Cmdline.run_after_exiting_stage/(unit -> Cmdline.exit) -> unit/Register an action to be executed at the end of the exiting stage. The guarded action must finish by exit n./
Cil.cilVisitor.vvrbl/Cil_types.varinfo -> Cil_types.varinfo Cil.visitAction/Invoked on each variable use. Here only the SkipChildren and ChangeTo actions make sense since there are no subtrees. Note that the type and attributes of the variable are not traversed for a variable use./
-Cil_types.varinfo/{mutable vname: string; vorig_name: string; mutable vtype: Cil_types.typ; mutable vattr: Cil_types.attributes; mutable vstorage: Cil_types.storage; mutable vglob: bool; mutable vdefined: bool; mutable vformal: bool; mutable vinline: bool; mutable vdecl: Cil_types.location; mutable vid: int; mutable vaddrof: bool; mutable vreferenced: bool; vtemp: bool; mutable vdescr: string option; mutable vdescrpure: bool; mutable vghost: bool; vsource: bool; mutable vlogic_var_assoc: Cil_types.logic_var option}/Information about a variable./
+Cil_types.varinfo//Information about a variable./
Lmap_bitwise/functor (V : Lmap_bitwise.With_default ) -> Lmap_bitwise.Location_map_bitwise with type v = V.tend /Functors making map indexed by zone./
-Cil.cilVisitor.behavior/Cil.visitor_behavior/the kind of behavior expected for the behavior./
+Cil.cilVisitor.behavior/Visitor_behavior.t/the kind of behavior expected for the behavior./
+Eva.Analysis.compute/unit -> unit/Computes the Eva analysis, if not already computed, using the entry point of the current project. You may set it with Globals.set_entry_point. raised exceptions: , if the entry point is incorrect, if some arguments are specified for the entry point using Db.Value.fun_set_args, and an incorrect number of them is given./
Datatype.Serializable_undefined/Datatype.Undefined/Same as Datatype.Undefined, but the type is supposed to be marshallable by the standard OCaml way (in particular, no hash-consing or projects inside the type)./
-Log.Messages.feedback/?ontty:Log.ontty -> ?level:int -> ?dkey:Log.category -> 'a Log.pretty_printer/Progress and feedback. Level is tested against the verbosity level./
-Log.set_echo/?plugin:string -> ?kind:Log.kind list -> bool -> unit/Turns echo on or off. Applies to all channel unless specified, and all kind of messages unless specified./
+Log.Messages.feedback/?ontty:Log.ontty -> ?level:int -> ?dkey:Log.Messages.category -> 'a Log.pretty_printer/Progress and feedback. Level is tested against the verbosity level./
+Log.set_echo/?plugin:string -> ?kind:Log.kind list -> bool -> unit/Turns echo on or off. Applies to all channel unless specified, and all kind of messages unless specified./
Db.Value.self/State.t/Internal state of the value analysis from projects viewpoint./
Log.new_channel/string -> Log.channel/Send an event over the associated listeners./
-Log.Messages.warning/'a Log.pretty_printer/Hypothesis and restrictions./
-Cil.get_stmt/Cil.visitor_behavior -> Cil_types.stmt -> Cil_types.stmt//
+Log.Messages.warning/?wkey:Log.Messages.warn_category -> 'a Log.pretty_printer/Hypothesis and restrictions./
Datatype.Undefined/Datatype.Undefined/Sub-signature of Datatype.S./
-Cil_types.fieldinfo/{mutable fcomp: Cil_types.compinfo; forig_name: string; mutable fname: string; mutable ftype: Cil_types.typ; mutable fbitfield: int option; mutable fattr: Cil_types.attributes; mutable floc: Cil_types.location; mutable faddrof: bool; mutable fsize_in_bits: int option; mutable foffset_in_bits: int option; mutable fpadding_in_bits: int option}/Information about a struct/union field./
-Cmdline.is_going_to_load/unit -> unit/To be call if one action is going to run after the loading stage. It is not necessary to call this function if the running action is set by an option put on the command line./
+Cil_types.fieldinfo//Information about a struct/union field./
+Cmdline.is_going_to_load/unit -> unit/To be call if one action is going to run after the loading stage. It is not necessary to call this function if the running action is set by an option put on the command line./
Datatype.func/?label:string * (unit -> 'a) option -> 'a Type.t -> 'b Type.t -> ('a -> 'b) Type.t//
+Cil_types.stmtkind.If/ of Cil_types.exp * Cil_types.block * Cil_types.block * Cil_types.location/A conditional. Two successors, the "then" and the "else" branches (in this order). Both branches fall-through to the successor of the If statement./
Datatype.Function/(string * (unit -> Datatype.t) option) option end ) -> functor (T2 : Datatype.S ) -> Datatype.S with type t = T1.t -> T2.t/Deep copy: no possible sharing between x and copy x./
-Project.clear/?selection:State_selection.t -> ?project:t -> unit -> unit/Clear the given project. Default project is current (). All the internal states of the given project are now empty (wrt the action registered with register_todo_on_clear)./
-Kernel.CodeOutput/(Format.formatter -> unit) -> unitend /Behavior of option "-ocode"./
+Project.clear/?selection:State_selection.t -> ?project:t -> unit -> unit/Clear the given project. Default project is current (). All the internal states of the given project are now empty (wrt the action registered with register_todo_on_clear)./
+Kernel.CodeOutput/(Stdlib.Format.formatter -> unit) -> unitend /Behavior of option "-ocode"./
+Datatype.S_with_collections.Set/Datatype.Set with type elt = t/Datatype with alternative ordering, where properties are ordered according the following criteria: 1. Kf name (global properties ranked first) 2. Kinstr 3. kind of property 4. id of the property/
Datatype.int/int Type.t//
+Cil.visitAction.ChangeTo/ of 'a/Replace the expression with the given one./
Log.Messages.fatal/('a, 'b) Log.pretty_aborter/internal error of the plug-in. raised exception: AbortFatal./
+Dataflow2/Cil_types.fundec -> Cil_types.stmt list * Cil_types.stmt listend /Implementation of data flow analyses over user-supplied domains./
Cil.cilVisitor.vexpr/Cil_types.exp -> Cil_types.exp Cil.visitAction/Invoked on each expression occurrence. The subtrees are the subexpressions, the types (for a Cast or SizeOf expression) or the variable use./
Parameter_customize/(string -> Cil_datatype.Kf.Set.t) -> unitend /Configuration of command line options. You can apply the functions below just before applying one of the functors provided by the functor Plugin.Register and generating a new parameter./
Cmdline.run_during_extending_stage/(unit -> unit) -> unit/Register an action to be executed during the extending stage./
-File.init_project_from_cil_file/Project.t -> Cil_types.file -> unit/Initialize the cil file representation with the given file for the given project from the current one. Should be called at most once per project. raised exception: File_types.Bad_Initialization./
-Datatype.func2/?label1:string * (unit -> 'a) option -> 'a Type.t -> ?label2:string * (unit -> 'b) option -> 'b Type.t -> 'c Type.t -> ('a -> 'b -> 'c) Type.t/optlabel_func lab dft ty1 ty2 is equivalent to func ~label:(lab, Some dft) ty1 ty2/
-Cil.visitAction/parameters: 'a, constructors: | SkipChildren/Do not visit the children. Return the node as it is./
-Log.Messages/Log.Messages/Returns currently active keys/
-Extlib.the/?exn:exn -> 'a option -> 'a/opt_bind f x returns None if x is None and f y if is Some y (monadic bind) raised exceptions: , if the value is None and exn is specified., if the value is None and exn is not specified./
+File.init_project_from_cil_file/Project.t -> Cil_types.file -> unit/Initialize the cil file representation with the given file for the given project from the current one. Should be called at most once per project. raised exception: File_types.Bad_Initialization./
+Datatype.func2/?label1:string * (unit -> 'a) option -> 'a Type.t -> ?label2:string * (unit -> 'b) option -> 'b Type.t -> 'c Type.t -> ('a -> 'b -> 'c) Type.t/optlabel_func lab dft ty1 ty2 is equivalent to func ~label:(lab, Some dft) ty1 ty2/
+Cil.visitAction//Different visiting actions. 'a will be instantiated with exp, instr, etc./
+Log.Messages/Log.Messages//
+Cil_types.code_annotation_node.AExtended/ of string list * bool * Cil_types.acsl_extension/extension in a code or loop annotation. Boolean flag is true for loop extensions and false for code extensions/
Parameter_sig.Builder.String_set/functor (X : Parameter_sig.Input_with_arg ) -> Parameter_sig.String_set/Is there some element satisfying the given predicate?/
-Cil.inplace_visit/unit -> Cil.visitor_behavior/In-place modification. Behavior of the original cil visitor./
Cmdline.Exit///
Cil_state_builder.Stmt_hashtbl/functor (Data : Datatype.S ) -> functor (Info : State_builder.Info_with_size ) -> State_builder.Hashtbl with type key = Cil_types.stmt and type data = Data.t/Return the list of all data associated with the given key./
-State_builder.Hashtbl/functor (H : Datatype.Hashtbl ) -> functor (Data : Datatype.S ) -> functor (Info : State_builder.Info_with_size ) -> State_builder.Hashtbl with type key = H.key and type data = Data.t and module Datatype = H.Make(Data)/remove x removes from the table one instance of x. Does nothing if there is no instance of x./
+State_builder.Hashtbl/functor (H : Datatype.Hashtbl ) -> functor (Data : Datatype.S ) -> functor (Info : State_builder.Info_with_size ) -> State_builder.Hashtbl with type key = H.key and type data = Data.t and module Datatype = H.Make(Data)/remove x removes from the table one instance of x. Does nothing if there is no instance of x./
Parameter_sig.Builder.True/functor (X : Parameter_sig.Input ) -> Parameter_sig.Bool/Set the boolean to false./
Parameter_sig.Builder/Parameter_sig.Builder/Signatures containing the different functors which may be used to generate new command line options./
+Acsl_extension.register_global_block/string -> ?preprocessor:Acsl_extension.extension_preprocessor_block -> Acsl_extension.extension_typer_block -> ?visitor:Acsl_extension.extension_visitor -> ?printer:Acsl_extension.extension_printer -> ?short_printer:Acsl_extension.extension_printer -> bool -> unit/Registers extension for global block annotation. See register_behavior./
+Typed_parameter/t -> stringend /Parameter settable through a command line option. This is a low level API, internally used by the kernel. As a plug-in developer, you certainly prefer to use the API of Plugin instead./
Log.Messages.abort/('a, 'b) Log.pretty_aborter/user error stopping the plugin. raised exception: AbortError./
Kernel_function/State.tend /Operations to get info from a kernel function. This module does not give access to information about the set of all the registered kernel functions (like iterators over kernel functions). This kind of operations is stored in module Globals.Functions./
Datatype.String/Datatype.S_with_collections with type t = string/Deep copy: no possible sharing between x and copy x./
File.init_from_cmdline/unit -> unit/Initialize the cil file representation with the file given on the command line. Should be called at most once per project. raised exception: File_types.Bad_Initialization./
-File.init_from_c_files/t list -> unit/Initialize the cil file representation of the current project. Should be called at most once per project. raised exception: File_types.Bad_Initialization./
-Cil_types.mach/{sizeof_short: int; sizeof_int: int; sizeof_long: int; sizeof_longlong: int; sizeof_ptr: int; sizeof_float: int; sizeof_double: int; sizeof_longdouble: int; sizeof_void: int; sizeof_fun: int; size_t: string; wchar_t: string; ptrdiff_t: string; alignof_short: int; alignof_int: int; alignof_long: int; alignof_longlong: int; alignof_ptr: int; alignof_float: int; alignof_double: int; alignof_longdouble: int; alignof_str: int; alignof_fun: int; char_is_unsigned: bool; underscore_name: bool; const_string_literals: bool; little_endian: bool; alignof_aligned: int; has__builtin_va_list: bool; __thread_is_keyword: bool; compiler: string; cpp_arch_flags: string list; version: string}/Definition of a machine model (architecture + compiler)./
-Ast.mark_as_grown/unit -> unit/call this function whenever you have added something to the AST, without modifying the existing nodes/
-Globals.set_entry_point/string -> bool -> unit/set_entry_point name lib sets Kernel.MainFunction to name and Kernel.LibEntry to lib. Moreover, clear the results of all the analysis which depend on Kernel.MainFunction or Kernel.LibEntry./
+File.init_from_c_files/t list -> unit/Initialize the cil file representation of the current project. Should be called at most once per project. raised exception: File_types.Bad_Initialization./
+Cil_types.mach//Definition of a machine model (architecture + compiler)./
+Ast.mark_as_grown/unit -> unit/call this function whenever you have added something to the AST, without modifying the existing nodes/
+Globals.set_entry_point/string -> bool -> unit/set_entry_point name lib sets Kernel.MainFunction to name and Kernel.LibEntry to lib. Moreover, clear the results of all the analysis which depend on Kernel.MainFunction or Kernel.LibEntry./
+State_selection.only_dependencies/State.t -> State_selection.t/The selection containing all the dependencies of the given state (but not this state itself)./
Cmdline/Cmdline.Group.t -> stringend end /Command line parsing./
+Datatype.Ty.t//A type with its type value./
Design.main_window_extension_points.register_source_selector/(GMenu.menu GMenu.factory -> Design.main_window_extension_points -> button:int -> Pretty_source.localizable -> unit) -> unit/register an action to perform when button is released on a given localizable. If the button 3 is released, the first argument is popped as a contextual menu./
Frontc.add_syntactic_transformation/(Cabs.file -> Cabs.file) -> unit/add a syntactic transformation that will be applied to all freshly parsed C files./
Project/unit -> unitend end /Projects management. A project groups together all the internal states of Frama-C. An internal state is roughly the result of a computation which depends of an AST. It is possible to have many projects at the same time. For registering a new state in the Frama-C projects, apply the functor State_builder.Register./
Visitor.frama_c_visitor.current_kf/Cil_types.kernel_function option/link to the kernel function currently being visited. NB: for copy visitors, the link is to the original kf (anyway, the new kf is created only after the visit is over)./
Datatype.undefined/'a -> 'b/Must be used if you don't want to implement a required function./
+Cil_types.stmtkind.TryExcept/ of Cil_types.block * (Cil_types.instr list * Cil_types.exp) * Cil_types.block * Cil_types.location/On MSVC we support structured exception handling. The try/except statement is a bit tricky: __try { blk } __except (e) { handler } The argument to __except must be an expression. However, we keep a list of instructions AND an expression in case you need to make function calls. We'll print those as a comma expression. The control can get to the __except expression only if an exception is thrown. After that, depending on the value of the expression the control goes to the handler, propagates the exception, or retries the exception. The location corresponds to the try keyword./
Log.Messages.failure/'a Log.pretty_printer/internal error of the plug-in./
Logic_const.prel/?loc:Cil_types.location -> Cil_types.relation * Cil_types.term * Cil_types.term -> Cil_types.predicate/Binary relation./
+Cil.visitAction.ChangeDoChildrenPost/ of 'a * ('a -> 'a)/First consider that the entire exp is replaced by the first parameter. Then continue with the children. On return rebuild the node if any of the children has changed and then apply the function on the node./
Locations.Zone/Locations.Zone.map_t -> Int_Intervals.t Hptmap.Shape(Base.Base).tend /Association between bases and ranges of bits./
-Cil.cilVisitor.get_filling_actions/(unit -> unit) Queue.t/get the queue of actions to be performed at the end of a full copy./
-Locations.location/{loc: Locations.Location_Bits.t; size: Int_Base.t}/A Location_Bits.t and a size in bits./
+Cil.cilVisitor.get_filling_actions/(unit -> unit) Stdlib.Queue.t/get the queue of actions to be performed at the end of a full copy./
+Locations.location//A Location_Bits.t and a size in bits./
Cil_types/end /The Abstract Syntax of CIL./
Visitor.frama_c_visitor.vstmt_aux/Cil_types.stmt -> Cil_types.stmt Cil.visitAction/Replacement of vstmt./
-File.init_project_from_visitor/?reorder:bool -> Project.t -> Visitor.frama_c_visitor -> unit/init_project_from_visitor prj vis initialize the cil file representation of prj. prj must be essentially empty: it can have some options set, but not an existing cil file; proj is filled using vis, which must be a copy visitor that puts its results in prj. if reorder is true (default is false) the new AST in prj will be reordered./
+File.init_project_from_visitor/?reorder:bool -> Project.t -> Visitor.frama_c_visitor -> unit/init_project_from_visitor prj vis initialize the cil file representation of prj. prj must be essentially empty: it can have some options set, but not an existing cil file; proj is filled using vis, which must be a copy visitor that puts its results in prj. if reorder is true (default is false) the new AST in prj will be reordered./
Datatype.Polymorphic4/((Project_skeleton.t -> bool) -> 'a -> bool) -> ((Project_skeleton.t -> bool) -> 'b -> bool) -> ((Project_skeleton.t -> bool) -> 'c -> bool) -> ((Project_skeleton.t -> bool) -> 'd -> bool) -> (Project_skeleton.t -> bool) -> ('a, 'b, 'c, 'd) Datatype.t -> bool end ) -> Datatype.Polymorphic4 with type ('a, 'b, 'c, 'd) poly = ('a, 'b, 'c, 'd) P.t/Functor for polymorphic types with 4 type variables./
Datatype.List/functor (T : Datatype.S ) -> Datatype.S with type t = T.t list/Deep copy: no possible sharing between x and copy x./
Structural_descr.pack/Structural_descr.t -> Structural_descr.pack/Pack a structural descriptor in order to embed it inside another one./
Log.set_output/?isatty:bool -> (string -> int -> int -> unit) -> (unit -> unit) -> unit/This function has the same parameters as Format.make_formatter./
-Cil.reset_behavior_varinfo/Cil.visitor_behavior -> unit/resets the internal tables used by the given visitor_behavior. If you use fresh instances of visitor for each round of transformation, this should not be needed. In place modifications do not need that at all./
-Logic_utils.expr_to_term/cast:bool -> Cil_types.exp -> Cil_types.term/translates a C expression into an "equivalent" logical term. cast specifies how C arithmetic operators are translated. When cast is true, the translation returns a logic term having the same semantics of the C expr by introducing casts (i.e. the C expr a+b can be translated as (char)(((char)a)+(char)b) to preserve the modulo feature of the C addition). Otherwise, no such casts are introduced and the C arithmetic operators are translated into perfect mathematical operators (i.e. a floating point addition is translated into an addition of real numbers)./
-Journal/(string -> string) Pervasives.refend /Journalization of functions./
+Log.Messages.logwith/(Log.event option -> 'b) -> ?wkey:Log.Messages.warn_category -> ?emitwith:(Log.event -> unit) -> ?once:bool -> ('a, 'b) Log.pretty_aborter/Recommanded generic log routine using warn_category instead of kind. logwith continuation ?wkey fmt similar to warning ?wkey fmt and then calling the continuation. The optional continuation argument refers to the corresponding event. None is used iff no message is logged. In case the wkey is considered as a Failure, the continution is not called. This kind of message denotes a fatal error aborting Frama-C. Notice that the ~emitwith action is called iff a message is logged./
+Logic_utils.expr_to_term/?coerce:bool -> Cil_types.exp -> Cil_types.term/Returns a logic term that has exactly the same semantics as the original C-expression. The type of the resulting term is determined by the ~coerce flag as follows:- when ~coerce:false is given (the default) the term has the same c-type as the original expression.- when ~coerce:true is given, if the original expression has an int or float type, then the returned term is coerced into the integer or real logic type, respectively. Remark: when the original expression is a comparison, it is evaluated as an int or an integer depending on the ~coerce flag. To obtain a boolean or predicate, use expr_to_boolean or expr_to_predicate instead./
+Journal/(string -> Datatype.Filepath.t) Stdlib.refend /Journalization of functions./
Cil.cilVisitor.vstmt/Cil_types.stmt -> Cil_types.stmt Cil.visitAction/Control-flow statement. The default DoChildren action does not create a new statement when the components change. Instead it updates the contents of the original statement. This is done to preserve the sharing with Goto and Case statements that point to the original statement. If you use the ChangeTo action then you should take care of preserving that sharing yourself./
-Cil.get_varinfo/Cil.visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo/retrieve the representative of a given varinfo in the current state of the visitor/
-Eva.Analysis.is_computed/unit -> bool/Return true iff the value analysis has been done./
+Db.Value.is_computed/unit -> bool/Return true iff the value analysis has been done./
Kernel.Unicode/('a -> 'b) -> 'a -> 'bend /Behavior of option "-unicode"./
Design.register_extension/(Design.main_window_extension_points -> unit) -> unit/Register an extension to the main GUI. It will be invoked at initialization time./
-Cil_types.global/ | GType of Cil_types.typeinfo * Cil_types.location | GCompTag of Cil_types.compinfo * Cil_types.location | GCompTagDecl of Cil_types.compinfo * Cil_types.location | GEnumTag of Cil_types.enuminfo * Cil_types.location | GEnumTagDecl of Cil_types.enuminfo * Cil_types.location | GVarDecl of Cil_types.varinfo * Cil_types.location | GFunDecl of Cil_types.funspec * Cil_types.varinfo * Cil_types.location | GVar of Cil_types.varinfo * Cil_types.initinfo * Cil_types.location | GFun of Cil_types.fundec * Cil_types.location | GAsm of string * Cil_types.location | GPragma of Cil_types.attribute * Cil_types.location | GText of string | GAnnot of Cil_types.global_annotation * Cil_types.location/The main type for representing global declarations and definitions. A list of these form a CIL file. The order of globals in the file is generally important./
+Cil_types.global//The main type for representing global declarations and definitions. A list of these form a CIL file. The order of globals in the file is generally important./
Cil.dummyStmt/Cil_types.stmt/A statement consisting of just dummyInstr./
Datatype.func3/?label1:string * (unit -> 'a) option -> 'a Type.t -> ?label2:string * (unit -> 'b) option -> 'b Type.t -> ?label3:string * (unit -> 'c) option -> 'c Type.t -> 'd Type.t -> ('a -> 'b -> 'c -> 'd) Type.t//
-Cil.cilVisitor//A visitor interface for traversing CIL trees. Create instantiations of this type by specializing the class Cil.nopCilVisitor. Each of the specialized visiting functions can also call the queueInstr to specify that some instructions should be inserted before the current instruction or statement. Use syntax like self#queueInstr to call a method associated with the current object. Important Note for Frama-C Users: Unless you really know what you are doing, you should probably inherit from the Visitor.generic_frama_c_visitor instead of Cil.genericCilVisitor or Cil.nopCilVisitor/
+Cmdline.stage.Loading//After Extended, the stage where a previous Frama-C internal states is restored (e.g. the one specified by -load or by running the journal)./
+Cil.cilVisitor//A visitor interface for traversing CIL trees. Create instantiations of this type by specializing the class Cil.nopCilVisitor. Each of the specialized visiting functions can also call the queueInstr to specify that some instructions should be inserted before the current statement. Use syntax like self#queueInstr to call a method associated with the current object. Important Note for Frama-C Users: Unless you really know what you are doing, you should probably inherit from the Visitor.generic_frama_c_visitor instead of Cil.genericCilVisitor or Cil.nopCilVisitor/
Cil.lzero/?loc:Cil_types.location -> unit -> Cil_types.term/The constant logic term zero./
Db.Value.is_reachable/Db.Value.state -> bool/add_formals_to_state state kf exps evaluates exps in state and binds them to the formal arguments of kf in the resulting state/
-Cil_types.compinfo/{mutable cstruct: bool; corig_name: string; mutable cname: string; mutable ckey: int; mutable cfields: Cil_types.fieldinfo list; mutable cattr: Cil_types.attributes; mutable cdefined: bool; mutable creferenced: bool}/The definition of a structure or union type. Use Cil.mkCompInfo to make one and use Cil.copyCompInfo to copy one (this ensures that a new key is assigned and that the fields have the right pointers to parents.)./
-Cil_types.logic_type_info/{lt_name: string; lt_params: string list; mutable lt_def: Cil_types.logic_type_def option; mutable lt_attr: Cil_types.attributes}/Description of a logic type./
+Cil_types.compinfo//The definition of a structure or union type. Use Cil.mkCompInfo to make one and use Cil.copyCompInfo to copy one (this ensures that a new key is assigned and that the fields have the right pointers to parents.)./
+Cil_types.logic_type_info//Description of a logic type./
Cmdline.run_after_loading_stage/(unit -> unit) -> unit/Register an action to be executed at the end of the loading stage./
Locations/Base.t -> Cil_types.typ -> Cil_types.offset -> Locations.locationend /Memory locations./
-File.must_recompute_cfg/Cil_types.fundec -> unit/must_recompute_cfg f must be called by code transformation hooks when they modify statements in function f. This will trigger a recomputation of the cfg of f after the transformation./
+Logic_const.new_acsl_extension/string -> Cil_types.location -> bool -> Cil_types.acsl_extension_kind -> Cil_types.acsl_extension/creates a new acsl_extension with a fresh id./
+Acsl_extension.register_code_annot_next_stmt/string -> ?preprocessor:Acsl_extension.extension_preprocessor -> Acsl_extension.extension_typer -> ?visitor:Acsl_extension.extension_visitor -> ?printer:Acsl_extension.extension_printer -> ?short_printer:Acsl_extension.extension_printer -> bool -> unit/Registers extension for code annotation to be evaluated for the _next_ statement. See register_behavior./
+File.must_recompute_cfg/Cil_types.fundec -> unit/must_recompute_cfg f must be called by code transformation hooks when they modify statements in function f. This will trigger a recomputation of the cfg of f after the transformation./
Parameter_sig.Builder.Kernel_function_set/functor (X : Parameter_sig.Input_with_arg ) -> Parameter_sig.Kernel_function_set/Is there some element satisfying the given predicate?/
Ast.add_monotonic_state/State.t -> unit/indicates that the given state (which must depend on Ast.self) is robust against additions to the AST, that is, it will be able to compute information on the new nodes whenever needed. Ast.mark_as_grown will not erase such states, while Ast.mark_as_changed and clearing Ast.self itself will./
Visitor.visitFramacFunction/Visitor.frama_c_visitor -> Cil_types.fundec -> Cil_types.fundec/Visit a function definition./
-File.create_project_from_visitor/?reorder:bool -> ?last:bool -> string -> (Project.t -> Visitor.frama_c_visitor) -> Project.t/Return a new project with a new cil file representation by visiting the file of the current project. If reorder is true, the globals in the AST of the new project are reordered (default is false). If last is true (by default), remember than the returned project is the last created one. The visitor is responsible to avoid sharing between old file and new file (i.e. it should use Cil.copy_visit at some point). raised exception: File_types.Bad_Initialization./
+File.create_project_from_visitor/?reorder:bool -> ?last:bool -> string -> (Project.t -> Visitor.frama_c_visitor) -> Project.t/Return a new project with a new cil file representation by visiting the file of the current project. If reorder is true, the globals in the AST of the new project are reordered (default is false). If last is true (by default), remember than the returned project is the last created one. The visitor is responsible to avoid sharing between old file and new file (i.e. it should use Cil.copy_visit at some point). raised exception: File_types.Bad_Initialization./
+Cil_types.binop.Div////
Parameter_sig.Bool/Parameter_sig.Bool/Signature for a boolean parameter./
-Visitor.generic_frama_c_visitor/Cil.visitor_behavior -> /Generic class that abstracts over frama_c_inplace and frama_c_copy./
-Db.Value.get_stmt_state/Cil_types.stmt -> Db.Value.state/Initial state used by the analysis/
-Logic_typing.typing_context/{is_loop: unit -> bool; anonCompFieldName: string; conditionalConversion: Cil_types.typ -> Cil_types.typ -> Cil_types.typ; find_macro: string -> Logic_ptree.lexpr; find_var: string -> Cil_types.logic_var; find_enum_tag: string -> Cil_types.exp * Cil_types.typ; find_comp_field: Cil_types.compinfo -> string -> Cil_types.offset; find_type: Logic_typing.type_namespace -> string -> Cil_types.typ; find_label: string -> Cil_types.stmt Pervasives.ref; remove_logic_function: string -> unit; remove_logic_type: string -> unit; remove_logic_ctor: string -> unit; add_logic_function: Cil_types.logic_info -> unit; add_logic_type: string -> Cil_types.logic_type_info -> unit; add_logic_ctor: string -> Cil_types.logic_ctor_info -> unit; find_all_logic_functions: string -> Cil_types.logic_info list; find_logic_type: string -> Cil_types.logic_type_info; find_logic_ctor: string -> Cil_types.logic_ctor_info; pre_state: Logic_typing.Lenv.t; post_state: Cil_types.termination_kind list -> Logic_typing.Lenv.t; assigns_env: Logic_typing.Lenv.t; silent: bool; type_predicate: Logic_typing.typing_context -> Logic_typing.Lenv.t -> Logic_ptree.lexpr -> Cil_types.predicate/typechecks a predicate. Note that the first argument is itself a typing_context, which allows for open recursion. Namely, it is possible for the extension to change the type-checking functions for the sub-nodes of the parsed tree, and not only for the toplevel lexpr./
+Cil_types.stmtkind.Instr/ of Cil_types.instr/An instruction that does not contain control flow. Control implicitly falls through./
+Visitor.generic_frama_c_visitor/Visitor_behavior.t -> /Generic class that abstracts over frama_c_inplace and frama_c_copy./
+Db.Value.get_stmt_state/?after:bool -> Cil_types.stmt -> Db.Value.state/after is false by default./
+Logic_typing.typing_context//Functions that can be called when type-checking an extension of ACSL./
Parameter_sig.Builder.False/functor (X : Parameter_sig.Input ) -> Parameter_sig.Bool/Set the boolean to false./
Cil.cilVisitor.vglob/Cil_types.global -> Cil_types.global list Cil.visitAction/Global (vars, types, etc.)/
+Cil_types.ext_category//Where are we expected to find corresponding extension keyword./
Parameter_sig.Builder.String/string end ) -> Parameter_sig.String/What is the possible range of values for this parameter./
State/t -> unitend /A state is a project-compliant mutable value./
Type.name/'a Type.t -> string/Apply this functor to access to the abstract type of the given name./
-Log.Messages.debug/?level:int -> ?dkey:Log.category -> 'a Log.pretty_printer/Debugging information dedicated to Plugin developers. Default level is 1. The debugging key is used in message headers. See also set_debug_keys and set_debug_keyset./
+Log.Messages.debug/?level:int -> ?dkey:Log.Messages.category -> 'a Log.pretty_printer/Debugging information dedicated to Plugin developers. Default level is 1. The debugging key is used in message headers. See also set_debug_keys and set_debug_keyset./
Cil_state_builder/functor (Data : Datatype.S ) -> functor (Info : State_builder.Info_with_size ) -> State_builder.Hashtbl with type key = Cil_types.kernel_function and type data = Data.tend /Functors for building computations which use kernel datatypes./
-Cil_printer.register_behavior_extension/string -> (Printer_api.extensible_printer_type -> Format.formatter -> Cil_types.acsl_extension_kind -> unit) -> unit/Register a pretty-printer used for behavior extension./
+Log.Messages.warn_category//Same as above, but for warnings/
Structural_descr.p_int/Structural_descr.pack/Equivalent to pack Abstract/
-Lmap/V.t Lmap.default_contents end ) -> module type of Lmap_sig with type v = V.t and type widen_hint_base = V.generic_widen_hint and type offsetmap = Offsetmap.tend /Maps from bases to memory maps. The memory maps are those of the Offsetmap module./
-Dynamic/string list -> unitend /Value accesses through dynamic typing./
-Kernel_function.dummy/unit -> t/callsites f collect the statements where f is called. Same complexity as find_from_sid./
-Design/GSourceView2.source_buffer -> offset:int -> Property_status.Feedback.t -> unitend end /The extensible GUI./
+Lmap/V.t Lmap.default_contents end ) -> module type of Lmap_sig with type v = V.t and type widen_hint_base = V.numerical_widen_hint and type offsetmap = Offsetmap.tend /Maps from bases to memory maps. The memory maps are those of the Offsetmap module./
+Dynamic/string -> boolend /Value accesses through dynamic typing./
+Kernel_function.dummy/unit -> t/is_between b s1 s2 s3 returns true if the statement s2 appears strictly between s1 and s3 inside the b.bstmts list. All three statements must actually occur in b.bstmts, either directly or indirectly (see Kernel_function.find_enclosing_stmt_in_block). raised exception: AbortFatal./
+Design/GSourceView.source_buffer -> ?call_site:Cil_types.stmt -> offset:int -> Property_status.Feedback.t -> unitend end /The extensible GUI./
+Structural_descr.structure.Sum/ of Structural_descr.pack array array/Sum c describes a non-array type where c is an array describing the non-constant constructors of the type being described (in the order of their declarations in that type). Each element of this latter array is an array of t that describes (in order) the fields of the corresponding constructor./
+Visitor_behavior.inplace/unit -> Visitor_behavior.t/In-place modification. Behavior of the original cil visitor./
Datatype.list/'a Type.t -> 'a list Type.t/Functor for polymorphic types with 4 type variables./
Cil.cilVisitor.vlogic_var_decl/Cil_types.logic_var -> Cil_types.logic_var Cil.visitAction//
-Cil_types.typeinfo/{torig_name: string; mutable tname: string; mutable ttype: Cil_types.typ; mutable treferenced: bool}/Information about a defined type./
+Cil_types.typeinfo//Information about a defined type./
Ast.self/State.t/The state kind associated to the cil AST./
Type.AlreadyExists/string/May be raised by Type.register./
Property_status/Property.t -> boolend /Status of properties./
Datatype.never_any_project/(Project_skeleton.t -> bool) -> 'a -> bool/Must be used for mem_project if values of your type does never contain any project./
-Property/string -> stringend end /ACSL comparable property./
-Cil_datatype/unit -> unitend /Datatypes of some useful CIL types./
+Property/?truncate:int -> Property.identified_property -> stringend end /ACSL comparable property./
+Cil_datatype/S with type t = Logic_ptree.lexprend /Datatypes of some useful CIL types./
+Cmdline.stage.Early//Initial stage for very specific almost hard-coded options. Do not use it./
+Acsl_extension.register_behavior/string -> ?preprocessor:Acsl_extension.extension_preprocessor -> Acsl_extension.extension_typer -> ?visitor:Acsl_extension.extension_visitor -> ?printer:Acsl_extension.extension_printer -> ?short_printer:Acsl_extension.extension_printer -> bool -> unit/register_behavior name ~preprocessor typer ~visitor ~printer ~short_printer status registers new ACSL extension to be used in function contracts with name name. The optional preprocessor is a function to be applied by the parser on the untyped content of the extension before parsing the rest of the processed file. By default, this function is the identity. The typer is applied when transforming the untyped AST to Cil. It recieves the typing context of the annotation that can be used to type the received logic expressions (see Logic_typing.typing_context), and the location of the annotation. The optional visitor allows changing the way the ACSL extension is visited. By default, the behavior is Cil.DoChildren, which ends up visiting each identified predicate/term in the list and leave the id as is. The optional printer allows changing the way the ACSL extension is pretty printed. By default, it prints the name of the extension followed by the formatted predicates, terms or identifier according to the Cil_types.acsl_extension_kind. The optional short_printer allows changing the Printer.pp_short_extended behavior for the ACSL extension. By default, it just prints the name. It is for example used for the filetree in the GUI. The status indicates whether the extension can be assigned a property status or not. Here is a basic example: let count = ref 0 let foo_typer typing_context loc = function | p :: [] -> Ext_preds [ (typing_context.type_predicate typing_context (typing_context.post_state [Normal]) p)]) | [] -> let id = !count in incr count; Ext_id id | _ -> typing_context.error loc "expecting a predicate after keyword FOO" let () = Acsl_extension.register_behavior "FOO" foo_typer false /
Datatype.Int/Datatype.S_with_collections with type t = int/Deep copy: no possible sharing between x and copy x./
Datatype.Make/functor (X : Datatype.Make_input ) -> Datatype.S with type t = X.t/Generic datatype builder./
-Cil.set_varinfo/Cil.visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo -> unit/change the representative of a given varinfo in the current state of the visitor. Use with care (i.e. makes sure that the old one is not referenced anywhere in the AST, or sharing will be lost./
+Acsl_extension.register_code_annot_next_loop/string -> ?preprocessor:Acsl_extension.extension_preprocessor -> Acsl_extension.extension_typer -> ?visitor:Acsl_extension.extension_visitor -> ?printer:Acsl_extension.extension_printer -> ?short_printer:Acsl_extension.extension_printer -> bool -> unit/Registers extension for loop annotation. See register_behavior./
Cmdline.run_after_setting_files/(string list -> unit) -> unit/Register an action to be executed just after setting the files put on the command line. The argument of the function is the list of files./
Dynamic.register/?comment:string -> plugin:string -> string -> 'a Type.t -> journalize:bool -> 'a -> 'a/register ~plugin name ty v registers v with the name name, the type ty and the plug-in plugin. raised exception: Type.AlreadyExists./
+Cil_types.ext_code_annot_context//can be found both as normal code annot or loop annot./
+Acsl_extension.register_code_annot/string -> ?preprocessor:Acsl_extension.extension_preprocessor -> Acsl_extension.extension_typer -> ?visitor:Acsl_extension.extension_visitor -> ?printer:Acsl_extension.extension_printer -> ?short_printer:Acsl_extension.extension_printer -> bool -> unit/Registers extension for code annotation to be evaluated at _current_ program point. See register_behavior./
Kernel/Parameter_sig.Boolend /Provided services for kernel developers./
Emitter.create/string -> Emitter.kind list -> correctness:Typed_parameter.t list -> tuning:Typed_parameter.t list -> t/Emitter.create name kind ~correctness ~tuning creates a new emitter with the given name. The given parameters are the ones which impact the generated annotations/status. A "correctness" parameter may fully change a generated element when its value changes (for instance, a valid status may become invalid and conversely). A "tuning" parameter may improve a generated element when its value changes (for instance, a "dont_know" status may become valid or invalid, but a valid status cannot become invalid). The given name must be unique. raised exception: Invalid_argument./
+Type.precedence.Call//Instantiation of polymorphic type/
Plugin.Register/string end ) -> Plugin.General_services/Functors for registering a new plug-in. It provides access to several services./
+Visitor_behavior.copy/Project.t -> Visitor_behavior.t/Makes fresh copies of the mutable structures.- preserves sharing for varinfo.- makes fresh copy of varinfo only for declarations. Variables that are only used in the visited AST are thus still shared with the original AST. This allows for instance to copy a function with its formals and local variables, and to keep the references to other globals in the function's body./
Cil.cilVisitor.vlogic_type_info_decl/Cil_types.logic_type_info -> Cil_types.logic_type_info Cil.visitAction//
Dynamic.Parameter.Bool/string -> unit -> unitend /Boolean parameters./
Datatype/functor (W : Datatype.Sub_caml_weak_hashtbl ) -> functor (D : Datatype.S with type t = W.data ) -> Datatype.S with type t = W.tend /A datatype provides useful values for types. It is a high-level API on top of module Type./
-Lattice_type/Lattice_type.Lattice_Hashconsed_Setend /Lattice signatures./
+Lattice_type/Lattice_type.Lattice_Setend /Lattice signatures./
Cabs2cil.convFile/Cabs.file -> Cil_types.file/new hook that will be called when processing a for loop. Argument is the increment part of the loop./
Datatype.Pair/functor (T1 : Datatype.S ) -> functor (T2 : Datatype.S ) -> Datatype.S with type t = T1.t * T2.t/Deep copy: no possible sharing between x and copy x./
Dynamic.get/plugin:string -> string -> 'a Type.t -> 'a/get ~plugin name ty returns the value registered with the name name, the type ty and the plug-in plugin. This plug-in will be loaded if required. raised exceptions: , if the name is not registered, if the name is not registered with a compatible type, _ in the -no-obj mode/
@@ -160,85 +196,118 @@ Annotations.add_assert/Emitter.t -> ?kf:Cil_types.kernel_function -> Cil_types.s
Cil.visitCilFileCopy/Cil.cilVisitor -> Cil_types.file -> Cil_types.file/Visit a file. This will re-cons all globals TWICE (so that it is tail-recursive). Use Cil.visitCilFileSameGlobals if your visitor will not change the list of globals./
Parameter_sig.Kernel_function_set/Parameter_sig.Set with type elt = Cil_types.kernel_function and type t = Cil_datatype.Kf.Set.t/Set of defined kernel functions. If you want to also include pure prototype, use Parameter_customize.argument_may_be_fundecl./
Parameter_sig.Builder.Empty_string/functor (X : Parameter_sig.Input_with_arg ) -> Parameter_sig.String/always return the argument, even if the argument is not a function name./
-Ast.mark_as_changed/unit -> unit/call this function whenever you've made some changes in place inside the AST/
-Log.Messages.result/?level:int -> ?dkey:Log.category -> 'a Log.pretty_printer/Results of analysis. Default level is 1./
+Ast.mark_as_changed/unit -> unit/call this function whenever you've made some changes in place inside the AST/
+Log.Messages.result/?level:int -> ?dkey:Log.Messages.category -> 'a Log.pretty_printer/Results of analysis. Default level is 1./
Kernel.SafeArrays/Parameter_sig.Bool/Behavior of option "-safe-arrays"./
-Cil_types.stmt/{mutable labels: Cil_types.label list; mutable skind: Cil_types.stmtkind; mutable sid: int; mutable succs: Cil_types.stmt list; mutable preds: Cil_types.stmt list; mutable ghost: bool}/Statements./
-Cil.visitCilFileSameGlobals/Cil.cilVisitor -> Cil_types.file -> unit/A visitor for the whole file that does not change the globals (but maybe changes things inside the globals). Use this function instead of Cil.visitCilFile whenever appropriate because it is more efficient for long files./
+Cil_types.stmt//Statements./
+Cil.visitCilFileSameGlobals/Cil.cilVisitor -> Cil_types.file -> unit/A visitor for the whole file that does not *physically* change the globals (but maybe changes things inside the globals through side-effects). Use this function instead of Cil.visitCilFile whenever appropriate because it is more efficient for long files./
+Datatype.S_with_collections/Datatype.S_with_collections/A datatype for a type t extended with predefined set, map and hashtbl over t./
Cmdline.run_after_extended_stage/(unit -> unit) -> unit/Register an action to be executed at the end of the extended stage./
-Db.Value.compute/(unit -> unit) Pervasives.ref/Compute the value analysis using the entry point of the current project. You may set it with Globals.set_entry_point. raised exceptions: , if the entry point is incorrect, if some arguments are specified for the entry point using Db.Value.fun_set_args, and an incorrect number of them is given./
-Cil_types.logic_info/{mutable l_var_info: Cil_types.logic_var; mutable l_labels: Cil_types.logic_label list; mutable l_tparams: string list; mutable l_type: Cil_types.logic_type option; mutable l_profile: Cil_types.logic_var list; mutable l_body: Cil_types.logic_body}/description of a logic function or predicate./
-Cil_types.fundec/{mutable svar: Cil_types.varinfo; mutable sformals: Cil_types.varinfo list; mutable slocals: Cil_types.varinfo list; mutable smaxid: int; mutable sbody: Cil_types.block; mutable smaxstmtid: int option; mutable sallstmts: Cil_types.stmt list; mutable sspec: Cil_types.funspec}/Function definitions./
-Locations.Location_Bytes/bool -> unitend /Association between bases and offsets in byte./
-Project.on/?selection:State_selection.t -> t -> ('a -> 'b) -> 'a -> 'b/on p f x sets the current project to p, computes f x then restores the current project. You should use this function if you use a project different of current ()./
+Db.Value.compute/(unit -> unit) Stdlib.ref/Compute the value analysis using the entry point of the current project. You may set it with Globals.set_entry_point. raised exceptions: , if the entry point is incorrect, if some arguments are specified for the entry point using Db.Value.fun_set_args, and an incorrect number of them is given./
+Visitor_behavior.Get_orig/Visitor_behavior.Get/Get operations on behaviors, allows to get the original representative of an element of the new AST in the curent state of the visitor. Get_orig.ast_element vis new_e with new_e of type ast_element gets the original representative of new_e in vis. For example for Cil_types.varinfo: Get_orig.varinfo vis new_vi./
+Cil_types.stmtkind.TryFinally/ of Cil_types.block * Cil_types.block * Cil_types.location/On MSVC we support structured exception handling. This is what you might expect. Control can get into the finally block either from the end of the body block, or if an exception is thrown./
+Cil_types.logic_info//description of a logic function or predicate./
+Cil_types.fundec//Function definitions./
+Locations.Location_Bytes/Locations.Location_Bytes.t -> Locations.Location_Bytes.tend /Association between bases and offsets in byte./
+Project.on/?selection:State_selection.t -> t -> ('a -> 'b) -> 'a -> 'b/on p f x sets the current project to p, computes f x then restores the current project. You should use this function if you use a project different of current ()./
Cabs/end /Untyped AST./
Design.main_window_extension_points//This is the type of extension points for the GUI./
Pretty_utils/?align:Pretty_utils.align -> ?pp:string Pretty_utils.formatter -> Pretty_utils.marger -> string Pretty_utils.formatterend /Pretty-printer utilities./
+Cil_types.binop.Mod//%/
Dynamic.Parameter/string -> (string -> unit) -> unitend end /Module to use for accessing parameters of plug-ins. Assume that the plug-in is already loaded./
Datatype.Polymorphic2/((Project_skeleton.t -> bool) -> 'a -> bool) -> ((Project_skeleton.t -> bool) -> 'b -> bool) -> (Project_skeleton.t -> bool) -> ('a, 'b) Datatype.t -> bool end ) -> Datatype.Polymorphic2 with type ('a, 'b) poly = ('a, 'b) P.t/Functor for polymorphic types with 2 type variables./
-Parameter_customize.set_negative_option_name/string -> unit/For boolean parameters, set the name of the negative option generating automatically from the positive one (the given option name). The default used value prefixes the given option name by "-no". Assume that the given string is a valid option name or empty. If it is empty, no negative option is created./
-Parameter_state.get_selection/?is_set:bool -> unit -> State_selection.t/Selection of all the settable parameters. is_set is true by default (for backward compatibility): in such a case, for each option, the extra internal state indicating whether it is set also belongs to the selection./
+Cil_types.stmtkind.Block/ of Cil_types.block/Just a block of statements. Use it as a way to keep some block attributes local./
+Cil.visitAction.JustCopyPost/ of ('a -> 'a)/same as JustCopy + applies the given function to the result./
+Parameter_customize.set_negative_option_name/string -> unit/For boolean parameters, set the name of the negative option generating automatically from the positive one (the given option name). The default used value prefixes the given option name by "-no". Assume that the given string is a valid option name or empty. If it is empty, no negative option is created./
+Parameter_state.get_selection/?is_set:bool -> unit -> State_selection.t/Selection of all the settable parameters. is_set is true by default (for backward compatibility): in such a case, for each option, the extra internal state indicating whether it is set also belongs to the selection./
Cil.cilVisitor.vlogic_ctor_info_decl/Cil_types.logic_ctor_info -> Cil_types.logic_ctor_info Cil.visitAction//
-Project.save/?selection:State_selection.t -> ?project:t -> string -> unit/Save a given project in a file. Default project is current (). raised exception: IOError./
-Plugin/(Plugin.plugin -> unit) -> unitend /Provided plug-general services for plug-ins./
-Cil.get_original_varinfo/Cil.visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo/retrieve the original representative of a given copy of a varinfo in the current state of the visitor./
-Cil_types.acsl_extension_kind/ | Ext_id of int | Ext_terms of Cil_types.term list | Ext_preds of Cil_types.predicate list/a list of predicates, the most common case of for extensions/
-Cabs.file//the string is a file name, and then the list of toplevel forms./
-Cil_datatype.Varinfo/tend /Identity of a key. Must verify id k >= 0 and equal k1 k2 ==> id k1 = id k2/
+Project.save/?selection:State_selection.t -> ?project:t -> Filepath.Normalized.t -> unit/Save a given project in a file. Default project is current (). raised exception: IOError./
+Plugin/(Plugin.plugin -> 'a -> 'a) -> 'a -> 'aend /Plugin registration and general services./
+Datatype.Ty.ty/Datatype.Ty.t Type.t//
+Cil_types.acsl_extension_kind//a list of predicates, the most common case of for extensions/
+Cabs.file//the file name, and then the list of toplevel forms./
+State_selection.with_dependencies/State.t -> State_selection.t/The selection containing the given state and all its dependencies./
+Cil_datatype.Varinfo/tend /Identity of a key. Must verify id k >= 0 and equal k1 k2 ==> id k1 = id k2/
+Analysis.is_computed/unit -> bool/Return true iff the Eva analysis has been done./
+Cil_types.global.GFun/ of Cil_types.fundec * Cil_types.location/A function definition./
Cil.cilVisitor.vfile/Cil_types.file -> Cil_types.file Cil.visitAction/visit a whole file./
-Cil.copy_visit/Project.t -> Cil.visitor_behavior/Makes fresh copies of the mutable structures.- preserves sharing for varinfo.- makes fresh copy of varinfo only for declarations. Variables that are only used in the visited AST are thus still shared with the original AST. This allows for instance to copy a function with its formals and local variables, and to keep the references to other globals in the function's body./
-Log.print_delayed/(Format.formatter -> unit) -> unit/Direct printing on output. Same as print_on_output, except that message echo is not delayed until text material is actually written. This gives an chance for formatters to emit messages before actual pretty printing. Can not be recursively invoked./
+Cil_types.global_annotation.Dextended/ of Cil_types.acsl_extension * Cil_types.attributes * Cil_types.location/Extended global clause./
+Log.print_delayed/(Stdlib.Format.formatter -> unit) -> unit/Direct printing on output. Same as print_on_output, except that message echo is not delayed until text material is actually written. This gives an chance for formatters to emit messages before actual pretty printing. Can not be recursively invoked./
Cil.cilVisitor.vvdec/Cil_types.varinfo -> Cil_types.varinfo Cil.visitAction/Invoked for each variable declaration. The children to be traversed are those corresponding to the type and attributes of the variable. Note that variable declarations are GVar, GVarDecl, GFun and GFunDecl globals, the formals of functions prototypes, and the formals and locals of function definitions. This means that the list of formals of a function may be traversed multiple times if there exists both a declaration and a definition, or multiple declarations./
+Datatype.S_no_copy.pretty/Stdlib.Format.formatter -> Datatype.t -> unit/Pretty print each value in an user-friendly way./
Visitor.frama_c_inplace//in-place visitor; always act in the current project./
Abstract_interp/functor (L1 : Lattice_type.AI_Lattice_with_cardinal_one ) -> functor (L2 : Lattice_type.AI_Lattice_with_cardinal_one ) -> Lattice_Sum with type t1 = L1.t and type t2 = L2.tend /Functors for generic lattices implementations./
+Eva.Analysis.is_computed/unit -> bool/Return true iff the Eva analysis has been done./
Log.Messages.verify/bool -> ('a, bool) Log.pretty_aborter/If the first argument is true, return true and do nothing else, otherwise, send the message on the fatal channel and return false. The intended usage is: assert (verify e "Bla...") ;./
-Ast.get/unit -> Cil_types.file/Get the cil file representation. One of the initialisation function of module File has to be called before using this function. raised exception: Bad_Initialization./
-Locations.enumerate_valid_bits/for_writing:bool -> Locations.location -> Locations.Zone.t/Is the valid part of the location bottom or a singleton?/
-File.add_code_transformation_after_cleanup/?deps:(module Parameter_sig.S) list -> ?before:File.code_transformation_category list -> ?after:File.code_transformation_category list -> File.code_transformation_category -> (Cil_types.file -> unit) -> unit/Same as above, but the hook is applied after clean up. At this level, globals and ACSL annotations have been registered. If the hook adds some new globals or annotations, it must take care of adding them in the appropriate tables. Note that it is the responsibility of the hook to use Ast.mark_as_changed or Ast.mark_as_grown whenever it is the case./
-Cil_types.file/{mutable fileName: string; mutable globals: Cil_types.global list; mutable globinit: Cil_types.fundec option; mutable globinitcalled: bool}/The top-level representation of a CIL source file (and the result of the parsing and elaboration). Its main contents is the list of global declarations and definitions. You can iterate over the globals in a Cil_types.file using the following iterators: Cil.mapGlobals, Cil.iterGlobals and Cil.foldGlobals. You can also use the Cil.dummyFile when you need a Cil_types.file as a placeholder. For each global item CIL stores the source location where it appears (using the type Cil_types.location)/
-Type.par/Type.precedence -> Type.precedence -> Format.formatter -> (Format.formatter -> unit) -> unit/par context myself fmt pp puts parenthesis around the verbatim prints by pp according to the precedence myself of the verbatim and to the precedence context of the caller of the pretty printer. fmt is the output formatter. The typical use is the following: let pretty_print p_caller fmt x = let pp fmt = Format.fprintf "..." ... x ... in let myself = Call in par p_caller myself fmt pp/
-Logic_typing.register_behavior_extension/string -> (typing_context:Logic_typing.typing_context -> loc:Cil_types.location -> Logic_ptree.lexpr list -> Cil_types.acsl_extension_kind) -> unit/register_behavior_extension name f registers a typing function f to be used to type clause with name name. Here is a basic example: let count = ref 0 in let foo_typer ~typing_context ~loc ps = match ps with p::[] -> Ext_preds (typing_context.type_predicate typing_context (typing_context.post_state [Normal]) p)) | [] -> let id = !count in incr count; Ext_id id | _ -> typing_context.error loc "expecting a predicate after keyword FOO" let () = register_behavior_extension "FOO" foo_typer/
+Cil.visitAction.SkipChildren//Do not visit the children. Return the node as it is./
+Ast.get/unit -> Cil_types.file/Get the cil file representation. One of the initialization function of module File has to be called before using this function. raised exception: Bad_Initialization./
+Cil_types.stmtkind.Switch/ of Cil_types.exp * Cil_types.block * Cil_types.stmt list * Cil_types.location/A switch statement. exp is the index of the switch. block is the body of the switch. stmt list contains the set of statements whose labels are cases of the switch (i.e. for each case, the corresponding statement is in stmt list, a statement cannot appear more than once in the list, and statements in stmt list can have several labels corresponding to several cases./
+Locations.enumerate_valid_bits/Locations.access -> Locations.location -> Locations.Zone.t/Is there a possibly non-empty intersection between two given locations? If partial is true, returns true if the two locations may be overlapping without being equal. If partial is false, also returns true if the two locations may be equal. Returns false when the two locations cannot be overlapping./
+File.add_code_transformation_after_cleanup/?deps:(module Parameter_sig.S) list -> ?before:File.code_transformation_category list -> ?after:File.code_transformation_category list -> File.code_transformation_category -> (Cil_types.file -> unit) -> unit/Same as above, but the hook is applied after clean up. At this level, globals and ACSL annotations have been registered. If the hook adds some new globals or annotations, it must take care of adding them in the appropriate tables. Note that it is the responsibility of the hook to use Ast.mark_as_changed or Ast.mark_as_grown whenever it is the case./
+Cil_types.file//The top-level representation of a CIL source file (and the result of the parsing and elaboration). Its main contents is the list of global declarations and definitions. You can iterate over the globals in a Cil_types.file using the following iterators: Cil.mapGlobals, Cil.iterGlobals and Cil.foldGlobals. You can also use the Cil.dummyFile when you need a Cil_types.file as a placeholder. For each global item CIL stores the source location where it appears (using the type Cil_types.location)/
+Type.par/Type.precedence -> Type.precedence -> Stdlib.Format.formatter -> (Stdlib.Format.formatter -> unit) -> unit/par context myself fmt pp puts parenthesis around the verbatim prints by pp according to the precedence myself of the verbatim and to the precedence context of the caller of the pretty printer. fmt is the output formatter. The typical use is the following: let pretty_print p_caller fmt x = let pp fmt = Format.fprintf "..." ... x ... in let myself = Call in par p_caller myself fmt pp/
Datatype.bool/bool Type.t//
-Datatype.pp_fail/Type.precedence -> Format.formatter -> 'a -> unit/Must be used for internal_pretty_code if this pretty-printer must fail only when called./
+Datatype.pp_fail/Type.precedence -> Stdlib.Format.formatter -> 'a -> unit/Must be used for internal_pretty_code if this pretty-printer must fail only when called./
Visitor.visitFramacFileSameGlobals/Visitor.frama_c_visitor -> Cil_types.file -> unit/A visitor for the whole file that does not change the globals (but maybe changes things inside the globals). Use this function instead of Visitor.visitFramacFile whenever appropriate because it is more efficient for long files./
-Log.Messages.with_log/(Log.event -> 'b) -> ?kind:Log.kind -> ('a, 'b) Log.pretty_aborter//
-Cil.visitor_behavior//Visitor behaviorHow the visitor should behave in front of mutable fields: in place modification or copy of the structure. This type is abstract. Use one of the two values below in your classes./
+Structural_descr.t.Structure/ of Structural_descr.structure/Provide a description of the representation of data./
+Cil_types.relation.Rneq//Different/
+Cil_types.stmtkind.Return/ of Cil_types.exp option * Cil_types.location/The return statement. This is a leaf in the CFG./
Cmdline.run_after_early_stage/(unit -> unit) -> unit/Register an action to be executed at the end of the early stage./
-Cil_types.logic_var/{mutable lv_name: string; mutable lv_id: int; mutable lv_type: Cil_types.logic_type; mutable lv_kind: Cil_types.logic_var_kind; mutable lv_origin: Cil_types.varinfo option; mutable lv_attr: Cil_types.attributes}/description of a logic variable/
-Dataflow/Cil_types.fundec -> Cil_types.stmt list * Cil_types.stmt listend /Deprecated: use Dataflows instead. A framework for implementing data flow analysis./
-Log.log_channel/Log.channel -> ?kind:Log.kind -> ?prefix:Log.prefix -> 'a Log.pretty_printer/logging function to user-created channel./
-Db.progress/(unit -> unit) Pervasives.ref/This function should be called from time to time by all analysers taking time. In GUI mode, this will make the interface reactive./
-Kernel_function.get_definition/t -> Cil_types.fundec/For functions with a declaration and a definition, returns the definition. raised exception: No_Definition./
+Cil.visitAction.ChangeToPost/ of 'a * ('a -> 'a)/applies the expression to the function and gives back the result. Useful to insert some actions in an inheritance chain./
+Cil_types.logic_var//description of a logic variable/
+Cil_types.exp_node.BinOp/ of Cil_types.binop * Cil_types.exp * Cil_types.exp * Cil_types.typ/Binary operation. Includes the type of the result. The arithmetic conversions are made explicit for the arguments./
+Log.log_channel/Log.channel -> ?kind:Log.kind -> 'a Log.pretty_printer/logging function to user-created channel./
+Cil_types.stmtkind.Loop/ of Cil_types.code_annotation list * Cil_types.block * Cil_types.location * Cil_types.stmt option * Cil_types.stmt option/A while(1) loop. The termination test is implemented in the body of a loop using a Break statement. If Cfg.prepareCFG has been called, the first stmt option will point to the stmt containing the continue label for this loop and the second will point to the stmt containing the break label for this loop./
+Db.progress/(unit -> unit) Stdlib.ref/This function should be called from time to time by all analysers taking time. In GUI mode, this will make the interface reactive./
+Kernel_function.get_definition/t -> Cil_types.fundec/Returns the list of static variables declared inside the function. raised exception: No_Definition./
Datatype.char/char Type.t//
+Visitor_behavior.Get.stmt/Visitor_behavior.t -> Cil_types.stmt -> Cil_types.stmt/Fold operations on table of a given type of AST elements. Fold.ast_element vis f, folds f over each pair of ast_element registered in vis. The ast_element in the old AST is presented to f first (that is, f looks like: let f old_e new_e acc = .... For example for Cil_types.varinfo: Fold.varinfo vis (fun old_vi new_vi acc -> ... )./
Cil.cilVisitor.vlogic_info_decl/Cil_types.logic_info -> Cil_types.logic_info Cil.visitAction/link to the current function being visited. NB: for copy visitors, the fundec is the original one./
-Cil_types.acsl_extension//extension to standard ACSL clause. Each extension is associated to a keyword. An extension can be registered through the following functions:- Logic_typing.register_behavior_extension for parsing and type-checking- Cil_printer.register_behavior_extension for pretty-printing an extended clause- Cil.register_behavior_extension for visiting an extended clause/
-Cil_types.offset/ | NoOffset | Field of Cil_types.fieldinfo * Cil_types.offset | Index of Cil_types.exp * Cil_types.offset/The offset part of an Cil_types.lval. Each offset can be applied to certain kinds of lvalues and its effect is that it advances the starting address of the lvalue and changes the denoted type, essentially focussing to some smaller lvalue that is contained in the original one./
+Cil_types.acsl_extension//Extension to standard ACSL clause with an unique identifier. The integer is a (unique) identifier. The boolean flag is true if the annotation can be assigned a property status. Use Logic_const.new_acsl_extension to create new acsl extension with a fresh id. Each extension is associated with a keyword, and can be either a global annotation, the clause of a function contract, a code annotation, or a loop annotation. An extension can be registered through the function Acsl_extension.register_xxx. It is _not_ possible to register the same keyword for annotations at two different levels (e.g. global and behavior), as this would make the grammar ambiguous./
+Cil_types.offset//The offset part of an Cil_types.lval. Each offset can be applied to certain kinds of lvalues and its effect is that it advances the starting address of the lvalue and changes the denoted type, essentially focussing to some smaller lvalue that is contained in the original one./
+Cil.visitAction.DoChildrenPost/ of ('a -> 'a)/visit the children, and apply the given function to the result./
Datatype.Bool/Datatype.S_with_collections with type t = bool/Deep copy: no possible sharing between x and copy x./
Cil.cilVisitor.vlogic_info_use/Cil_types.logic_info -> Cil_types.logic_info Cil.visitAction//
-File.new_file_type/string -> (string -> Cil_types.file * Cabs.file) -> unit/new_file_type suffix func funcname registers a new type of files (with corresponding suffix) as recognized by Frama-C through func./
+File.new_file_type/string -> (string -> Cil_types.file * Cabs.file) -> unit/new_file_type suffix func funcname registers a new type of files (with corresponding suffix) as recognized by Frama-C through func./
Log.Messages.log/?kind:Log.kind -> ?verbose:int -> ?debug:int -> 'a Log.pretty_printer/Generic log routine. The default kind is Result. Use cases (with n,m > 0):- log ~verbose:n: emit the message only when verbosity level is at least n.- log ~debug:n: emit the message only when debugging level is at least n.- log ~verbose:n ~debug:m: any debugging or verbosity level is sufficient./
Type/'b Type.Obj_tbl.t -> ('a Type.ty -> 'a -> 'b -> unit) -> unitend end /Type value. A type value is a value representing a static ML monomorphic type. This API is quite low level. Prefer to use module Datatype instead whenever possible./
+Cmdline.stage.Exiting//Run once when exiting Frama-C./
Datatype.identity/'a -> 'a/Must be used if you want to implement a required function by fun x -> x. Only useful for implementing rehash and copy./
-State_selection/end /A state selection is a set of states with operations for easy handling of state dependencies./
-Project.set_current/?on:bool -> ?selection:State_selection.t -> t -> unit/Set the current project with the given one. The flag on is not for casual users. raised exception: Invalid_argument./
+State_selection/(State.t -> 'a -> 'a) -> State_selection.t -> 'a -> 'aend /A state selection is a set of states with operations for easy handling of state dependencies./
+Project.set_current/?on:bool -> ?selection:State_selection.t -> t -> unit/Set the current project with the given one. The flag on is not for casual users. raised exception: Invalid_argument./
Logic_const/Cil_types.term_offset -> Cil_types.term_lval -> Cil_types.term_lvalend /Smart constructors for logic annotations./
Cil.cilVisitor.vlogic_type_info_use/Cil_types.logic_type_info -> Cil_types.logic_type_info Cil.visitAction//
+Project.IOError/string/register_before_remove_hook f adds a hook called just before removing a project./
Kernel_function.Make_Table/functor (Data : Datatype.S ) -> functor (Info : State_builder.Info_with_size ) -> State_builder.Hashtbl with type key = t and type data = Data.t/Hashtable indexed by kernel functions and dealing with project./
-State_builder.Ref/unit -> Data.t end ) -> State_builder.Ref with type data = Data.t/Deep copy: no possible sharing between x and copy x./
-File.add_code_transformation_before_cleanup/?deps:(module Parameter_sig.S) list -> ?before:File.code_transformation_category list -> ?after:File.code_transformation_category list -> File.code_transformation_category -> (Cil_types.file -> unit) -> unit/add_code_transformation_before_cleanup name hook adds an hook in the corresponding category that will be called during the normalization of a linked file, before clean up and removal of temps and unused declarations. If this transformation involves changing statements of a function f, f must be flagged with File.must_recompute_cfg. The optional before (resp after) categories indicates that current transformation must be executed before (resp after) the corresponding ones, if they exist. In case of dependencies cycle, an arbitrary order will be chosen for the transformations involved in the cycle. The optional deps argument gives the list of options whose change (e.g. after a -then) will trigger the transformation over the already computed AST. If several transformations are triggered by the same option, their relative order is preserved. At this level, globals and ACSL annotations have not been registered./
+State_builder.Ref/unit -> Data.t end ) -> State_builder.Ref with type data = Data.t and type Datatype.t = Data.t ref/Deep copy: no possible sharing between x and copy x./
+Visitor_behavior.Get.kernel_function/Visitor_behavior.t -> Cil_types.kernel_function -> Cil_types.kernel_function//
+Cmdline.stage.Configuring//The stage where all the parameters which were not already set may be modified to take into account cmdline options. Just after this stage, Frama-C will run the plug-in mains./
+Acsl_extension.register_global/string -> ?preprocessor:Acsl_extension.extension_preprocessor -> Acsl_extension.extension_typer -> ?visitor:Acsl_extension.extension_visitor -> ?printer:Acsl_extension.extension_printer -> ?short_printer:Acsl_extension.extension_printer -> bool -> unit/Registers extension for global annotation. See register_behavior./
+File.add_code_transformation_before_cleanup/?deps:(module Parameter_sig.S) list -> ?before:File.code_transformation_category list -> ?after:File.code_transformation_category list -> File.code_transformation_category -> (Cil_types.file -> unit) -> unit/add_code_transformation_before_cleanup name hook adds an hook in the corresponding category that will be called during the normalization of a linked file, before clean up and removal of temps and unused declarations. If this transformation involves changing statements of a function f, f must be flagged with File.must_recompute_cfg. The optional before (resp after) categories indicates that current transformation must be executed before (resp after) the corresponding ones, if they exist. In case of dependencies cycle, an arbitrary order will be chosen for the transformations involved in the cycle. The optional deps argument gives the list of options whose change (e.g. after a -then) will trigger the transformation over the already computed AST. If several transformations are triggered by the same option, their relative order is preserved. At this level, globals and ACSL annotations have not been registered./
Db/end /Database in which static plugins are registered./
+Cmdline.stage.Extending//Before loading plug-ins. Run only once./
+Analysis.compute/unit -> unit/Computes the Eva analysis, if not already computed, using the entry point of the current project. You may set it with Globals.set_entry_point. raised exceptions: , if the entry point is incorrect, if some arguments are specified for the entry point using Db.Value.fun_set_args, and an incorrect number of them is given./
+Type.precedence.Basic//Normal precedence/
+FCHashtbl/int -> int -> 'a -> intend /Extension of OCaml's Hashtbl module./
+Cil_datatype.Fundec/Cil_datatype.S_with_collections_pretty with type t = fundec//
+Acsl_extension.register_code_annot_next_both/string -> ?preprocessor:Acsl_extension.extension_preprocessor -> Acsl_extension.extension_typer -> ?visitor:Acsl_extension.extension_visitor -> ?printer:Acsl_extension.extension_printer -> ?short_printer:Acsl_extension.extension_printer -> bool -> unit/Registers extension both for code and loop annotations. See register_behavior./
+From_parameters.ForceCallDeps/Parameter_sig.With_output/Option -calldeps./
Type.Abstract/Type.Abstract.t Type.tyend /Apply this functor to access to the abstract type of the given name. raised exception: No_abstract_type./
+Cil_types.behavior//Behavior of a function or statement. This type shares the name of its constructors with Logic_ptree.behavior./
Logic_utils/unit -> boolend /Utilities for ACSL constructs./
+Cil_types.stmtkind.Continue/ of Cil_types.location/A continue to the start of the nearest enclosing Loop./
Cil.cilVisitor.voffs/Cil_types.offset -> Cil_types.offset Cil.visitAction/Invoked on each offset occurrence that is *not* as part of an initializer list specification, i.e. in an lval or recursively inside an offset./
Cil.cilVisitor.vlogic_ctor_info_use/Cil_types.logic_ctor_info -> Cil_types.logic_ctor_info Cil.visitAction//
-Log.print_on_output/(Format.formatter -> unit) -> unit/Direct printing on output. Message echo is delayed until the output is finished. Then, the output is flushed and all pending message are echoed. Notification of listeners is not delayed, however. Can not be recursively invoked./
+Log.print_on_output/(Stdlib.Format.formatter -> unit) -> unit/Direct printing on output. Message echo is delayed until the output is finished. Then, the output is flushed and all pending message are echoed. Notification of listeners is not delayed, however. Can not be recursively invoked./
Visitor.frama_c_visitor.vglob_aux/Cil_types.global -> Cil_types.global list Cil.visitAction/Replacement of vglob./
+Visitor_behavior.t//How the visitor should behave in front of mutable fields: in place modification or copy of the structure. This type is abstract. Use one of the two values below in your classes./
Cmdline.run_after_configuring_stage/(unit -> unit) -> unit/Register an action to be executed at the end of the configuring stage./
Project.current/unit -> t/The current project. raised exception: NoProject./
State.dummy/t/A dummy state./
-Project_skeleton.t/{pid: int; mutable name: string; mutable unique_name: string}/No function is exported. Extension of the GUI in order to support project switching./
-Cil.get_kernel_function/Cil.visitor_behavior -> Cil_types.kernel_function -> Cil_types.kernel_function//
+Project_skeleton.t//This module should not be used outside of the Project library./
File.new_machdep/string -> Cil_types.mach -> unit/new_machdep name module registers a new machdep name as recognized by Frama-C through The usual uses is Cmdline.run_after_loading_stage (fun () -> File.new_machdep "my_machdep" my_machdep_implem) raised exception: Invalid_argument./
State_builder/?prj:Project.t -> string -> 'a Type.t -> 'a * boolend end /State builders. Provide ways to implement signature State_builder.S. Depending on the builder, also provide some additional useful information./
+Datatype.S_no_copy.equal/Datatype.t -> Datatype.t -> bool/Equality: same spec than Stdlib.(=)./
Cil.cilVisitor.current_kinstr/Cil_types.kinstr/Kstmt stmt when visiting statement stmt, Kglobal when called outside of a statement./
-Parameter_sig.Int/Parameter_sig.Int/Signature for an integer parameter./
\ No newline at end of file
+Parameter_sig.Int/Parameter_sig.Int/Signature for an integer parameter./
+Visitor_behavior.Memo/Visitor_behavior.Get/Memo operations on behaviors, allows to get a binding in the new project for the given AST element, creating one if it does not already exists. Memo.ast_element vis e with e of type ast_element tries to find a binding to a e in the new project created using vis in the current state, if it does not exist this binding is created. For example for Cil_types.varinfo: Memo.varinfo vis vi./
\ No newline at end of file
diff --git a/doc/developer/tutorial.tex b/doc/developer/tutorial.tex
index 832fee3fcc70f60857c2526e8fe0df54c365887e..f53f9402a64563223b2aa41cd9065c307dacb14c 100644
--- a/doc/developer/tutorial.tex
+++ b/doc/developer/tutorial.tex
@@ -797,7 +797,7 @@ nothing for the other globals.
\sscodeidx{Cil}{visitAction}{DoChildrenPost}
\sscodeidx{Cil}{visitAction}{SkipChildren}
\sscodeidx{Visitor}{frama\_c\_visitor}{vglob\_aux}
-\scodeidx{Cil\_types}{GFun}
+\sscodeidx{Cil\_types}{global}{GFun}
\scodeidx{Printer\_api}{S.pp\_varinfo}
\texttt{Cil.SkipChildren} tells the visitor not to visit the children
@@ -976,6 +976,15 @@ CFG'' item appears, that displays the control flow graph of the
function in a dialog box. This is achieved just by appending the following
pieces of code at the end of the \texttt{cfg\_print.ml} file.
+\begin{important}
+Frama-C's GUI can be compiled against two versions of lablgtk (the OCaml
+bindings to the Gtk toolkit). The actual rendering of the control flow graph
+is actually done by the external OCamlgraph library, and only available
+when compiling against lablgtk2. If you're using lablgtk3,
+you will only see a pop-up window indicating that there's no support for
+displaying graphs.
+\end{important}
+
Currently, we used a visitor that outputs a \dottool file with the CFG of
all functions of all files. We use \texttt{dump\_function} to output
the CFG of a single function instead.
@@ -990,10 +999,10 @@ representing a function definition.
Now we write the GUI extension code:
\ocamlinput{./tutorial/viewcfg/src/gui.ml}
-\scodeidx{Pretty\_source}{PVDecl}
+\sscodeidx{Pretty\_source}{localizable}{PVDecl}
\sscodeidx{Globals}{Functions}{get}
\scodeidx{Kernel\_function}{get\_definition}
-\scodeidx{Gtk\_helper}{graph\_window}
+\scodeidx{Dgraph\_helper}{graph\_window}
\scodeidx{Design}{register\_extension}
\sscodeidx{Design}{main\_window\_extension\_points}{register\_source\_selector}
@@ -1169,7 +1178,7 @@ Registering a state is done by a functor application:
\ocamlinput{./tutorial/viewcfg/src/register_cfg_graph_state.ml}
\scodeidx{State\_builder}{Hashtbl}
-\sscodeidx{Cil\_datatype}{Fundec}{Hashtbl}
+\scodeidx{Cil\_datatype}{Fundec}
\scodeidx{Datatype}{String}
\scodeidx{Ast}{self}
\sscodeidx{Db}{Value}{self}
@@ -1256,7 +1265,7 @@ following.
\ocamlinput{./tutorial/viewcfg/src/dump_function_memo_clear_cache.ml}
\sscodeidx{Db}{Value}{is\_computed}
-\scodeidx{State\_selection}{with\_dependencies}
+\sscodeidx{State\_selection}{S}{with\_dependencies}
\scodeidx{Project}{clear}
The only part that need to be explained is the notion of
@@ -1280,7 +1289,8 @@ val clear: ?selection:State_selection.t -> ?project:t -> unit -> unit
\end{ocamlcode}
\scodeidxdef{Project}{clear}
\scodeidx{State\_selection}{t}
-\scodeidx{Project}{t}
+\codeidx{Project}
+\sscodeidx{Datatype}{Ty}{t}
The arguments \texttt{selection} and \texttt{project} can be seen as a
coordinate system, and the function allows to clear specific versions
@@ -1309,7 +1319,7 @@ To summarize:
when the former is modified in an incompatible way. For instance, it would
have been incorrect to not call
\texttt{State\_selection.with\_dependencies}
- \scodeidx{State\_selection}{with\_dependencies} in the last code snippet of
+ \sscodeidx{State\_selection}{S}{with\_dependencies} in the last code snippet of
this tutorial.
\end{itemize}
diff --git a/doc/developer/tutorial/hello/Makefile b/doc/developer/tutorial/hello/Makefile
index cdeaa65fbabc6fdcbcd072b58387dd47bd62029c..94d8f6148ccf99409a28556efa0b2e4dcda8024f 100644
--- a/doc/developer/tutorial/hello/Makefile
+++ b/doc/developer/tutorial/hello/Makefile
@@ -104,6 +104,7 @@ generated/makefile_multiple: generated/src/help_msg.ml \
generated/with_test: generated/src/run_call_print_bug.ml \
generated/src/tests/hello/hello_test.c \
+ generated/src/tests/hello/oracle/hello_test.res.oracle \
generated/src/Makefile.test
mkdir -p $@
cp generated/makefile_multiple/hello_options.ml $@/hello_options.ml
@@ -112,8 +113,9 @@ generated/with_test: generated/src/run_call_print_bug.ml \
cp generated/src/run_call_print_bug.ml $@/hello_run_bug.ml
echo "" >> $@/hello_run_bug.ml
cat generated/src/extend_run.ml >> $@/hello_run_bug.ml
- mkdir -p $@/tests/hello
+ mkdir -p $@/tests/hello/oracle
cp generated/src/tests/hello/hello_test.c $@/tests/hello/hello_test.c
+ cp generated/src/tests/hello/oracle/hello_test.res.oracle $@/tests/hello/oracle/hello_test.res.oracle
cp generated/src/Makefile.test $@/Makefile
generated/with_doc: generated/src/help_msg.ml \
diff --git a/doc/developer/tutorial/hello/src/hello_test.c b/doc/developer/tutorial/hello/src/hello_test.c
index 6ee10eeafa3bf084d6bb579ed00d4b31076b3a4b..9fcbfc12af7290704fe8367dfa4c18c556751347 100644
--- a/doc/developer/tutorial/hello/src/hello_test.c
+++ b/doc/developer/tutorial/hello/src/hello_test.c
@@ -1,3 +1,4 @@
/* run.config
+ PLUGIN: Hello
OPT: -hello
- */
\ No newline at end of file
+ */
diff --git a/doc/developer/tutorial/hello/src/hello_test.res.oracle b/doc/developer/tutorial/hello/src/hello_test.res.oracle
index 32e9c05eee637f6c2347a8584c15369651faaa6a..5f6ab2389a8695bba00d6527d2135e7cc3389c6b 100644
--- a/doc/developer/tutorial/hello/src/hello_test.res.oracle
+++ b/doc/developer/tutorial/hello/src/hello_test.res.oracle
@@ -1,2 +1,2 @@
-[kernel] Parsing tests/hello/hello_test.c (with preprocessing)
+[kernel] Parsing hello_test.c (with preprocessing)
[hello] Hello, world!
diff --git a/doc/developer/tutorial/viewcfg/src/Makefile.split b/doc/developer/tutorial/viewcfg/src/Makefile.split
index ee56b8cad49061542f416bac73f901bb8ce4c325..3d0922804d614f9c43366c029efe16a5f36a1ba9 100644
--- a/doc/developer/tutorial/viewcfg/src/Makefile.split
+++ b/doc/developer/tutorial/viewcfg/src/Makefile.split
@@ -1,5 +1,6 @@
FRAMAC_SHARE := $(shell frama-c-config -print-share-path)
-PLUGIN_NAME = ViewCfg
-PLUGIN_CMO = cfg_options cfg_core cfg_register
-PLUGIN_GUI_CMO = cfg_gui
+PLUGIN_NAME:= ViewCfg
+PLUGIN_CMO:= cfg_options cfg_core cfg_register
+PLUGIN_GUI_CMO:= cfg_gui
+PLUGIN_DEPENDENCIES:=eva
include $(FRAMAC_SHARE)/Makefile.dynamic
diff --git a/doc/release/build.tex b/doc/release/build.tex
index e95334456938807a721bd3feefeab4641b3198cf..204751c397533b2a27013ce286bf178eb0994585 100644
--- a/doc/release/build.tex
+++ b/doc/release/build.tex
@@ -203,9 +203,9 @@ make -j byte gui-byte
make doc # or just doc-kernel
\end{shell}
-\todo{What is this step:
-check consistency of API documentation. (the plug-in development guide
- (\texttt{make check-devguide}) doesn't work anymore)}
+You can also check that the elements referred to in the index of the
+development guide are marked as such in the API doc and vice-versa
+by issuing \texttt{make check-devguide}.
\section{Build the Source Distribution}
\label{sec:build-source-distr}
diff --git a/share/Makefile.dynamic_config.external b/share/Makefile.dynamic_config.external
index 298c4ceab2036ba1c823bf6738a4557e88d83a7d..bb292956a60bae3a8a82bb794cf0832d086476d0 100644
--- a/share/Makefile.dynamic_config.external
+++ b/share/Makefile.dynamic_config.external
@@ -20,8 +20,6 @@
# #
##########################################################################
-export FRAMAC_INTERNAL=no
-
export FRAMAC_OPT=$(BINDIR)/frama-c$(EXE)
export FRAMAC_BYTE=$(BINDIR)/frama-c.byte$(EXE)
diff --git a/share/Makefile.dynamic_config.internal b/share/Makefile.dynamic_config.internal
index b49d5e38fa946e457f703df44d961117e0aeb9d0..d0dc72810bcc5418e0107c004d98121de5f69a1b 100644
--- a/share/Makefile.dynamic_config.internal
+++ b/share/Makefile.dynamic_config.internal
@@ -20,7 +20,7 @@
# #
##########################################################################
-export FRAMAC_INTERNAL=yes
+export FRAMAC_INTERNAL?=yes
export FRAMAC_OPT=$(FRAMAC_ROOT_SRCDIR)/bin/toplevel.opt$(EXE)
export FRAMAC_BYTE=$(FRAMAC_ROOT_SRCDIR)/bin/toplevel.byte$(EXE)
diff --git a/share/Makefile.plugin.template b/share/Makefile.plugin.template
index 976ab0f64615566a95fb0e05d58c2ffc027ea2fe..a00758817d2b640aff5ea8b5d2bc8a66ec5cf39d 100644
--- a/share/Makefile.plugin.template
+++ b/share/Makefile.plugin.template
@@ -762,6 +762,9 @@ ifneq ($(ENABLE_GUI),no)
OCAMLDOC_DEPEND:= $(OCAMLDOC_DEPEND) $(PLUGIN_GUI_CMO)
endif
+PLUGIN_DOC_DUMP:=$(@PLUGIN_NAME@_DOC_DIR)/@PLUGIN_NAME@.ocamldoc
+@PLUGIN_NAME@_DOC_DUMP:=$(PLUGIN_DOC_DUMP)
+
.PHONY: @PLUGIN_NAME@_DOC
@PLUGIN_NAME@_DOC: $(OCAMLDOC_DEPEND) \
$(OCAMLDOC_GEN) \
@@ -780,6 +783,7 @@ endif
-t "@PLUGIN_NAME@ plugin" \
-css-style ../style.css \
-d $(@PLUGIN_NAME@_DOC_DIR) -g $(DOC_PLUGIN) -passopt -docpath $(DOC_DIR)/html \
+ -dump $(@PLUGIN_NAME@_DOC_DUMP) \
$(addprefix -load ,$(wildcard $(DOC_DIR)/kernel-doc.ocamldoc)) \
$(wildcard $(@PLUGIN_NAME@_DOC_SRC))
# [rb+js] 20090619
@@ -798,6 +802,7 @@ endif
$(ISED) -e 's|\(doc/code/html\)|../../../\1|g' $$f ; \
done
+PLUGIN_DOC_DUMP_LIST+=$(PLUGIN_DOC_DUMP)
# removed dependencies:
# $(PLUGIN_DOC_DIR)/modules.ps \
diff --git a/src/kernel_internals/runtime/boot.mli b/src/kernel_internals/runtime/boot.mli
index 00218e7f71ed938b0927aa1169b5f27da247c510..11d608fcaced570e6d4586bd475b091c177a9b77 100644
--- a/src/kernel_internals/runtime/boot.mli
+++ b/src/kernel_internals/runtime/boot.mli
@@ -20,4 +20,6 @@
(* *)
(**************************************************************************)
-(** Nothing is exported. *)
+(** Main entry point of Frama-C. Nothing is exported.
+ @plugin development guide
+*)
diff --git a/src/kernel_services/analysis/dataflow2.mli b/src/kernel_services/analysis/dataflow2.mli
index 904542fe9b18f29fc1b2147120ff892c18b1c4e4..25f8da8cedf699d3ed2fddb5afb828d5b36b26f2 100644
--- a/src/kernel_services/analysis/dataflow2.mli
+++ b/src/kernel_services/analysis/dataflow2.mli
@@ -20,8 +20,11 @@
(* *)
(**************************************************************************)
-(** Implementation of data flow analyses over user-supplied domains. *)
+(** Implementation of data flow analyses over user-supplied domains.
+ @plugin development guide
+*)
+(** possible kinds of action for backward analysis *)
type 't action =
Default (** The default action *)
| Done of 't (** Do not do the default action. Use this result *)
diff --git a/src/kernel_services/ast_data/annotations.mli b/src/kernel_services/ast_data/annotations.mli
index cea099e3d89ba723c173ff56b3e19656aafe96d0..443ace6310713cbfc0e773f0a4458d7a30853b60 100644
--- a/src/kernel_services/ast_data/annotations.mli
+++ b/src/kernel_services/ast_data/annotations.mli
@@ -297,13 +297,13 @@ val add_check:
Emitter.t -> ?kf:kernel_function -> stmt -> predicate -> unit
(** Add a checking assertion attached to the given statement. If [kf] is
provided, the function runs faster.
- @plugin development guide *)
+*)
val add_admit:
Emitter.t -> ?kf:kernel_function -> stmt -> predicate -> unit
(** Add an hypothesis assertion attached to the given statement. If [kf] is
provided, the function runs faster.
- @plugin development guide *)
+*)
val add_global: Emitter.t -> global_annotation -> unit
(** Add a new global annotation into the program. *)
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 8f13b954a39d7337a3a5e7eca15af4964316c234..76bf365de0d1e9064f92f438b68105115f1edfe8 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -143,7 +143,9 @@ and global =
entire program. Cannot have storage Extern or function type. *)
| GFun of fundec * location
- (** A function definition. *)
+ (** A function definition.
+ @plugin development guide
+ *)
| GAsm of string * location
(** Global asm statement. These ones can contain only a template *)
@@ -1525,7 +1527,7 @@ and relation =
| Rle
| Rge
| Req
- | Rneq (** @plugin development guide *)
+ | Rneq (** Different @plugin development guide *)
(** predicates *)
@@ -1681,6 +1683,7 @@ and ext_category =
| Ext_global
| Ext_code_annot of ext_code_annot_context
+(** @plugin development guide *)
and ext_code_annot_context =
| Ext_here (** at current program point. *)
| Ext_next_stmt (** covers next statement. *)
@@ -1693,6 +1696,8 @@ and ext_code_annot_context =
@since Carbon-20101201 [b_requires] has been added.
@modify Boron-20100401 [b_ensures] is replaced by [b_post_cond].
Old [b_ensures] represent the [Normal] case of [b_post_cond].
+
+ @plugin development guide
*)
and behavior = {
mutable b_name : string; (** name of the behavior. *)
@@ -1703,8 +1708,7 @@ and behavior = {
mutable b_assigns : assigns; (** assignments. *)
mutable b_allocation : allocation; (** frees, allocates. *)
mutable b_extended : acsl_extension list
- (** extensions
- @plugin development guide *)
+ (** extensions *)
}
(** kind of termination a post-condition applies to. See ACSL manual. *)
@@ -1768,7 +1772,10 @@ and code_annotation_node =
| AExtended of string list * bool * acsl_extension
(** extension in a code or loop annotation.
Boolean flag is true for loop extensions and false for code extensions
- @since Silicon-20161101 *)
+ @since Silicon-20161101
+
+ @plugin development guide
+ *)
(** function contract. *)
@@ -1806,7 +1813,9 @@ and global_annotation =
(** Model field for a type t, seen as a logic function with one
argument of type t *)
| Dextended of acsl_extension * attributes * location
- (** Extended global clause. *)
+ (** Extended global clause.
+ @plugin development guide
+ *)
type kinstr =
| Kstmt of stmt
diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index 807648fbb378e86a9e0df39f6810bc800242db47..af6cce3d44a8e5ad63d9ee54ab28e893a483e040 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/src/kernel_services/ast_queries/cil_datatype.mli
@@ -218,6 +218,8 @@ module OffsetStructEq: S_with_collections with type t = offset
module OffsetStructEqStrict: S_with_collections with type t = offset
module Stmt_Id: Hptmap.Id_Datatype with type t = stmt
+
+(** @plugin development guide *)
module Stmt: sig
include S_with_collections_pretty with type t = stmt
module Hptset: sig
@@ -299,7 +301,9 @@ module Funbehavior: S_with_pretty with type t = funbehavior
module Funspec: S_with_pretty with type t = funspec
-(** @since Fluorine-20130401 *)
+(** @since Fluorine-20130401
+ @plugin development guide
+*)
module Fundec: S_with_collections_pretty with type t = fundec
module Global_annotation: sig
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index e28f890ce5d2ee571f74e0fd23d830695ef25815..a28ab252637beaf4ee4f19fdb0db1e30cd4077f5 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -85,13 +85,16 @@ module Lenv : sig
end
-type type_namespace = Typedef | Struct | Union | Enum
(** The different namespaces a C type can belong to, used when we are searching
a type by its name. *)
+type type_namespace = Typedef | Struct | Union | Enum
module Type_namespace: Datatype.S with type t = type_namespace
-(** Functions that can be called when type-checking an extension of ACSL. *)
+(** Functions that can be called when type-checking an extension of ACSL.
+
+ @plugin development guide
+*)
type typing_context = {
is_loop: unit -> bool;
anonCompFieldName : string;
@@ -129,8 +132,6 @@ type typing_context = {
[typing_context], which allows for open recursion. Namely, it is
possible for the extension to change the type-checking functions for
the sub-nodes of the parsed tree, and not only for the toplevel [lexpr].
-
- @plugin development guide
*)
type_term:
typing_context -> Lenv.t -> Logic_ptree.lexpr -> term;
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index ef79c06f510414ea50d57d1a24f4484cea12a90a..c12b050d8a0776b6157a92af8c104e35d1f6387e 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -180,6 +180,7 @@ val expr_to_term : ?coerce:bool -> exp -> term
[expr_to_predicate] instead.
@modify 21.0-Scandium
+ @plugin development guide
*)
val expr_to_predicate: exp -> predicate
diff --git a/src/kernel_services/cmdline_parameters/typed_parameter.mli b/src/kernel_services/cmdline_parameters/typed_parameter.mli
index 55534d228298066cd472566b8a1e307be19bc511..605be08c5c4c771cd6080bdaccae7e7971931b95 100644
--- a/src/kernel_services/cmdline_parameters/typed_parameter.mli
+++ b/src/kernel_services/cmdline_parameters/typed_parameter.mli
@@ -23,8 +23,11 @@
(** Parameter settable through a command line option.
This is a low level API, internally used by the kernel. As a plug-in
developer, you certainly prefer to use the API of {!Plugin} instead.
- @since Nitrogen-20111001 *)
+ @since Nitrogen-20111001
+ @plugin development guide
+*)
+(** generic accessor type *)
type ('a, 'b) gen_accessor =
{ get: unit -> 'a;
set: 'a -> unit;
diff --git a/src/kernel_services/plugin_entry_points/log.mli b/src/kernel_services/plugin_entry_points/log.mli
index 72740f68e89e8842d5fa7b6c60ae5b4246d12f93..5dce8e57a5a491535c8267915b14de2d8325c406 100644
--- a/src/kernel_services/plugin_entry_points/log.mli
+++ b/src/kernel_services/plugin_entry_points/log.mli
@@ -135,6 +135,7 @@ module type Messages = sig
type warn_category
(** Same as above, but for warnings
@since Chlorine-20180501
+ @plugin development guide
*)
val verbose_atleast : int -> bool
@@ -267,7 +268,9 @@ module type Messages = sig
In case the [wkey] is considered as a [Failure], the continution is not called.
This kind of message denotes a fatal error aborting Frama-C.
Notice that the [~emitwith] action is called iff a message is logged.
- @since 18.0-Argon *)
+ @since 18.0-Argon
+ @plugin development guide
+ *)
val register : kind -> (event -> unit) -> unit
(** Local registry for listeners. *)
@@ -343,6 +346,7 @@ module type Messages = sig
*)
val register_warn_category: string -> warn_category
+ (** @plugin development guide *)
val is_warn_category: string -> bool
@@ -362,6 +366,7 @@ module type Messages = sig
val get_all_warn_categories_status: unit -> (warn_category * warn_status) list
val set_warn_status: warn_category -> warn_status -> unit
+ (** @plugin development guide *)
val get_warn_status: warn_category -> warn_status
diff --git a/src/kernel_services/plugin_entry_points/plugin.mli b/src/kernel_services/plugin_entry_points/plugin.mli
index da7d795389d76899763eb37e2670329f8d149f15..a8fb8142af826e6db7b4aa0d3d31ea95372b3950 100644
--- a/src/kernel_services/plugin_entry_points/plugin.mli
+++ b/src/kernel_services/plugin_entry_points/plugin.mli
@@ -20,12 +20,14 @@
(* *)
(**************************************************************************)
+(** Plugin registration and general services.
+ @plugin development guide
+*)
(** Special signature for Kernel services, whose messages are handled in
an ad'hoc manner. Should not be of any use for a standard plug-in,
who would rather rely on {!Plugin.S} below.
@since Chlorine-20180501
- @plugin development guide
*)
module type S_no_log = sig
@@ -78,7 +80,7 @@ end
@since Beryllium-20090601-beta1
@modify Chlorine-20180501 removed programmatic access to [Debug_category]:
managing categories is now entirely done by Log.Messages
- @plugin development guide *)
+*)
module type S = sig
include Log.Messages
include S_no_log
diff --git a/src/kernel_services/visitors/visitor_behavior.mli b/src/kernel_services/visitors/visitor_behavior.mli
index 9e4adf0201f6d0745700fd4f6e2890144bea0bbe..273fb6189e542df940daf6eee1960a27da530225 100644
--- a/src/kernel_services/visitors/visitor_behavior.mli
+++ b/src/kernel_services/visitors/visitor_behavior.mli
@@ -50,7 +50,7 @@ val copy: Project.t -> t
val refresh: Project.t -> t
(** Makes fresh copies of the mutable structures and provides fresh id
- for the structures that have ids. Note that as for {!copy_visit}, only
+ for the structures that have ids. Note that as for {!copy}, only
varinfo that are declared in the scope of the visit will be copied and
provided with a new id.
*)
@@ -99,12 +99,16 @@ module type Get = sig
val enumitem: t -> enumitem -> enumitem
val typeinfo: t -> typeinfo -> typeinfo
val stmt: t -> stmt -> stmt
+ (** @plugin development guide *)
+
val logic_info: t -> logic_info -> logic_info
val logic_type_info: t -> logic_type_info -> logic_type_info
val fieldinfo: t -> fieldinfo -> fieldinfo
val model_info: t -> model_info -> model_info
val logic_var: t -> logic_var -> logic_var
val kernel_function: t -> kernel_function -> kernel_function
+ (** @plugin development guide *)
+
val fundec: t -> fundec -> fundec
end
@@ -187,6 +191,7 @@ module Set: Set
{!Cil_types.varinfo}: [Set_orig.varinfo vis vi new_original_repr].
@since 20.0-Calcium
+ @plugin development guide
*)
module Set_orig: Set
diff --git a/src/libraries/datatype/datatype.mli b/src/libraries/datatype/datatype.mli
index 34026478a1a927da4afaf3547b4eb8731d96f1a9..02bad2ddd43230e1ef09f63edfd530a27469c4fd 100644
--- a/src/libraries/datatype/datatype.mli
+++ b/src/libraries/datatype/datatype.mli
@@ -45,7 +45,10 @@ type 'a t = private
(** A type with its type value. *)
module type Ty = sig
type t
+ (** @plugin development guide *)
+
val ty: t Type.t
+ (** @plugin development guide *)
end
(** All values associated to a datatype, excepted [copy]. *)
@@ -66,7 +69,9 @@ module type S_no_copy = sig
(** List of representants of the descriptor. *)
val equal: t -> t -> bool
- (** Equality: same spec than [Stdlib.(=)]. *)
+ (** Equality: same spec than [Stdlib.(=)].
+ @plugin development guide
+ *)
val compare: t -> t -> int
(** Comparison: same spec than [Stdlib.compare]. *)
@@ -83,7 +88,9 @@ module type S_no_copy = sig
context in order to put parenthesis if required. See {!Type.par}. *)
val pretty: Format.formatter -> t -> unit
- (** Pretty print each value in an user-friendly way. *)
+ (** Pretty print each value in an user-friendly way.
+ @plugin development guide
+ *)
val varname: t -> string
(** A good prefix name to use for an OCaml variable of this type. Only useful
@@ -279,12 +286,18 @@ module type Hashtbl = sig
end
(** A datatype for a type [t] extended with predefined set, map and hashtbl
- over [t]. *)
+ over [t].
+
+ @plugin development guide
+*)
module type S_with_collections = sig
include S
module Set: Set with type elt = t
+ (** @plugin development guide *)
+
module Map: Map with type key = t
module Hashtbl: Hashtbl with type key = t
+ (** @plugin development guide *)
end
(** Generic comparable datatype builder: functions [equal], [compare] and
diff --git a/src/libraries/datatype/type.mli b/src/libraries/datatype/type.mli
index 0cc7b1ff57f7b15825f0d3d5345f128eb616e94d..f2d65db3c320c293209dafe9905047f1084a67a0 100644
--- a/src/libraries/datatype/type.mli
+++ b/src/libraries/datatype/type.mli
@@ -45,8 +45,8 @@ type 'a ty = 'a t
(** Precedences used for generating the minimal number of parenthesis in
combination with function {!par} below. *)
type precedence =
- | Basic (** @plugin development guide *)
- | Call (** @plugin development guide *)
+ | Basic (** Normal precedence @plugin development guide *)
+ | Call (** Instantiation of polymorphic type @plugin development guide *)
| Tuple
| List
| NoPar
diff --git a/src/libraries/project/project.mli b/src/libraries/project/project.mli
index 47d055df191824a5b9f2dd30413e873997d7a04b..0b607c99804252b227d5dc062e76376276b58787 100644
--- a/src/libraries/project/project.mli
+++ b/src/libraries/project/project.mli
@@ -208,6 +208,7 @@ val register_before_remove_hook: (t -> unit) -> unit
(* ************************************************************************* *)
exception IOError of string
+(** @plugin development guide *)
val save: ?selection:State_selection.t -> ?project:t -> Filepath.Normalized.t -> unit
(** Save a given project in a file. Default project is [current ()].
diff --git a/src/libraries/stdlib/FCHashtbl.mli b/src/libraries/stdlib/FCHashtbl.mli
index c890d905578e8a781730d37383b94b8b87718a1f..3fe0a74217bc8add3a933a5226ae458c6907c6a9 100644
--- a/src/libraries/stdlib/FCHashtbl.mli
+++ b/src/libraries/stdlib/FCHashtbl.mli
@@ -20,7 +20,10 @@
(* *)
(**************************************************************************)
-(** Extension of OCaml's [Hashtbl] module. *)
+(** Extension of OCaml's [Hashtbl] module.
+
+ @plugin development guide
+*)
(* No need to expand OCaml's [Hashtbl.S] here: we do not provide an alternative
implementation of [Hashtbl]. Hence, we will always be compatible with the
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index d8551183ffe17a263faf75b9e971f34c7c69fc2f..fff461b5b4c57a05323e6d044f3cce741c8e4969 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -225,7 +225,7 @@ val the: exn:exn -> 'a option -> 'a
@modify Magnesium-20151001 add optional argument [exn]
@modify 23.0-Vanadium optional argument [exn] now mandatory; otherwise,
use [Option.get], which is equivalent.
- @plugin development guide *)
+*)
val opt_hash: ('a -> int) -> 'a option -> int
(** @since Sodium-20150201 *)
diff --git a/src/plugins/gui/dgraph_helper.mli b/src/plugins/gui/dgraph_helper.mli
index a57f5fc064c3bf0f692d450434b7c868fb34a9c9..0dac7a9dc8a9e9f0b59e0e004c7f63a22957d4ed 100644
--- a/src/plugins/gui/dgraph_helper.mli
+++ b/src/plugins/gui/dgraph_helper.mli
@@ -20,6 +20,11 @@
(* *)
(**************************************************************************)
+(** Creation of windows for displaying graphs. Only available
+ for lablgtk2. In lablgtk3 mode, the window will only display a
+ text saying that the feature is not available.
+*)
+
(** Create a new window displaying a graph.
@plugin development guide *)
val graph_window:
diff --git a/src/plugins/gui/pretty_source.mli b/src/plugins/gui/pretty_source.mli
index a76f237f0cbcc4b53fea9d3bf7e6f9ce16b5beed..5880954f800a2a3940c4b32afca227cc54bb8b9e 100644
--- a/src/plugins/gui/pretty_source.mli
+++ b/src/plugins/gui/pretty_source.mli
@@ -36,7 +36,10 @@ type localizable = Printer_tag.localizable =
of the varinfo to distinguish between the various possibilities.
If the varinfo is a global or a local, the kernel_function is the
one in which the variable is declared. The [kinstr] argument is given
- for local variables with an explicit initializer. *)
+ for local variables with an explicit initializer.
+
+ @plugin development guide
+ *)
| PGlobal of global (** all globals but variable declarations and function
definitions. *)
| PIP of Property.t
diff --git a/src/plugins/pdg_types/pdgTypes.mli b/src/plugins/pdg_types/pdgTypes.mli
index e90bc536de1e7316d67addf4c4b3315a866a7426..ca007069dfb42b9b8dee808180aa84873ad72054 100644
--- a/src/plugins/pdg_types/pdgTypes.mli
+++ b/src/plugins/pdg_types/pdgTypes.mli
@@ -22,7 +22,7 @@
(** This module defines the types that are used to store the PDG of a
function.
- @plugin development guide *)
+*)
(** [Dpd] stands for 'dependence'. This object is used as a label on the edges
* of the PDG. There are three kinds of dependencies :
diff --git a/src/plugins/users/users_register.ml b/src/plugins/users/users_register.ml
index 40f1eb7c2d98cca4f390ac3296444570ecbc268d..742d0fd00fa1149cea6030880149fd6a19cb8a75 100644
--- a/src/plugins/users/users_register.ml
+++ b/src/plugins/users/users_register.ml
@@ -20,8 +20,6 @@
(* *)
(**************************************************************************)
-(** @plugin development guide *)
-
include
Plugin.Register
(struct
@@ -30,7 +28,6 @@ include
let help = "function callees"
end)
-(** @plugin development guide *)
module ForceUsers =
False
(struct
diff --git a/src/plugins/value/engine/analysis.mli b/src/plugins/value/engine/analysis.mli
index ae7383efe459843611c1b59a0001c1065d0f8ccc..99fa1e27592fd03fa534e3473545852e7f6a656b 100644
--- a/src/plugins/value/engine/analysis.mli
+++ b/src/plugins/value/engine/analysis.mli
@@ -88,7 +88,9 @@ val compute : unit -> unit
@plugin development guide *)
val is_computed : unit -> bool
-(** Return [true] iff the Eva analysis has been done. *)
+(** Return [true] iff the Eva analysis has been done.
+ @plugin development guide
+*)
val self : State.t
(** Internal state of Eva analysis from projects viewpoint. *)
diff --git a/src/plugins/value_types/cilE.mli b/src/plugins/value_types/cilE.mli
index a32fc59c506ef02be93f94870f4b9d21428b44e9..86e8be09466080f90986feb9d3c04ff26e34047c 100644
--- a/src/plugins/value_types/cilE.mli
+++ b/src/plugins/value_types/cilE.mli
@@ -20,8 +20,7 @@
(* *)
(**************************************************************************)
-(** Value analysis alarms
- @plugin development guide *)
+(** Value analysis alarms *)
(* ************************************************************************* *)
(* [JS 2011/03/11] All the below stuff manage warnings of the value analysis