Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
ff9a8541
Commit
ff9a8541
authored
1 year ago
by
Allan Blanchard
Committed by
Loïc Correnson
1 year ago
Browse files
Options
Downloads
Patches
Plain Diff
[wp] typos in doc
parent
e39edd8a
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/plugins/wp/doc/manual/wp_plugin.tex
+4
-4
4 additions, 4 deletions
src/plugins/wp/doc/manual/wp_plugin.tex
with
4 additions
and
4 deletions
src/plugins/wp/doc/manual/wp_plugin.tex
+
4
−
4
View file @
ff9a8541
...
@@ -1504,7 +1504,7 @@ generation can be identified by the \verb$"counterexamples"$ variant after their
...
@@ -1504,7 +1504,7 @@ generation can be identified by the \verb$"counterexamples"$ variant after their
name. For example, in the prover selection example above,
\verb
+
cvc4-ce
+
and
name. For example, in the prover selection example above,
\verb
+
cvc4-ce
+
and
\verb
+
z3-ce
+
are such provers.
\verb
+
z3-ce
+
are such provers.
To
activat
e counter examples generation by
\textsf
{
WP
}
you shall use
To
enabl
e counter examples generation by
\textsf
{
WP
}
you shall use
\verb
+
-wp-counter-examples
+
option. Then, for each selected solver that has a
\verb
+
-wp-counter-examples
+
option. Then, for each selected solver that has a
counter-examples variant, this variant will be used instead and counter-examples
counter-examples variant, this variant will be used instead and counter-examples
will be asked to the solver in case of unknown result. Notice that you can also
will be asked to the solver in case of unknown result. Notice that you can also
...
@@ -1528,7 +1528,7 @@ A proof obligation for which a counter-example has been generated is reported by
...
@@ -1528,7 +1528,7 @@ A proof obligation for which a counter-example has been generated is reported by
Unknown: 1
Unknown: 1
\end{shell}
\end{shell}
Notice that cache usage is d
eactivat
ed for provers asked to generate a
Notice that cache usage is d
isabl
ed for provers asked to generate a
counter-example, since models are currently not stored in
\textsf
{
WP
}
's
counter-example, since models are currently not stored in
\textsf
{
WP
}
's
cache
\footnote
{
This feature might be added in future versions of the plugin.
}
.
cache
\footnote
{
This feature might be added in future versions of the plugin.
}
.
...
@@ -1540,7 +1540,7 @@ wrong, although they might not be \emph{sufficient} in practice.
...
@@ -1540,7 +1540,7 @@ wrong, although they might not be \emph{sufficient} in practice.
Generated models are reported by
\textsf
{
WP
}
along with prover results when
Generated models are reported by
\textsf
{
WP
}
along with prover results when
either
\verb
+
-wp-print
+
or
\verb
+
-wp-status
+
options are used. The interactive
either
\verb
+
-wp-print
+
or
\verb
+
-wp-status
+
options are used. The interactive
proof transformer (
\textsf
{
TIP
}
) also display models in the graphical user
proof transformer (
\textsf
{
TIP
}
) also display
s
models in the graphical user
interface, when available.
interface, when available.
Probes are generalization of variables. They are named expressions for which the
Probes are generalization of variables. They are named expressions for which the
...
@@ -1618,7 +1618,7 @@ is activated. For instance, in the previous example:
...
@@ -1618,7 +1618,7 @@ is activated. For instance, in the previous example:
\noindent
\noindent
Summary of
\textsf
{
WP
}
options related to probes and counter-examples generation:
Summary of
\textsf
{
WP
}
options related to probes and counter-examples generation:
\begin{description}
\begin{description}
\item
[\tt -wp-(no)-counter-examples]
activat
es counter examples generation for
\item
[\tt -wp-(no)-counter-examples]
enabl
es counter examples generation for
supporting provers. Also generate probes for formal parameters of functions
supporting provers. Also generate probes for formal parameters of functions
and universal quantifiers of lemmas. Not set by default.
and universal quantifiers of lemmas. Not set by default.
\item
[\tt -wp-print, -wp-status]
pretty-prints the probes and the associated models,
\item
[\tt -wp-print, -wp-status]
pretty-prints the probes and the associated models,
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment