From 08dfecc4113ef401e1995301fddc05639a0f6261 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 25 Mar 2024 11:02:52 +0100
Subject: [PATCH] [wp] rename wp_nullable_args ext - wp_nullable_args ->
nullable_args - also changes documentation for strategies
---
src/plugins/wp/RefUsage.ml | 2 +-
src/plugins/wp/doc/manual/nullable.c | 2 +-
src/plugins/wp/doc/manual/wp_plugin.tex | 6 +++---
src/plugins/wp/tests/wp_plugin/nullable_ext.c | 14 +++++++-------
4 files changed, 12 insertions(+), 12 deletions(-)
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index d34ad61347c..1771bbd362d 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -852,7 +852,7 @@ struct
let () =
Acsl_extension.register_behavior ~plugin:"wp"
- "wp_nullable_args" Nullable_extension.typer false
+ "nullable_args" Nullable_extension.typer false
module HasNullable =
State_builder.Option_ref(Datatype.Bool)
diff --git a/src/plugins/wp/doc/manual/nullable.c b/src/plugins/wp/doc/manual/nullable.c
index 9b403ffe91c..f84f31d995e 100644
--- a/src/plugins/wp/doc/manual/nullable.c
+++ b/src/plugins/wp/doc/manual/nullable.c
@@ -3,7 +3,7 @@ void foo(int* p /*@ wp_nullable */, int* q /*@ wp_nullable */){
}
// or equivalently:
-//@ wp_nullable_args p, q ;
+//@ \wp::nullable_args p, q ;
void foo(int* p, int* q){
}
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 8c6f6ae198d..f7c53c749ba 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -1919,12 +1919,12 @@ The syntax of ACSL extensions for proof strategies is defined below:
\begin{center}
\begin{tabular}{l}
- \verb+@strategy+ \textit{name}\,: \\
+ \verb+@\wp::strategy+ \textit{name}\,: \\
\quad\quad\textit{alternative}\,, \\
\quad\quad\ldots, \\
\quad\quad\textit{alternative}\,; \\
\\
- \verb+@proof+ \textit{name}\,: \textit{target}\pdots\textit{target}\,;
+ \verb+@\wp::proof+ \textit{name}\,: \textit{target}\pdots\textit{target}\,;
\end{tabular}
\end{center}
@@ -2051,7 +2051,7 @@ name to the strategies to use:
\begin{center}
\begin{tabular}{l}
- \verb+@proof+ \textit{strategy}\,: smoke,\textit{target}\pdots\textit{target}\,;
+ \verb+@\wp::proof+ \textit{strategy}\,: smoke,\textit{target}\pdots\textit{target}\,;
\end{tabular}
\end{center}
diff --git a/src/plugins/wp/tests/wp_plugin/nullable_ext.c b/src/plugins/wp/tests/wp_plugin/nullable_ext.c
index aac3f9c4781..830970f30e0 100644
--- a/src/plugins/wp/tests/wp_plugin/nullable_ext.c
+++ b/src/plugins/wp/tests/wp_plugin/nullable_ext.c
@@ -17,7 +17,7 @@ int x;
int *g;
/*@ assigns *g, *p, x ;
- \wp::wp_nullable_args p ;
+ \wp::nullable_args p ;
*/
void nullable_coherence(int *p) {
if (p == (void *)0) {
@@ -31,7 +31,7 @@ void nullable_coherence(int *p) {
}
/*@ assigns *p, *q, *r, *s, *t ;
- \wp::wp_nullable_args p, q, r ;
+ \wp::nullable_args p, q, r ;
*/
void nullable_in_context(int *p, int *q, int *r, int *s, int *t) {
*p = 42;
@@ -41,35 +41,35 @@ void nullable_in_context(int *p, int *q, int *r, int *s, int *t) {
}
/*@ assigns *ptr ;
- \wp::wp_nullable_args ptr ;
+ \wp::nullable_args ptr ;
*/
void with_declaration(int *ptr);
void with_declaration(int *ptr) {}
#ifdef FAIL_1
/*@ assigns *ptr ;
- \wp::wp_nullable_args unexisting_ptr ;
+ \wp::nullable_args unexisting_ptr ;
*/
void fails_no_variable(int *ptr) {}
#endif
#ifdef FAIL_2
/*@ assigns *ptr ;
- \wp::wp_nullable_args *ptr ;
+ \wp::nullable_args *ptr ;
*/
void not_a_variable(int *ptr) {}
#endif
#ifdef FAIL_3
/*@ assigns *ptr ;
- \wp::wp_nullable_args g ;
+ \wp::nullable_args g ;
*/
void not_a_formal(int *ptr) {}
#endif
#ifdef FAIL_4
/*@ assigns x ;
- \wp::wp_nullable_args f ;
+ \wp::nullable_args f ;
*/
void not_a_pointer(int f) {}
#endif
--
GitLab