diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml index d34ad61347c88f5561733c339655c8c4aa94c39f..1771bbd362d21f6183d4894843c15927723cf101 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 9b403ffe91cb9148bcff3b461de90cec89c09cb1..f84f31d995e3cf5d197737e171c58e00b9739083 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 8c6f6ae198dd42769f4294a21206d70ea4c03b79..f7c53c749ba7ba2e1ab7f87961b239d7aef9bbec 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 aac3f9c478127075782514f9bef34c73c8fa4a34..830970f30e01ed34f43b75582c3a32d9e3b99fee 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