Commit d069cd2d authored by Allan Blanchard's avatar Allan Blanchard

Apply suggestion to src/plugins/wp/doc/manual/wp_plugin.tex

parent 64347a62
......@@ -901,7 +901,7 @@ int caller(int (*fp)(int)){
}
\end{lstlisting}
generates two goals for \verb+POST+, one for call to \verb+f1+ and
These annotations split post-conditions to the dynamic call into two sub-goals: one for call to \verb+f1+ and
a second for the call to \verb+f2+. A last goal is generated at the call
site: one must prove that \verb+fp+ is either \verb+f1+ or \verb+f2+.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment