From bb99bdf39a9c8e899a8bad312588432b6725a7c5 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Tue, 8 Jun 2021 14:07:20 +0200
Subject: [PATCH] [WP] adds doc of -wp-frama-c-stdlib-terminate
---
src/plugins/wp/doc/manual/wp_plugin.tex | 3 +++
1 file changed, 3 insertions(+)
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 4d005251d80..997f869dcea 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -977,6 +977,9 @@ weakest precondition calculus.
it is generally not necessary and it can generates a large number of
verifications for structures with many (nested) fields. \texttt{-1} enables
full unfolding.
+\item[\tt -wp-(no)-frama-c-stdlib-terminate] Frama-C libc functions without
+ \texttt{terminates} specification are considered to terminate when called
+ (default is: \texttt{no}).
\item[\tt -wp-(no)-declarations-terminate] Undefined external functions without
\texttt{terminates} specification are considered to terminate when called
(default is: \texttt{no}).
--
GitLab