Skip to content
Snippets Groups Projects
Commit 89b2eba7 authored by Thibault Martin's avatar Thibault Martin Committed by Allan Blanchard
Browse files

[doc] Fix some typos, indent code

parent e32b56f3
No related branches found
No related tags found
No related merge requests found
...@@ -3814,7 +3814,7 @@ When the default behavior is missing in a function contract but needed by either ...@@ -3814,7 +3814,7 @@ When the default behavior is missing in a function contract but needed by either
\scodeidxdef{Populate\_spec}{populate\_funspec} as follows: \scodeidxdef{Populate\_spec}{populate\_funspec} as follows:
\begin{ocamlcode} \begin{ocamlcode}
Populate_spec.populate_funspec ~do_body:true kf [`Exits; `Assigns] Populate_spec.populate_funspec ~do_body:true kf [`Exits; `Assigns]
\end{ocamlcode} \end{ocamlcode}
This code will generate specifications for the function \verb+kf+ using the This code will generate specifications for the function \verb+kf+ using the
...@@ -3836,28 +3836,28 @@ a customized mode. For this, we need to define generation functions for each ...@@ -3836,28 +3836,28 @@ a customized mode. For this, we need to define generation functions for each
clause: clause:
\begin{ocamlcode} \begin{ocamlcode}
(* Generate exits \false clauses. *) (* Generate exits \false clauses. *)
let gen_exits _ _ = let gen_exits _ _ =
[ Exits, Logic_const.(new_predicate pfalse) ] [ Exits, Logic_const.(new_predicate pfalse) ]
(* Generate assigns for prototypes. *) (* Generate assigns for prototypes. *)
let gen_assigns kf _ = let gen_assigns kf _ =
if Kernel_function.has_definition kf then if Kernel_function.has_definition kf then
WritesAny WritesAny
else Writes (Infer_assigns.from_prototype kf) else Writes (Infer_assigns.from_prototype kf)
(* Do not generate requires. *) (* Do not generate requires. *)
let gen_requires _ _ = [ ] let gen_requires _ _ = [ ]
(* Do not generate allocates. *) (* Do not generate allocates. *)
let gen_allocates _ _ = FreeAllocAny let gen_allocates _ _ = FreeAllocAny
(* Do not generate terminates. *) (* Do not generate terminates. *)
let gen_terminates _ _ = None let gen_terminates _ _ = None
(* Property status to be emitted for the generated clauses. *) (* Property status to be emitted for the generated clauses. *)
let status_exits = Property_status.Dont_know let status_exits = Property_status.Dont_know
let status_assigns = Property_status.True let status_assigns = Property_status.True
\end{ocamlcode} \end{ocamlcode}
Each function takes 2 parameters: Each function takes 2 parameters:
...@@ -3877,23 +3877,23 @@ Then we need to register the mode using \verb+Populate_spec.register+% ...@@ -3877,23 +3877,23 @@ Then we need to register the mode using \verb+Populate_spec.register+%
\begin{ocamlcode} \begin{ocamlcode}
let create_mode () = let create_mode () =
Populate_spec.register Populate_spec.register
~gen_exits ~status_exits ~gen_exits ~status_exits
~gen_assigns ~status_assigns ~gen_assigns ~status_assigns
~gen_requires ~gen_requires
~gen_allocates ~gen_allocates
~gen_terminates ~gen_terminates
"mymode" "mymode"
\end{ocamlcode} \end{ocamlcode}
This function registers a new mode \verb+mymode+ which can be selected using This function registers a new mode \verb+mymode+ which can be selected using
command line options \verb+-generated-spec-mode mymode+. All parameters are command line options \verb+-generated-spec-mode mymode+. All parameters are
optionnals and, if a generation function is left unspecified, \verb+Frama_C+ optional and, if a generation function is left unspecified, \verb+Frama_C+ mode
mode (see the user manual~\cite{userman}) will be used instead to generate the (see the user manual~\cite{userman}) will be used instead to generate the
corresponding clauses (emits a warning). It is also possible to specify a corresponding clauses (emits a warning). It is also possible to specify a
property status\codeidx{Property\_status} to be emitted when a clause is property status\codeidx{Property\_status} to be emitted when a clause is
generated (emits a warning if omitted). Requires is the only clause for which it generated (emits a warning if omitted). Requires are the only clause for which
is not possible to specify a status, because it is not possible to specify a status, because
\texttt{Populate\_spec}\codeidx{Populate\_spec} will never try to emit status of \texttt{Populate\_spec}\codeidx{Populate\_spec} will never try to emit status of
requires. requires.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment