Merge branch 'fix/virgile/ptests-arobase' into 'master'

@ in ptests and other fixes

See merge request frama-c/frama-c!2180

doc/developer/Makefile

@@ -49,7 +49,7 @@ else
 		-load-script ./examples/acsl_extension \
 		-load-script ./hello_world/hello_world.ml \
        | tee check.log
-	if grep -e "user error" check.log; then \
+	if grep -e "User Error" check.log; then \
            echo "Examples script do not compile with current Frama-C."; \
            echo "Please examine check.log and make appropriate changes"; \
            exit 1; \

doc/developer/advance.tex

@@ -1062,8 +1062,8 @@ or
   line. Once such a directive has been encountered, each occurrence of
   \texttt{@macro-name@} in a \texttt{CMD}, \texttt{LOG}, \texttt{OPT},
   \texttt{STDOPT} or \texttt{EXECNOW} directive at this configuration level
-  or in any level below it will be replaced by \texttt{content}. Existing 
-  pre-defined macros are listed in section~\ref{sec:ptests-macros}.
+  or in any level below it will be replaced by \texttt{content}. Existing
+  pre-defined macros are listed in section~\ref{sec:ptests-macros}. 
 \item The \texttt{FILEREG}\sscodeidxdef{Test}{Directive}{FILEREG}
   directive contains a regular expression indicating which files in
   the directory containing the current test suite are actually part of
@@ -1072,6 +1072,14 @@ or
   configuration file.
 \end{itemize}
 
+\begin{important}
+\paragraph{\texttt{@} in the text of a directive}
+As mentioned above, \texttt{@} is recognized by \ptests as the beginning of
+a macro. If you need to have a literal \texttt{@} in the text of the directive
+itself, it needs to be doubled, {\it i.e.} \texttt{@@} will be translated as
+\texttt{@}.
+\end{important}
+
 \begin{important}
   \textbf{Summary: ordering of test executions}
 
@@ -3918,7 +3926,7 @@ the corresponding list is traversed normally by the visitor
 (see section~\ref{adv:visitors}).
 
 In order for the extension to be recognized by the parser, it must be
-registered by one of the following functions, depending on its category:
+registered by one of the following functions, depending on its category.
 \begin{itemize}
 \item \texttt{Logic\_typing.register\_behavior\_extension}%
 \scodeidx{Logic\_typing}{register\_behavior\_extension}
@@ -3933,6 +3941,15 @@ registered by one of the following functions, depending on its category:
 \item \texttt{Logic\_typing.register\_code\_annot\_next\_both\_extension}%
 \scodeidx{Logic\_typing}{register\_code\_annot\_next\_loop\_extension}
 \end{itemize}
+
+Each function takes three arguments:
+\begin{itemize}
+\item \texttt{kw} the name of the extension,
+\item \texttt{status}, a boolean flag indicating whether the extended annotation
+  may have a validity status, and
+\item \texttt{f} the type-checking function itself.
+\end{itemize}
+
 After a call to the appropriate registration function,
 a clause of the form \verb|kw e1,...,en;|, where each \verb|ei| can be
 any syntactically valid ACSL term or predicate,

doc/developer/changes.tex

@@ -7,6 +7,12 @@ This chapter summarizes the major changes in this documentation between each
 
 \section*{Frama-C+dev}
 \begin{itemize}
+\item \textbf{ACSL Extension}: Document new \texttt{status} flag for registration functions
+\item \textbf{Testing}: Document of usage \texttt{@@} in a directive
+\end{itemize}
+
+\section*{18.0 Argon}
+\begin{itemize}
 \item \textbf{Logging Services}: Document \texttt{error} and \texttt{failure} behaviors.
 \item \textbf{ACSL Extensions}: New extension categories, for global and plain code annotations
 \end{itemize}

doc/developer/examples/acsl_extension.ml

@@ -14,4 +14,4 @@ let type_foo ~typing_context ~loc:_loc l =
   in
   Ext_terms res
 
-let () = Logic_typing.register_behavior_extension "foo" type_foo
+let () = Logic_typing.register_behavior_extension "foo" false type_foo

ptests/ptests.ml

@@ -493,7 +493,7 @@ end = struct
 
 end
 
-let macro_regex = Str.regexp "\\([^@]*\\)@\\([^@]+\\)@\\(.*\\)"
+let macro_regex = Str.regexp "\\([^@]*\\)@\\([^@]*\\)@\\(.*\\)"
 
 type execnow =
     {
@@ -585,15 +585,19 @@ let replace_macros macros s =
       let rest = Str.matched_group 3 s in
       let new_n = Str.group_end 1 in
       let n, new_s =
-        try
-          if !verbosity >= 2 then lock_printf "macro is %s\n%!" macro;
-          let replacement =  StringMap.find macro macros in
-          if !verbosity >= 1 then
-            lock_printf "replacement for %s is %s\n%!" macro replacement;
-          new_n,
-          String.sub s 0 n ^ start ^ replacement ^ rest
-        with
+        if macro = "" then begin
+          new_n + 1, String.sub s 0 new_n ^ "@" ^ rest
+        end else begin
+          try
+            if !verbosity >= 2 then lock_printf "macro is %s\n%!" macro;
+            let replacement =  StringMap.find macro macros in
+            if !verbosity >= 1 then
+              lock_printf "replacement for %s is %s\n%!" macro replacement;
+            new_n,
+            String.sub s 0 n ^ start ^ replacement ^ rest
+          with
           | Not_found -> Str.group_end 2 + 1, s
+        end
       in
        if !verbosity >= 2 then lock_printf "new string is %s\n%!" new_s;
       let new_acc = ptest_file_matched, new_s in

src/kernel_services/ast_queries/logic_typing.mli

@@ -172,6 +172,7 @@ type typing_context = {
 
     @since Carbon-20101201
     @modify Silicon-20161101 change type of the function
+    @Frama-C+dev add [status] argument
 *)
 val register_behavior_extension:
   string -> bool ->

tests/rte/twofunc3.c

 /* run.config
    EXECNOW: make -s @PTEST_DIR@/rte_api/rte_get_annot.cmxs
-   OPT: -load-module @PTEST_DIR@/rte_api/rte_get_annot -journal-disable
+   OPT: -rte-select @@all -load-module @PTEST_DIR@/rte_api/rte_get_annot -journal-disable
 */