diff --git a/Makefile b/Makefile
index 5136dd9a8b93c557310c9baea7309210b55371ed..cdfca959234201f053bf2b2cd8d43978fc1c3c56 100644
--- a/Makefile
+++ b/Makefile
@@ -543,6 +543,7 @@ KERNEL_CMO=\
src/kernel_internals/parsing/logic_parser.cmo \
src/kernel_internals/parsing/logic_lexer.cmo \
src/kernel_services/ast_queries/logic_typing.cmo \
+ src/kernel_services/ast_queries/acsl_extension.cmo \
src/kernel_services/ast_queries/ast_info.cmo \
src/kernel_services/ast_data/ast.cmo \
src/kernel_services/ast_printing/cprint.cmo \
diff --git a/doc/developer/Makefile b/doc/developer/Makefile
index 4ce9e948e29de1c21f184f401c6168901f8de54d..12024d9005f101707df599f64955cbf3667f252b 100644
--- a/doc/developer/Makefile
+++ b/doc/developer/Makefile
@@ -46,7 +46,8 @@ else
-load-script ./examples/syntactic_check \
-load-script ./examples/callstack \
-load-script ./examples/use_callstack \
- -load-script ./examples/acsl_extension \
+ -load-script ./examples/acsl_extension_foo \
+ -load-script ./examples/acsl_extension_ext_types \
-load-script ./hello_world/hello_world.ml \
| tee check.log
if grep -e "User Error" check.log; then \
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 0a09948afd525477b4a2d0fd41cf79db3fb990de..b92bf5c08af89d2787a2f28c09872cc0d19840cc 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -3917,6 +3917,30 @@ An extension is characterized by its introducing keyword \texttt{kw}, or \texttt
extension. It is not possible to have the same keyword for two distinct extensions, especially if
they belong to different categories, as this would lead to ambiguities in the parser.
+Once an extension is registered a clause of the form \verb|kw e1,...,en;|, where each \verb|ei| can be
+any syntactically valid ACSL term or predicate, will be treated by the parser as belonging to the
+extension \verb|kw|.
+
+Contract extension clauses must occur after \verb|assumes| and \verb|requires| clauses if any, but
+can be freely mixed with other behavior clauses (post-conditions, \verb|assigns|, \verb|frees| and
+\verb|allocates|).
+
+Similarly, in a loop annotation, \verb|loop kw e1, ..., en;| will be treated as belonging to the
+\verb|kw| extension. In case the loop annotation has a \verb|loop variant|, the extension must
+occur before. Otherwise, there is no ordering constraint with other loop annotations clauses.
+
+Global extensions can appear either alone in a global annotation, or as part of an axiomatic with
+a set of other global annotations.
+
+Finally, a code annotation extension must appear as a single code annotation, like any code annotation.
+
+Code (and loop) extensions can be made specific to a
+set of existing behaviors using the standard ACSL \verb|for| construction.
+Namely, \verb|for bhv: loop kw e1, ..., en;| will indicate that the
+(loop) extension is supposed to be considered only when behavior \verb|bhv| is
+active (although it is ultimately up to the plugin to decide what to do with
+this information).
+
An \texttt{acsl\_extension}\scodeidx{Cil\_types}{acsl\_extension} is a triple
\texttt{(id, kw, ext)} where \texttt{id} is its unique ID, used in annotation tables and generated
by \scodeidx{Logic\_const}{new\_acsl\_extension}\texttt{Logic\_const.new\_acsl\_extension},
@@ -3940,75 +3964,48 @@ the corresponding list is traversed normally by the visitor
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.
\begin{itemize}
-\item \texttt{Logic\_typing.register\_behavior\_extension}%
-\scodeidx{Logic\_typing}{register\_behavior\_extension}
-\item \texttt{Logic\_typing.register\_global\_extension}%
-\scodeidx{Logic\_typing}{register\_global\_extension}
-\item \texttt{Logic\_typing.register\_code\_annot\_extension}%
-\scodeidx{Logic\_typing}{register\_code\_annot\_extension}
-\item \texttt{Logic\_typing.register\_code\_annot\_next\_stmt\_extension}%
-\scodeidx{Logic\_typing}{register\_code\_annot\_next\_stmt\_extension}
-\item \texttt{Logic\_typing.register\_code\_annot\_next\_loop\_extension}%
-\scodeidx{Logic\_typing}{register\_code\_annot\_next\_both\_extension}
-\item \texttt{Logic\_typing.register\_code\_annot\_next\_both\_extension}%
-\scodeidx{Logic\_typing}{register\_code\_annot\_next\_loop\_extension}
+\item \texttt{Acsl\_extension.register\_behavior}%
+\scodeidx{Acsl\_extension}{register\_behavior}
+\item \texttt{Acsl\_extension.register\_global}%
+\scodeidx{Acsl\_extension}{register\_global}
+\item \texttt{Acsl\_extension.register\_code\_annot}%
+\scodeidx{Acsl\_extension}{register\_code\_annot}
+\item \texttt{Acsl\_extension.register\_code\_annot\_next\_stmt}%
+\scodeidx{Acsl\_extension}{register\_code\_annot\_next\_stmt}
+\item \texttt{Acsl\_extension.register\_code\_annot\_next\_loop}%
+\scodeidx{Acsl\_extension}{register\_code\_annot\_next\_both}
+\item \texttt{Acsl\_extension.register\_code\_annot\_next\_both}%
+\scodeidx{Acsl\_extension}{register\_code\_annot\_next\_loop}
\end{itemize}
-Each function takes three arguments:
+Each function takes the following mandatory 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,
-will be treated by the parser
-as belonging to the extension \verb|kw|. Contract extension clauses must occur after
-\verb|assumes| and \verb|requires| clauses if any, but can be freely
-mixed with other behavior clauses (post-conditions, \verb|assigns|,
-\verb|frees| and \verb|allocates|).
-
-Similarly, in a loop annotation,
-\verb|loop kw e1, ..., en;| will be treated as belonging to the \verb|kw|
-extension. In case the loop annotation has a \verb|loop variant|, the
-extension must occur before. Otherwise, there is no ordering constraint with
-other loop annotations clauses.
-
-Global extensions can appear either alone in a global annotation, or as part of an axiomatic with
-a set of other global annotations.
-
-Finally, a code annotation extension must appear as a single code annotation, like any code annotation.
+\item \texttt{typer} the type-checking function itself.
+\item \texttt{status}, a boolean flag indicating whether the extended
+ annotation may have a validity status, and
-Code (and loop) extensions can be made specific to a
-set of existing behaviors using the standard ACSL \verb|for| construction.
-Namely, \verb|for bhv: loop kw e1, ..., en;| will indicate that the
-(loop) extension is supposed to be considered only when behavior \verb|bhv| is
-active (although it is ultimately up to the plugin to decide what to do with
-this information).
+\end{itemize}
-During type-checking,
-the list \verb|[e1;...;en]| will be given to \verb|f|, together
-with the current typing environment (which allows discriminating
+During type-checking, the list \verb|[e1;...;en]| will be given to \verb|typer|,
+together with the current typing environment (which allows discriminating
between contract and loop extensions and will have the appropriate logic labels
-set in the local environment). \verb|f| must return the corresponding
+set in the local environment). \verb|typer| must return the corresponding
\verb|acsl_extension_kind| (possibly adding an entry for key \verb|id|
in an internal table if it chooses to return \verb|Ext_id id|).
-The first argument of \verb|f| is a \verb|Logic_typing.typing_context|%
-\scodeidx{Logic\_typing}{typing\_context}
-which provides lookup functions for the various kinds of identifiers that are
-present in the environment, as well as extensible type-checking functions for
-predicates, terms, and assigns clauses. Indeed, these functions take themselves
-as argument a \verb|typing_context| \verb|ctxt| and will use the functions
-of \verb|ctxt| to type-check the children of the current node. Extensions
-can take advantage of this open recursion to recognize only subtrees of an
-otherwise normal ACSL predicate or term. For instance, the following code will
-let extension \verb|foo| replace all occurrences of \verb|\foo| by \verb|42|.
+The first argument of \verb|typer| is a \verb|Logic_typing.typing_context|%
+\scodeidx{Logic\_typing}{typing\_context} which provides lookup functions for the
+various kinds of identifiers that are present in the environment, as well as
+extensible type-checking functions for predicates, terms, and assigns clauses.
+Indeed, these functions take themselves as argument a \verb|typing_context|
+\verb|ctxt| and will use the functions of \verb|ctxt| to type-check the children
+of the current node. Extensions can take advantage of this open recursion to
+recognize only subtrees of an otherwise normal ACSL predicate or term. For
+instance, the following code will let extension \verb|foo| replace all
+occurrences of \verb|\foo| by \verb|42|.
-\ocamlinput{./examples/acsl_extension.ml}
+\ocamlinput{./examples/acsl_extension_foo.ml}
With this extension enabled, \framac will interpret the following clause in
a given source file:
@@ -4020,32 +4017,93 @@ as the following type-checked AST fragment:
/*@ foo 84 == 42 + 42; */
\end{lstlisting}
-If all the information of the extended clause is contained in
-the predicate list \verb|preds|, no other registration is needed beyond
-the parsing and type-checking: the pretty-printer will output \verb|preds|
-as a comma-separated list preceded by \verb|kw| (or \verb|loop kw| if
-the extension is a loop annotation), and the visitor will traverse
-each \verb|preds| as well as any predicate present in the AST. However, if
-some information is present in the internal state of the plugin, two more
-functions may be required for pretty-printing and visiting the extending
-clause respectively.
-
-First,
-\texttt{Cil\_printer.register\_behavior\_extension}%
-\scodeidx{Cil\_printer}{register\_behavior\_extension}
-registers a new pretty-printer \verb|pp| for a given extension \verb|kw|.
-Together with the \verb|acsl_extension_kind| of the extended clause,
-\verb|pp| is given the current pretty-printer and the formatter where to
-output the result.
-
-Second,
-\texttt{Cil.register\_behavior\_extension}%
-\scodeidx{Cil}{register\_behavior\_extension}
-registers a custom visitor \verb|vext| for a given extension \verb|kw|.
-\verb|vext| is given the content of the extended clause and the current
-visitor, and must return a \texttt{Cil.visitAction}
-(if all the information is in the plugin's own table, it can
-return \texttt{SkipChildren}).
+If the extended clause is of kind \verb|Ext_preds l| or \verb|Ext_terms l|,
+and all the information of the extension is contained in the list \verb|l|,
+no function other than the typing function needs to be registered. The parsing
+will use the standard way to parse untyped predicates and terms. After
+typing, the visitor will traverse each element of \verb|l| as well as any
+predicate or term present in the AST. The pretty-printer will output these
+elements as a comma-separated list preceded by \verb|kw| (or \verb|loop kw| if
+the extension is a loop annotation).
+
+However, depending on the situation, the following optional functions can be
+provided to the registration function in order to modify how ACSL extensions
+are handled by Frama-C:
+
+\begin{itemize}
+\item \texttt{preprocessor} a transformer to apply on the untyped term or
+ predicate read during the parsing phase,
+\item \texttt{visitor} the visitor function to be applied when visiting
+ the extension,
+\item \texttt{printer} the pretty-printing function associated to the
+ extension,
+\item \texttt{short\_printer} a function used to provide a brief textual
+ representation of an extension.
+\end{itemize}
+
+The \verb|preprocessor| function is applied just after parsing the extension
+terms. It takes the list of untyped terms or predicates and can either return
+the same list (but reading it to do some stuff) or return a new list. By
+default, this function is the identity.
+
+The \verb|visitor| function is used by the Frama-C visitors. It takes the
+current visitor, together with the \verb|acsl_extension_kind| of the extended
+clause and must returns a \verb|Cil.visitAction|. By default, this function
+just returns \verb|Cil.DoChildren|.
+
+The \verb|printer| function is used by the \verb|Cil_printer.pp_extended|
+function. It takes the current pretty-printer, the formatter, together with
+the \verb|acsl_extension_kind| of the extended clause. By default, it prints
+the list of terms or predicates if the kind is \verb|Ext_preds l| or
+\verb|Ext_terms l|. If the kind is \verb|Ext_id i|, it only prints the
+integer \verb|i|.
+
+The \verb|short_printer| function is a function that can be useful for
+debugging or user-feedback. As an alternative to \verb|Cil_printer.pp_extended|,
+the \verb|Cil_printer.pp_short_extended| can be used to get brief description
+of the content of the extension. It is for example used by the GUI to get
+a more informative name for the extension in the file tree. By default, it
+does not print anything about the content of the extension, so that the
+result is \verb|"kwd"| or \verb|"loop kwd"|.
+
+When the extension kind is \verb|Ext_id|, it is common that the plugin
+defining the extension contains a table that associates some data to this
+identifier. In such a case, a \verb|printer| might be needed to reconstruct
+the source code from the data so that a pretty printed code can be parsed
+again. For the same reason, an extension that registers a \verb|preprocessor|
+that modifies the AST should probably register a \verb|printer| to recover
+the original content.
+
+It is also common, when the kind is \verb|Ext_id|, to define a particular
+visitor for the extension, either to ignore the content of the extension as
+it is in an internal table of the plugin (thus returning a \verb|SkipChildren|
+action) or, on the opposite, to give the possibility to a user defined visitor
+to get an access to this content.
+
+The following code shows a more complete extension example. It provides the
+user a way to load some types (assumed to be external to Frama-C) so that they
+can be used in ACSL specification.
+
+\ocamlinput{./examples/acsl_extension_ext_types.ml}
+
+Namely, specification:
+
+\begin{lstlisting}[language=C,alsolanguage=ACSL]
+/*@ ext_type load: foo ; */
+/*@
+ axiomatic Pred {
+ predicate P(foo f) reads \nothing ;
+ }
+*/
+/*@ lemma X: \forall foo f ; P(f) ; */
+\end{lstlisting}
+
+is correctly parsed and typed by Frama-C and leads to the following displayed
+version in the interface:
+
+\includegraphics[width=\textwidth]{examples/acsl_extension_ext_types}
+
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/doc/developer/examples/acsl_extension_ext_types.ml b/doc/developer/examples/acsl_extension_ext_types.ml
new file mode 100644
index 0000000000000000000000000000000000000000..a387bad3fef54bfc18dd31db4121cc76feb6251f
--- /dev/null
+++ b/doc/developer/examples/acsl_extension_ext_types.ml
@@ -0,0 +1,42 @@
+open Logic_ptree
+open Logic_typing
+open Cil_types
+
+let preprocessor =
+ List.map (fun e -> begin match e with
+ | { lexpr_node = PLnamed ("load", { lexpr_node = PLvar s}) } ->
+ if not (Logic_env.is_logic_type s) then Logic_env.add_typename s
+ else Kernel.error "Type already exists %s" s
+ | _ -> ()
+ end ; e)
+
+module Ts = struct
+ let id = ref 0
+ let types = Hashtbl.create 5
+
+ let add t = let i = !id in Hashtbl.add types i t ; id := i + 1 ; i
+ let find = Hashtbl.find types
+end
+
+let typer ctxt loc = function
+ | [ { lexpr_node = PLnamed ("load", { lexpr_node = PLvar s}) } ] ->
+ let ti = { lt_name = s ; lt_params = [] ; lt_def = None ; lt_attr = []} in
+ ctxt.add_logic_type s ti ;
+ Ext_id (Ts.add ti)
+ | _ ->
+ ctxt.error loc "Expected type loader"
+
+let visitor _ _ = Cil.SkipChildren
+
+let gen_printer s _pp fmt = function
+ | Ext_id i ->
+ Format.fprintf fmt "%s: %s"
+ (if s then "ext_type" else "load") (Ts.find i).lt_name
+ | _ -> assert false
+
+let printer = gen_printer false
+let short_printer = gen_printer true
+
+let () =
+ Acsl_extension.register_global
+ "ext_type" ~preprocessor typer ~visitor ~printer ~short_printer false
\ No newline at end of file
diff --git a/doc/developer/examples/acsl_extension_ext_types.png b/doc/developer/examples/acsl_extension_ext_types.png
new file mode 100644
index 0000000000000000000000000000000000000000..10943fd6b17151f8c5cc60cc9557a0b4d8c6b31c
Binary files /dev/null and b/doc/developer/examples/acsl_extension_ext_types.png differ
diff --git a/doc/developer/examples/acsl_extension.ml b/doc/developer/examples/acsl_extension_foo.ml
similarity index 78%
rename from doc/developer/examples/acsl_extension.ml
rename to doc/developer/examples/acsl_extension_foo.ml
index 9c677e002004f551f2cbfe95d296cdc3caa23997..239ccd00b7ab944e00e02acc3d086207b22fc296 100644
--- a/doc/developer/examples/acsl_extension.ml
+++ b/doc/developer/examples/acsl_extension_foo.ml
@@ -2,7 +2,7 @@ open Logic_ptree
open Cil_types
open Logic_typing
-let type_foo ~typing_context ~loc:_loc l =
+let type_foo typing_context _loc l =
let type_term ctxt env expr =
match expr.lexpr_node with
| PLvar "\\foo" -> Logic_const.tinteger ~loc:expr.lexpr_loc 42
@@ -14,4 +14,4 @@ let type_foo ~typing_context ~loc:_loc l =
in
Ext_terms res
-let () = Logic_typing.register_behavior_extension "foo" false type_foo
+let () = Acsl_extension.register_behavior "foo" type_foo false
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index f93a3797c6f1586aaeaa52de9858856bd5509e5b..3f43e26665fa03ad739e990fc8f99fc1e6d10fa9 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -525,6 +525,8 @@ src/kernel_services/ast_printing/printer_builder.mli: CEA_LGPL
src/kernel_services/ast_printing/printer_tag.ml: CEA_LGPL
src/kernel_services/ast_printing/printer_tag.mli: CEA_LGPL
src/kernel_services/ast_queries/README.md: .ignore
+src/kernel_services/ast_queries/acsl_extension.ml: CEA_LGPL
+src/kernel_services/ast_queries/acsl_extension.mli: CEA_LGPL
src/kernel_services/ast_queries/ast_info.ml: CEA_LGPL
src/kernel_services/ast_queries/ast_info.mli: CEA_LGPL
src/kernel_services/ast_queries/cil.ml: CIL
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index 07071b3e13a346cdd04a0827752b5aa5896fb005..dbb11fb4ac8537ec04e0be5b3437ea07063556e1 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -174,10 +174,10 @@
let res =
if not (Logic_utils.is_kw_c_mode ()) then begin
match Logic_env.extension_category s with
- | None -> None
- | Some Cil_types.Ext_contract -> Some (EXT_CONTRACT s)
- | Some Cil_types.Ext_global -> Some (EXT_GLOBAL s)
- | Some Cil_types.Ext_code_annot _ -> Some (EXT_CODE_ANNOT s)
+ | exception Not_found -> None
+ | Cil_types.Ext_contract -> Some (EXT_CONTRACT s)
+ | Cil_types.Ext_global -> Some (EXT_GLOBAL s)
+ | Cil_types.Ext_code_annot _ -> Some (EXT_CODE_ANNOT s)
end
else None
in
@@ -241,7 +241,7 @@
];
fun lexbuf ->
let s = lexeme lexbuf in
- try Hashtbl.find h s with Not_found ->
+ try Hashtbl.find h s with Not_found ->
if Logic_env.typename_status s then TYPENAME s
else
IDENTIFIER s
@@ -495,7 +495,7 @@ and comment = parse
{
let set_initial_location dest_lexbuf src_loc =
Lexing.(
- dest_lexbuf.lex_curr_p <-
+ dest_lexbuf.lex_curr_p <-
{ src_loc with
pos_bol = src_loc.pos_bol - src_loc.pos_cnum;
pos_cnum = 0; };
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 7d800ea9fe6be22f57a17c8ecab9b301efba66b1..cb3068846b093a6a5f2efe1e807fda896318128d 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -109,14 +109,14 @@
let concat_froms a1 a2 =
let compare_pair (b1,_) (b2,_) = is_same_lexpr b1 b2 in
- (* NB: the following has an horrible complexity, but the order of
+ (* NB: the following has an horrible complexity, but the order of
clauses in the input is preserved. *)
let concat_one acc (_,f2 as p) =
try
let (_,f1) = List.find (compare_pair p) acc
in
match (f1, f2) with
- | _,FromAny ->
+ | _,FromAny ->
(* the new fundeps does not give more information than the one
which is already present. Just ignore it.
*)
@@ -125,11 +125,11 @@
(* the new fundeps is strictly more precise than the old one.
We replace the old dependency by the new one, but keep
the location at its old place in the list. This ensures
- that we get the exact same clause if we try to
+ that we get the exact same clause if we try to
link the original contract with its pretty-printed version. *)
Extlib.replace compare_pair p acc
- | From _, From _ ->
- (* we keep the two functional dependencies,
+ | From _, From _ ->
+ (* we keep the two functional dependencies,
as they have to be proved separately. *)
acc @ [p]
with Not_found -> acc @ [p]
@@ -140,7 +140,7 @@
| FreeAllocAny,_ -> fa2
| _,FreeAllocAny -> fa1
| FreeAlloc(f1,a1),FreeAlloc(f2,a2) -> FreeAlloc(f2@f1,a2@a1)
-
+
(* a1 represents the assigns _after_ the current clause a2. *)
let concat_assigns a1 a2 =
match a1,a2 with
@@ -152,17 +152,17 @@
| Writes a1, a2 -> Writes (concat_froms a2 a1)
let concat_loop_assigns_allocation annots bhvs2 a2 fa2=
- (* NB: this is supposed to merge assigns related to named behaviors, in
+ (* NB: this is supposed to merge assigns related to named behaviors, in
case of annotation like
for a,b: assigns x,y;
for b,c: assigns z,t;
- DO NOT CALL this function for loop assigns not attached to specific
- behaviors.
+ DO NOT CALL this function for loop assigns not attached to specific
+ behaviors.
*)
assert (bhvs2 <> []);
- if fa2 == FreeAllocAny && a2 == WritesAny
+ if fa2 == FreeAllocAny && a2 == WritesAny
then annots
- else
+ else
let split l1 l2 =
let treat_one (only1,both,only2) x =
if List.mem x l1 then
@@ -201,12 +201,12 @@
let (bhvs2, annots) = List.fold_right treat_one annots (bhvs2,[]) in
match bhvs2 with
| [] -> annots (* Already considered all cases. *)
- | _ ->
- let annots = if a2 <> WritesAny
+ | _ ->
+ let annots = if a2 <> WritesAny
then AAssigns (bhvs2,a2) :: annots
else annots
- in
- if fa2 <> FreeAllocAny
+ in
+ if fa2 <> FreeAllocAny
then AAllocation (bhvs2,fa2) :: annots
else annots
@@ -362,9 +362,9 @@ lexpr:
{ info (PLif ($1, $3, $5)) }
/* both terms and predicates */
| any_identifier COLON lexpr %prec prec_named { info (PLnamed ($1, $3)) }
-| string COLON lexpr %prec prec_named
+| string COLON lexpr %prec prec_named
{ let (iswide,str) = $1 in
- if iswide then begin
+ if iswide then begin
let l = loc () in
raise (Not_well_formed(l, "Wide strings are not allowed as labels."))
end;
@@ -459,15 +459,15 @@ lexpr_inner:
| VALID opt_label_1 LPAR lexpr RPAR { info (PLvalid ($2,$4)) }
| VALID_READ opt_label_1 LPAR lexpr RPAR { info (PLvalid_read ($2,$4)) }
| VALID_FUNCTION LPAR lexpr RPAR { info (PLvalid_function $3) }
-| VALID_INDEX opt_label_1 LPAR lexpr COMMA lexpr RPAR {
+| VALID_INDEX opt_label_1 LPAR lexpr COMMA lexpr RPAR {
let source = fst (loc ()) in
obsolete ~source "\\valid_index(addr,idx)" ~now:"\\valid(addr+idx)";
info (PLvalid ($2,info (PLbinop ($4, Badd, $6)))) }
| VALID_RANGE opt_label_1 LPAR lexpr COMMA lexpr COMMA lexpr RPAR {
let source = fst (loc ()) in
- obsolete "\\valid_range(addr,min,max)"
+ obsolete "\\valid_range(addr,min,max)"
~source ~now:"\\valid(addr+(min..max))";
- info (PLvalid
+ info (PLvalid
($2,info (PLbinop ($4, Badd, (info (PLrange((Some $6),Some $8)))))))
}
| INITIALIZED opt_label_1 LPAR lexpr RPAR { info (PLinitialized ($2,$4)) }
@@ -953,7 +953,7 @@ ext_function_specs_opt:
;
ext_function_specs:
-| ext_at_stmt_markup { []}
+| ext_at_stmt_markup { []}
| ext_function_spec { [$1] }
| ext_function_spec ext_function_specs { $1::$2 }
;
@@ -969,7 +969,7 @@ ext_fun_specs:
;
ext_fun_spec:
-| ext_at_stmt_markup ext_stmt_loop_spec
+| ext_at_stmt_markup ext_stmt_loop_spec
{ Ext_stmt($1,$2,loc()) }
| ext_contract_markup contract
{ let s,pos = $2 in Ext_spec (s,pos) }
@@ -981,7 +981,7 @@ ext_stmt_loop_spec:
;
ext_identifier_opt:
-| /* empty*/ { "" }
+| /* empty*/ { "" }
| ext_identifier { $1 }
;
@@ -1030,12 +1030,12 @@ contract:
let behaviors =
if requires <> [] || post_cond <> [] ||
allocation <> FreeAllocAny ||
- assigns <> WritesAny || extended <> []
+ assigns <> WritesAny || extended <> []
then
(Cabshelper.mk_behavior
~requires ~post_cond ~assigns ~allocation ~extended ())
:: behaviors
- else if $2<>None || $3<>None ||
+ else if $2<>None || $3<>None ||
behaviors<>[] || completes<>[] ||disjoints<>[]
then behaviors
else raise (Not_well_formed (loc(),"Empty annotation is not allowed"))
@@ -1100,7 +1100,7 @@ clause_kw:
| FREES {"frees"}
| COMPLETE {"complete"}
| DISJOINT {"disjoint"}
-/* often, we'll be in c_kw_mode, where these keywords are
+/* often, we'll be in c_kw_mode, where these keywords are
recognized as identifiers... */
| IDENTIFIER { $1 }
| EXT_CONTRACT { $1 }
@@ -1166,7 +1166,8 @@ ne_simple_clauses:
}
| EXT_CONTRACT grammar_extension SEMICOLON simple_clauses
{ let allocation,assigns,post_cond,extended = $4 in
- allocation,assigns,post_cond,($1,$2)::extended
+ let processed = Logic_env.preprocess_extension $1 $2 in
+ allocation,assigns,post_cond,($1,processed)::extended
}
| post_cond_kind full_lexpr clause_kw { missing 2 ";" $3 }
| allocation clause_kw { missing 1 ";" $2 }
@@ -1301,7 +1302,7 @@ loop_annotations:
let ext = List.map (fun x -> AExtended([],true, x)) e in
let oth = match a with
| WritesAny -> b
- | Writes _ ->
+ | Writes _ ->
(* by definition all existing AAssigns are tied to at least
one behavior. No need to merge against them. *)
AAssigns ([],a)::b
@@ -1338,7 +1339,7 @@ loop_annot_stack:
check_empty
(pos, "loop extension is not allowed after loop variant.") e;
(match fa with
- | FreeAlloc(f,a) ->
+ | FreeAlloc(f,a) ->
check_empty
(pos,"loop frees is not allowed after loop variant.") f ;
check_empty
@@ -1346,9 +1347,9 @@ loop_annot_stack:
| FreeAllocAny -> ());
(match a with
WritesAny -> ()
- | Writes _ ->
- raise
- (Not_well_formed
+ | Writes _ ->
+ raise
+ (Not_well_formed
(pos,"loop assigns is not allowed after loop variant.")));
check_empty
(pos,"loop behavior is not allowed after loop variant.") b ;
@@ -1391,13 +1392,18 @@ loop_grammar_extension:
| LOOP EXT_CODE_ANNOT grammar_extension SEMICOLON {
let open Cil_types in
let ext = $2 in
- match Logic_env.extension_category ext with
- | Some (Ext_code_annot (Ext_next_loop | Ext_next_both)) -> (ext, $3)
- | Some (Ext_code_annot (Ext_here | Ext_next_stmt)) ->
- raise
- (Not_well_formed
- (lexeme_loc 2, ext ^ " is not a loop annotation extension"))
- | Some (Ext_contract | Ext_global) | None ->
+ try
+ begin match Logic_env.extension_category ext with
+ | Ext_code_annot (Ext_next_loop | Ext_next_both) ->
+ let processed = Logic_env.preprocess_extension ext $3 in
+ (ext, processed)
+ | Ext_code_annot (Ext_here | Ext_next_stmt) ->
+ raise
+ (Not_well_formed
+ (lexeme_loc 2, ext ^ " is not a loop annotation extension"))
+ | _ -> raise Not_found
+ end
+ with Not_found ->
Kernel.fatal ~source:(lexeme_start 2)
"%s is not a code annotation extension. Parser got wrong lexeme." ext
}
@@ -1444,16 +1450,20 @@ code_annotation:
{ fun bhvs ->
let open Cil_types in
let ext = $1 in
- match Logic_env.extension_category ext with
- | Some (Ext_code_annot (Ext_here | Ext_next_stmt | Ext_next_both)) ->
- Logic_ptree.AExtended(bhvs,false,(ext,$2))
- | Some (Ext_code_annot Ext_next_loop) ->
- raise
- (Not_well_formed
- (lexeme_loc 1,
- ext ^ " is not a loop annotation extension. It can't be used as \
- plain code annotation extension"))
- | Some (Ext_contract | Ext_global) | None ->
+ try
+ begin match Logic_env.extension_category ext with
+ | Ext_code_annot (Ext_here | Ext_next_stmt | Ext_next_both) ->
+ let processed = Logic_env.preprocess_extension ext $2 in
+ Logic_ptree.AExtended(bhvs,false,(ext,processed))
+ | Ext_code_annot Ext_next_loop ->
+ raise
+ (Not_well_formed
+ (lexeme_loc 1,
+ ext ^ " is not a loop annotation extension. It can't be used \
+ as plain code annotation extension"))
+ | _ -> raise Not_found
+ end
+ with Not_found ->
Kernel.fatal ~source:(lexeme_start 1)
"%s is not a code annotation extension. Parser got wrong lexeme" ext
}
@@ -1491,7 +1501,10 @@ decl:
| type_annot {LDtype_annot $1}
| model_annot {LDmodel_annot $1}
| logic_def { $1 }
-| EXT_GLOBAL grammar_extension SEMICOLON { LDextended ($1, $2) }
+| EXT_GLOBAL grammar_extension SEMICOLON {
+ let processed = Logic_env.preprocess_extension $1 $2 in
+ LDextended ($1, processed)
+ }
| deprecated_logic_decl { $1 }
;
@@ -1516,7 +1529,7 @@ volatile_opt:
type_annot:
| TYPE INVARIANT any_identifier LPAR full_parameter RPAR EQUAL
full_lexpr SEMICOLON
- { let typ,name = $5 in{ inv_name = $3; this_name = name; this_type = typ; inv = $8; } }
+ { let typ,name = $5 in{ inv_name = $3; this_name = name; this_type = typ; inv = $8; } }
;
opt_semicolon:
@@ -1525,8 +1538,8 @@ opt_semicolon:
model_annot:
| MODEL type_spec LBRACE full_parameter opt_semicolon RBRACE SEMICOLON
- { let typ,name = $4 in
- { model_for_type = $2; model_name = name; model_type = typ; }
+ { let typ,name = $4 in
+ { model_for_type = $2; model_name = name; model_type = typ; }
}
;
@@ -1612,7 +1625,7 @@ deprecated_logic_decl:
exit_type_variables_scope ();
let source = fst (loc ()) in
obsolete "logic type declaration" ~source ~now:"an axiomatic block";
- LDtype(id,tvars,None)
+ LDtype(id,tvars,None)
}
/* OBSOLETE: axiom */
| AXIOM poly_id COLON full_lexpr SEMICOLON
@@ -1710,21 +1723,21 @@ ne_label_list:
| label_name COMMA ne_label_list { $1 :: $3 }
;
-opt_label_1:
-| opt_label_list { match $1 with
+opt_label_1:
+| opt_label_list { match $1 with
| [] -> None
| l::[] -> Some l
| _ -> raise (Not_well_formed (loc(),"Only one label is allowed")) }
;
-
-opt_label_2:
-| opt_label_list { match $1 with
+
+opt_label_2:
+| opt_label_list { match $1 with
| [] -> None
| l1::l2::[] -> Some (l1,l2)
| _::[] -> raise (Not_well_formed (loc(),"One label is missing"))
| _ -> raise (Not_well_formed (loc(),"Only two labels are allowed")) }
;
-
+
opt_label_list:
| /* epsilon */ { [] }
| LBRACE ne_label_list RBRACE { $2 }
@@ -1884,7 +1897,7 @@ non_logic_keyword:
| is_acsl_spec { $1 }
| is_acsl_decl_or_code_annot { $1 }
| is_acsl_other { $1 }
-| CUSTOM { "custom" (* token that cannot be used in C fields *) }
+| CUSTOM { "custom" (* token that cannot be used in C fields *) }
;
bs_keyword:
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 385f2198dc87e4b379def5051dd28664120ab273..b459538e712e53f261195d44c944a766181fcf88 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -9625,29 +9625,35 @@ and doBody local_env (blk: A.block) : chunk =
(Logic_ptree.AExtended(_,is_loop,(name,_)),loc) ->
let source = fst loc in
(match Logic_env.extension_category name, is_loop with
- | Some (Ext_code_annot Ext_here), false -> [], false
- | Some (Ext_code_annot Ext_next_stmt), false -> [], true
- | Some (Ext_code_annot Ext_next_loop), true -> [], false
- | Some (Ext_code_annot Ext_next_both), _ -> [], not is_loop
- | Some (Ext_code_annot (Ext_here | Ext_next_stmt)), true ->
+ | exception Not_found ->
+ Kernel.(
+ warning
+ ~source ~wkey:wkey_acsl_extension
+ "%s is not a known extension" name);
+ [], false
+ | Ext_code_annot Ext_here, false -> [], false
+ | Ext_code_annot Ext_next_stmt, false -> [], true
+ | Ext_code_annot Ext_next_loop, true -> [], false
+ | Ext_code_annot Ext_next_both, _ -> [], not is_loop
+ | Ext_code_annot (Ext_here | Ext_next_stmt), true ->
Kernel.(
warning
~source ~wkey:wkey_acsl_extension
"%s is a code annotation extension, \
but used here as a loop annotation" name);
[], false
- | Some (Ext_code_annot Ext_next_loop), false ->
+ | Ext_code_annot Ext_next_loop, false ->
Kernel.(
warning
~source ~wkey:wkey_acsl_extension
"%s is a loop annotation extension, \
but used here as a code annotation" name);
[], false
- | (Some (Ext_global | Ext_contract) | None), _ ->
+ | (Ext_global | Ext_contract), _ ->
Kernel.(
warning
~source ~wkey:wkey_acsl_extension
- "%s is not a known code annotation extension" name);
+ "%s is not a code annotation extension" name);
[], false)
| _ -> [], false
in
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 13259d5a56cf1cbc129ac1842053fbaf8d629cec..5aa6db6a1c5830df96ed4fcad6ee30d720d69dfd 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -27,37 +27,47 @@ open Cil_datatype
open Printer_api
open Format
-module Behavior_extensions = struct
+module Extensions = struct
+ let initialized = ref false
+ let ref_print = ref (fun _ _ _ _ -> assert false)
+ let ref_short_print = ref (fun _ _ _ _ -> assert false)
+
+ let set_handler ~print ~short_print =
+ assert (not !initialized) ;
+ ref_print := print ;
+ ref_short_print := short_print ;
+ initialized := true ;
+ ()
- let printer_tbl = Hashtbl.create 5
-
- let register name printer =
- Hashtbl.add printer_tbl name printer
+ let pp (printer) fmt {ext_name; ext_kind} =
+ !ref_print ext_name printer fmt ext_kind
- let default_pp printer fmt ext =
- match ext with
- | Ext_id i -> Format.pp_print_int fmt i
- | Ext_terms terms ->
- Pretty_utils.pp_list ~sep:",@ " printer#term fmt terms
- | Ext_preds preds ->
- Pretty_utils.pp_list ~sep:",@ " printer#predicate fmt preds
+ let pp_short (printer) fmt {ext_name; ext_kind} =
+ !ref_short_print ext_name printer fmt ext_kind
- let pp (printer) fmt {ext_name; ext_kind} =
- let pp =
- try
- Hashtbl.find printer_tbl ext_name
- with Not_found -> default_pp
- in
- Format.fprintf fmt "@[<hov 2>%s %a;@]" ext_name (pp printer) ext_kind
+ let ref_deprecated_handler = ref (fun _ _ _ -> assert false)
+ let set_deprecated_handler ~handler =
+ ref_deprecated_handler := handler
+ let deprecated_register name =
+ !ref_deprecated_handler name
end
-let register_behavior_extension = Behavior_extensions.register
+let set_extension_handler = Extensions.set_handler
-let register_code_annot_extension = Behavior_extensions.register
+(* Deprecated functions *)
+let set_deprecated_extension_handler = Extensions.set_deprecated_handler
-let register_loop_annot_extension = Behavior_extensions.register
+let register_behavior_extension name =
+ Extensions.deprecated_register name Ext_contract
-let register_global_extension = Behavior_extensions.register
+let register_code_annot_extension name =
+ Extensions.deprecated_register name (Ext_code_annot Ext_here)
+
+let register_loop_annot_extension name =
+ Extensions.deprecated_register name (Ext_code_annot Ext_next_loop)
+
+let register_global_extension name =
+ Extensions.deprecated_register name Ext_global
(* Internal attributes. Won't be pretty-printed *)
let reserved_attributes = ref []
@@ -2746,8 +2756,11 @@ class cil_printer () = object (self)
self#pp_acsl_keyword "requires"
self#identified_predicate p
- method extended fmt (ext : acsl_extension) =
- Behavior_extensions.pp (self :> extensible_printer_type) fmt ext
+ method extended fmt ext =
+ Extensions.pp (self :> extensible_printer_type) fmt ext
+
+ method short_extended fmt ext =
+ Extensions.pp_short (self :> extensible_printer_type) fmt ext
method post_cond fmt (k,p) =
let kw = get_termination_kind_name k in
diff --git a/src/kernel_services/ast_printing/cil_printer.mli b/src/kernel_services/ast_printing/cil_printer.mli
index 3edbd8bc09e81650ba7cc7a2caff541df00960ce..20761da4fbddf55e599663f6ef423fee3e84a15f 100644
--- a/src/kernel_services/ast_printing/cil_printer.mli
+++ b/src/kernel_services/ast_printing/cil_printer.mli
@@ -41,31 +41,39 @@ val register_behavior_extension:
Cil_types.acsl_extension_kind -> unit) -> unit
(** Register a pretty-printer used for behavior extension.
@plugin development guide
+ @deprecated Frama-C+dev
*)
+[@@ deprecated "Use Acsl_extension.register_behavior (arg: ~printer) instead"]
val register_global_extension:
string ->
(Printer_api.extensible_printer_type -> Format.formatter ->
Cil_types.acsl_extension_kind -> unit) -> unit
-(** Register a pretty-printer used for behavior extension.
+(** Register a pretty-printer used for global extension.
@plugin development guide
+ @deprecated Frama-C+dev
*)
+[@@ deprecated "Use Acsl_extension.register_global (arg: ~printer) instead"]
val register_code_annot_extension:
string ->
(Printer_api.extensible_printer_type -> Format.formatter ->
Cil_types.acsl_extension_kind -> unit) -> unit
-(** Register a pretty-printer used for behavior extension.
+(** Register a pretty-printer used for code annotation extension.
@plugin development guide
+ @deprecated Frama-C+dev
*)
+[@@ deprecated "Use Acsl_extension.register_code_annot_<kind> (arg: ~printer) instead"]
val register_loop_annot_extension:
string ->
(Printer_api.extensible_printer_type -> Format.formatter ->
Cil_types.acsl_extension_kind -> unit) -> unit
-(** Register a pretty-printer used for behavior extension.
+(** Register a pretty-printer used for loop annotation extension.
@plugin development guide
+ @deprecated Frama-C+dev
*)
+[@@ deprecated "Use Acsl_extension.register_loop_annot (arg: ~printer) instead"]
val state: Printer_api.state
@@ -73,6 +81,25 @@ val print_global: Cil_types.global -> bool
(** Is the given global displayed by the pretty-printer.
@since Aluminium-20160501 *)
+(**/**)
+
+val set_extension_handler:
+ print:(string -> Printer_api.extensible_printer_type ->
+ Format.formatter -> Cil_types.acsl_extension_kind -> unit) ->
+ short_print:(string -> Printer_api.extensible_printer_type ->
+ Format.formatter -> Cil_types.acsl_extension_kind -> unit) ->
+ unit
+(** Used to setup a reference related to the handling of ACSL extensions.
+ If your name is not [Acsl_extension], do not call this.
+ @since Frama-C+dev
+*)
+
+val set_deprecated_extension_handler:
+ handler:(string -> Cil_types.ext_category ->
+ (Printer_api.extensible_printer_type -> Format.formatter ->
+ Cil_types.acsl_extension_kind -> unit) ->
+ unit) -> unit
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/ast_printing/printer_api.mli b/src/kernel_services/ast_printing/printer_api.mli
index edc38a8890da411df5bc4698814c770cad3837db..b377d619209b748b717be7efffaa57e09f18ae90 100644
--- a/src/kernel_services/ast_printing/printer_api.mli
+++ b/src/kernel_services/ast_printing/printer_api.mli
@@ -283,6 +283,7 @@ class type extensible_printer_type = object
method assumes: Format.formatter -> identified_predicate -> unit
method extended: Format.formatter -> Cil_types.acsl_extension -> unit
+ method short_extended: Format.formatter -> Cil_types.acsl_extension -> unit
method funspec: Format.formatter -> funspec -> unit
@@ -444,6 +445,8 @@ module type S_pp = sig
val pp_logic_label: Format.formatter -> logic_label -> unit
val pp_builtin_logic_info: Format.formatter -> builtin_logic_info -> unit
val pp_extended: Format.formatter -> acsl_extension -> unit
+ val pp_short_extended: Format.formatter -> acsl_extension -> unit
+ (** @since Frama-C+dev *)
val pp_predicate_node: Format.formatter -> predicate_node -> unit
val pp_predicate: Format.formatter -> predicate -> unit
val pp_identified_predicate: Format.formatter -> identified_predicate -> unit
diff --git a/src/kernel_services/ast_printing/printer_builder.ml b/src/kernel_services/ast_printing/printer_builder.ml
index bba10960ff4b6230c9e9f06c7bf1ab1b3302d263..1d9ba02b1b68e8d275b3696c2d5735feb4f9ff16 100644
--- a/src/kernel_services/ast_printing/printer_builder.ml
+++ b/src/kernel_services/ast_printing/printer_builder.ml
@@ -85,6 +85,7 @@ struct
let pp_logic_type_info fmt x = (printer ())#logic_type_info fmt x
let pp_logic_ctor_info fmt x = (printer ())#logic_ctor_info fmt x
let pp_extended fmt x = (printer())#extended fmt x
+ let pp_short_extended fmt x = (printer())#short_extended fmt x
let pp_initinfo fmt x = (printer ())#initinfo fmt x
let pp_logic_info fmt x = (printer ())#logic_info fmt x
let pp_logic_constant fmt x = (printer ())#logic_constant fmt x
diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e82c29b554f4acfc0e56a08282a5a8924b214326
--- /dev/null
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -0,0 +1,191 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open Logic_typing
+open Logic_ptree
+
+type extension_preprocessor =
+ lexpr list -> lexpr list
+type extension_typer =
+ typing_context -> location -> lexpr list -> acsl_extension_kind
+type extension_visitor =
+ Cil.cilVisitor -> acsl_extension_kind -> acsl_extension_kind Cil.visitAction
+type extension_printer =
+ Printer_api.extensible_printer_type -> Format.formatter ->
+ acsl_extension_kind -> unit
+type extension = {
+ category: ext_category ;
+ status: bool ;
+ preprocessor: extension_preprocessor ;
+ typer: extension_typer ;
+ visitor: extension_visitor ;
+ printer: extension_printer ;
+ short_printer: extension_printer ;
+}
+
+let default_printer printer fmt = function
+ | Ext_id i -> Format.fprintf fmt "%d" i
+ | Ext_terms ts -> Pretty_utils.pp_list ~sep:",@ " printer#term fmt ts
+ | Ext_preds ps -> Pretty_utils.pp_list ~sep:",@ " printer#predicate fmt ps
+
+let default_short_printer name _printer fmt _ext_kind =
+ Format.fprintf fmt "%s" name
+
+let make
+ name category
+ ?(preprocessor=Extlib.id)
+ typer
+ ?(visitor=fun _ _ -> Cil.DoChildren)
+ ?(printer=default_printer)
+ ?(short_printer=default_short_printer name)
+ status =
+ { category; status; preprocessor; typer; visitor; printer; short_printer }
+
+module Extensions = struct
+ let ext_tbl = Hashtbl.create 5
+
+ let find name =
+ try Hashtbl.find ext_tbl name
+ with Not_found ->
+ Kernel.fatal ~current:true "unsupported clause of name '%s'" name
+
+ (* [Logic_lexer] can ask for something that is not a category, which is not
+ a fatal error. *)
+ let category name = (Hashtbl.find ext_tbl name).category
+
+ let is_extension = Hashtbl.mem ext_tbl
+
+ let register
+ cat name ?preprocessor typer ?visitor ?printer ?short_printer status =
+ let info =
+ make name cat ?preprocessor typer ?visitor ?printer ?short_printer status
+ in
+ if is_extension name then
+ Kernel.warning ~wkey:Kernel.wkey_acsl_extension
+ "Trying to register ACSL extension %s twice. Ignoring second extension"
+ name
+ else Hashtbl.add ext_tbl name info
+
+ let preprocess name = (find name).preprocessor
+
+ let typing name typing_context loc es =
+ let ext_info = find name in
+ let status = ext_info.status in
+ let typer = ext_info.typer in
+ let normal_error = ref false in
+ let has_error () = normal_error := true in
+ let wrapper =
+ typing_context.on_error (typer typing_context loc) has_error
+ in
+ try status, wrapper es
+ with
+ | (Log.AbortError _ | Log.AbortFatal _) as exn -> raise exn
+ | exn when not !normal_error ->
+ Kernel.fatal "Typechecking ACSL extension %s raised exception %s"
+ name (Printexc.to_string exn)
+
+ let visit name = (find name).visitor
+
+ let print name printer fmt kind =
+ let pp = (find name).printer printer in
+ Format.fprintf fmt "@[<hov 2>%s %a;@]" name pp kind
+
+ let short_print name printer fmt kind =
+ let pp = (find name).short_printer in
+ Format.fprintf fmt "%a" (pp printer) kind
+end
+
+(* Registration functions *)
+
+let register_behavior =
+ Extensions.register Ext_contract
+let register_global =
+ Extensions.register Ext_global
+let register_code_annot =
+ Extensions.register (Ext_code_annot Ext_here)
+let register_code_annot_next_stmt =
+ Extensions.register (Ext_code_annot Ext_next_stmt)
+let register_code_annot_next_loop =
+ Extensions.register (Ext_code_annot Ext_next_loop)
+let register_code_annot_next_both =
+ Extensions.register (Ext_code_annot Ext_next_both)
+
+(* Setup global references *)
+
+let () =
+ Logic_env.set_extension_handler
+ ~category:Extensions.category
+ ~is_extension: Extensions.is_extension
+ ~preprocess: Extensions.preprocess ;
+ Logic_typing.set_extension_handler
+ ~is_extension: Extensions.is_extension
+ ~typer: Extensions.typing ;
+ Cil.set_extension_handler
+ ~visit: Extensions.visit ;
+ Cil_printer.set_extension_handler
+ ~print: Extensions.print
+ ~short_print:Extensions.short_print
+
+(* For Deprecation: *)
+
+let deprecated_replace name ext = Hashtbl.add Extensions.ext_tbl name ext
+
+let strong_cat = Hashtbl.create 5
+
+let default_typer _typing_context _loc _l = assert false
+
+
+let deprecated_find ?(strong=true) name cat op_name =
+ match Hashtbl.find_opt Extensions.ext_tbl name with
+ | None ->
+ if strong then Hashtbl.add strong_cat name cat ;
+ (make name cat default_typer false)
+ | Some ext ->
+ if strong && Hashtbl.mem strong_cat name then begin
+ if ext.category = cat then ext
+ else
+ Kernel.fatal
+ "Registring %s for %s: this extension already exists for another \
+ category"
+ op_name name
+ end else if strong then begin
+ Hashtbl.add strong_cat name cat ;
+ { ext with category = cat }
+ end else ext
+
+let deprecated_register_typing name cat status typer =
+ deprecated_replace name
+ { (deprecated_find name cat "typing") with status ; typer }
+
+let deprecated_register_printing name cat printer =
+ deprecated_replace name
+ { (deprecated_find ~strong:false name cat "printing") with printer }
+
+let deprecated_register_visit name cat visitor =
+ deprecated_replace name
+ { (deprecated_find name cat "visit") with visitor }
+
+let () =
+ Logic_typing.set_deprecated_extension_handler deprecated_register_typing ;
+ Cil.set_deprecated_extension_handler deprecated_register_visit ;
+ Cil_printer.set_deprecated_extension_handler deprecated_register_printing
diff --git a/src/kernel_services/ast_queries/acsl_extension.mli b/src/kernel_services/ast_queries/acsl_extension.mli
new file mode 100644
index 0000000000000000000000000000000000000000..5ea377e07750705c16b9792e78b898df503d0278
--- /dev/null
+++ b/src/kernel_services/ast_queries/acsl_extension.mli
@@ -0,0 +1,150 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** ACSL extensions registration module
+ @since Frama-C+dev
+*)
+
+open Cil_types
+open Logic_typing
+open Logic_ptree
+
+(** Untyped ACSL extensions transformers *)
+type extension_preprocessor =
+ lexpr list -> lexpr list
+
+(** Transformers from untyped to typed ACSL extension *)
+type extension_typer =
+ typing_context -> location -> lexpr list -> acsl_extension_kind
+(** Visitor functions for ACSL extensions *)
+type extension_visitor =
+ Cil.cilVisitor -> acsl_extension_kind -> acsl_extension_kind Cil.visitAction
+(** Pretty printers for ACSL extensions *)
+type extension_printer =
+ Printer_api.extensible_printer_type -> Format.formatter ->
+ acsl_extension_kind -> unit
+
+
+(** [register_behavior name ~preprocessor typer ~visitor ~printer ~short_printer status]
+ registers new ACSL extension to be used in function contracts with name
+ [name].
+
+ The optional [preprocessor] is a function to be applied by the parser on the
+ untyped content of the extension before parsing the rest of the processed
+ file. By default, this function is the identity.
+
+ The [typer] is applied when transforming the untyped AST to Cil. It recieves
+ the typing context of the annotation that can be used to type the received
+ logic expressions (see [Logic_typing.typing_context]), and the location of
+ the annotation.
+
+ The optional [visitor] allows changing the way the ACSL extension is visited.
+ By default, the behavior is [Cil.DoChildren], which ends up visiting
+ each identified predicate/term in the list and leave the id as is.
+
+ The optional [printer] allows changing the way the ACSL extension is pretty
+ printed. By default, it prints the name of the extension followed by the
+ formatted predicates, terms or identifier according to the
+ [Cil_types.acsl_extension_kind].
+
+ The optional [short_printer] allows changing the [Printer.pp_short_extended]
+ behavior for the ACSL extension. By default, it just prints the [name]. It
+ is for example used for the filetree in the GUI.
+
+ The [status] indicates whether the extension can be assigned a property
+ status or not.
+
+ Here is a basic example:
+ [
+ let count = ref 0
+ let foo_typer ~typing_context ~loc = function
+ | p :: [] ->
+ Ext_preds
+ [ (typing_context.type_predicate
+ typing_context
+ (typing_context.post_state [Normal])
+ p)])
+ | [] -> let id = !count in incr count; Ext_id id
+ | _ -> typing_context.error loc "expecting a predicate after keyword FOO"
+
+ let () = Acsl_extension.register_behavior "FOO" foo_typer false
+ ]
+ @plugin development guide
+*)
+val register_behavior:
+ string -> ?preprocessor:extension_preprocessor -> extension_typer ->
+ ?visitor:extension_visitor ->
+ ?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
+ unit
+
+(** Registers extension for global annotation. See [register_behavior].
+
+ @plugin development guide
+*)
+val register_global:
+ string -> ?preprocessor:extension_preprocessor -> extension_typer ->
+ ?visitor:extension_visitor ->
+ ?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
+ unit
+
+(** Registers extension for code annotation to be evaluated at _current_
+ program point. See [register_behavior].
+
+ @plugin development guide
+*)
+val register_code_annot:
+ string -> ?preprocessor:extension_preprocessor -> extension_typer ->
+ ?visitor:extension_visitor ->
+ ?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
+ unit
+
+(** Registers extension for code annotation to be evaluated for the _next_
+ statement. See [register_behavior].
+
+ @plugin development guide
+*)
+val register_code_annot_next_stmt:
+ string -> ?preprocessor:extension_preprocessor -> extension_typer ->
+ ?visitor:extension_visitor ->
+ ?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
+ unit
+
+(** Registers extension for loop annotation. See [register_behavior].
+
+ @plugin development guide
+*)
+val register_code_annot_next_loop:
+ string -> ?preprocessor:extension_preprocessor -> extension_typer ->
+ ?visitor:extension_visitor ->
+ ?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
+ unit
+
+(** Registers extension both for code and loop annotations.
+ See [register_behavior].
+
+ @plugin development guide
+*)
+val register_code_annot_next_both:
+ string -> ?preprocessor:extension_preprocessor -> extension_typer ->
+ ?visitor:extension_visitor ->
+ ?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
+ unit
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index d52be341225739de126ccc744555a101393a6d96..2b2014430b23d0279877de51b5d16ce373e2b553 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -755,9 +755,31 @@ let alphabetabeta _ x = x
let alphabetafalse _ _ = false
let alphatrue _ = true
-let visitor_tbl = Hashtbl.create 5
+module Extensions = struct
+ let initialized = ref false
+ let ref_visit = ref (fun _ _ _ -> assert false)
+
+ let set_handler ~visit =
+ assert (not !initialized) ;
+ ref_visit := visit ;
+ initialized := true ;
+ ()
+
+ let visit name = !ref_visit name
+
+ let ref_deprecated_handler = ref (fun _ _ _ -> assert false)
+ let set_deprecated_handler ~handler =
+ ref_deprecated_handler := handler
+
+ let register_behavior name ext =
+ !ref_deprecated_handler name Ext_contract ext
+end
+let set_extension_handler = Extensions.set_handler
+
+(* Deprecated *)
+let set_deprecated_extension_handler = Extensions.set_deprecated_handler
+let register_behavior_extension = Extensions.register_behavior
-let register_behavior_extension name ext = Hashtbl.add visitor_tbl name ext
(* sm/gn: cil visitor interface for traversing Cil trees. *)
(* Use visitCilStmt and/or visitCilFile to use this. *)
@@ -1889,10 +1911,7 @@ and childrenBehavior vis b =
b
and visitCilExtended vis orig =
- let visit =
- try Hashtbl.find visitor_tbl orig.ext_name
- with Not_found -> (fun _ _ -> DoChildren)
- in
+ let visit = Extensions.visit orig.ext_name in
let e' = doVisitCil vis id (visit vis) childrenCilExtended orig.ext_kind in
if Visitor_behavior.is_fresh vis#behavior then
Logic_const.new_acsl_extension orig.ext_name orig.ext_loc
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 71441398d0f3295ff00892f83f4c7a5b59b37a5d..45ed7d8e6a810257090bfe89984685338084b964 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1725,11 +1725,13 @@ end
@since Sodium-20150201
@modify Silicon-20161101
+ @deprecated Frama-C+dev
*)
val register_behavior_extension:
string ->
(cilVisitor -> acsl_extension_kind -> (acsl_extension_kind) visitAction)
-> unit
+[@@ deprecated "Use Acsl_extension.register_behavior instead (arg: ~visitor)"]
(**/**)
class internal_genericCilVisitor:
@@ -2283,6 +2285,20 @@ val pp_ikind_ref: (Format.formatter -> ikind -> unit) ref
val pp_attribute_ref: (Format.formatter -> attribute -> unit) ref
val pp_attributes_ref: (Format.formatter -> attribute list -> unit) ref
+val set_extension_handler:
+ visit:(string -> cilVisitor -> acsl_extension_kind ->
+ acsl_extension_kind visitAction) ->
+ unit
+(** Used to setup a reference related to the handling of ACSL extensions.
+ If your name is not [Acsl_extension], do not call this
+ @since Frama-C+dev
+*)
+
+val set_deprecated_extension_handler:
+ handler:(string -> ext_category ->
+ (cilVisitor -> acsl_extension_kind -> acsl_extension_kind visitAction) ->
+ unit) -> unit
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 8407b28c10c8f1d1f6ad88010bda899003db46d2..e52999590bdfd130d82f902af2ee6e1b6c6a1e7e 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -724,15 +724,17 @@ let synchronize_source_annot has_new_stmt kf =
| AStmtSpec _ | APragma (Slice_pragma SPstmt | Impact_pragma IPstmt)
-> true
| AExtended(_,is_loop,{ext_name}) ->
+ let warn_not_a_code_annot () =
+ Kernel.(
+ warning ~wkey:wkey_acsl_extension
+ "%s is not a code annotation extension" name)
+ in
(match Logic_env.extension_category ext_name with
- | Some (Ext_code_annot (Ext_here | Ext_next_loop)) -> false
- | Some (Ext_code_annot Ext_next_stmt) -> true
- | Some (Ext_code_annot Ext_next_both) -> not is_loop
- | Some (Ext_contract | Ext_global) | None ->
- Kernel.(
- warning ~wkey:wkey_acsl_extension
- "%s is not a code annotation extension" name);
- false)
+ | exception Not_found -> warn_not_a_code_annot () ; false
+ | Ext_code_annot (Ext_here | Ext_next_loop)-> false
+ | Ext_code_annot Ext_next_stmt-> true
+ | Ext_code_annot Ext_next_both-> not is_loop
+ | Ext_contract | Ext_global -> warn_not_a_code_annot () ; false)
| AAssert _ | AInvariant _ | AVariant _
| AAssigns _ | AAllocation _
| APragma (Slice_pragma (SPctrl | SPexpr _))
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index 7f9fb6810d409045fa5db13cd6df8e8acc8ff5ae..0e23bbe7a382f1ddf718b8d17b8b4cca4c755e76 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -614,28 +614,33 @@ module Base_checker = struct
match ca.annot_content with
| AExtended (_, is_loop, {ext_name}) ->
(match Logic_env.extension_category ext_name, is_loop with
- | Some (Ext_code_annot (Ext_next_stmt | Ext_next_both)), false ->
+ | exception Not_found ->
+ Kernel.(
+ warning ~wkey:wkey_acsl_extension
+ "%s is not a known extension" ext_name);
+ my_labels
+ | Ext_code_annot (Ext_next_stmt | Ext_next_both), false ->
Logic_const.post_label :: my_labels
- | Some (Ext_code_annot Ext_here), false -> my_labels
- | Some (Ext_code_annot (Ext_next_loop | Ext_next_both)), true ->
+ | Ext_code_annot Ext_here, false -> my_labels
+ | Ext_code_annot (Ext_next_loop | Ext_next_both), true ->
Logic_const.loop_current_label ::
Logic_const.loop_entry_label :: my_labels
- | Some (Ext_code_annot (Ext_here | Ext_next_stmt)), true ->
+ | Ext_code_annot (Ext_here | Ext_next_stmt), true ->
Kernel.(
warning ~wkey:wkey_acsl_extension
"%s is a code annotation extension, \
but used as a loop annotation" ext_name);
my_labels
- | Some (Ext_code_annot (Ext_next_loop)), false ->
+ | Ext_code_annot (Ext_next_loop), false ->
Kernel.(
warning ~wkey:wkey_acsl_extension
"%s is a loop annotation extension, \
but used as a code annotation" ext_name;
my_labels)
- | (Some (Ext_contract | Ext_global) | None), _ ->
+ | (Ext_contract | Ext_global), _ ->
Kernel.(
warning ~wkey:wkey_acsl_extension
- "%s is not a known code annotation extension" ext_name);
+ "%s is not a code annotation extension" ext_name);
my_labels)
| AAssert _ | AStmtSpec _ | AInvariant _ | AVariant _
| AAssigns _ | AAllocation _ | APragma _ -> my_labels
diff --git a/src/kernel_services/ast_queries/logic_env.ml b/src/kernel_services/ast_queries/logic_env.ml
index 5c09918e303db103dbf6ea685ef0c85b6638eb26..6d040a71c18ad8a29c375260c2aad8adcff4a595 100644
--- a/src/kernel_services/ast_queries/logic_env.ml
+++ b/src/kernel_services/ast_queries/logic_env.ml
@@ -24,15 +24,28 @@
open Cil_types
-let extensions = ref Datatype.String.Map.empty
-
-let is_extension s = Datatype.String.Map.mem s !extensions
-
-let extension_category s = Datatype.String.Map.find_opt s !extensions
-
-let register_extension s cat =
- if not (is_extension s) then
- extensions := Datatype.String.Map.add s cat !extensions
+module Extensions = struct
+ let initialized = ref false
+ let ref_is_extension = ref (fun _ -> assert false)
+ let ref_category = ref (fun _ -> assert false)
+ let ref_preprocess = ref (fun _ -> assert false)
+
+ let set_extension_handler ~category ~is_extension ~preprocess =
+ assert (not !initialized) ;
+ ref_is_extension := is_extension ;
+ ref_category := category ;
+ ref_preprocess := preprocess ;
+ initialized := true ;
+ ()
+
+ let is_extension s = !ref_is_extension s
+ let category s = !ref_category s
+ let preprocess s = !ref_preprocess s
+end
+let set_extension_handler = Extensions.set_extension_handler
+let is_extension = Extensions.is_extension
+let extension_category = Extensions.category
+let preprocess_extension = Extensions.preprocess
module CurrentLoc = Cil_const.CurrentLoc
diff --git a/src/kernel_services/ast_queries/logic_env.mli b/src/kernel_services/ast_queries/logic_env.mli
index afa488e5c8e8770e01b7c23807a6807a3df0fb41..c7570841b400b1bc0feb5487e81b31d3e6320f38 100644
--- a/src/kernel_services/ast_queries/logic_env.mli
+++ b/src/kernel_services/ast_queries/logic_env.mli
@@ -28,12 +28,12 @@ open Cil_types
(** {2 registered ACSL extensions } *)
-(** register a given name as a clause name for extended category. *)
-val register_extension: string -> ext_category -> unit
-
val is_extension: string -> bool
-val extension_category: string -> ext_category option
+val extension_category: string -> ext_category
+
+val preprocess_extension:
+ string -> Logic_ptree.lexpr list -> Logic_ptree.lexpr list
(** {2 Global Tables} *)
module Logic_info: State_builder.Hashtbl
@@ -204,6 +204,16 @@ val builtin_types_as_typenames: unit -> unit
(** {2 Internal use} *)
+val set_extension_handler:
+ category:(string -> ext_category) ->
+ is_extension:(string -> bool) ->
+ preprocess:(string -> Logic_ptree.lexpr list -> Logic_ptree.lexpr list) ->
+ unit
+(** Used to setup references related to the handling of ACSL extensions.
+ If your name is not [Acsl_extension], do not call this
+ @since Frama-C+dev
+*)
+
val init_dependencies: State.t -> unit
(** Used to postpone dependency of Lenv global tables wrt Cil_state, which
is initialized afterwards. *)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 08b217e0cc326183800bd3c00694e7c0eb695e18..3b44f67953dd8194a2ccbad07acfff9d4dce6823 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -525,56 +525,54 @@ type typing_context = {
}
module Extensions = struct
- let typer_tbl = Hashtbl.create 5
- let find_typer name = Hashtbl.find typer_tbl name
- let is_extension name = Hashtbl.mem typer_tbl name
- let register name category status typer =
- if is_extension name then
- Kernel.warning ~wkey:Kernel.wkey_acsl_extension
- "Trying to register ACSL extension %s twice. Ignoring second extension"
- name
- else begin
- Logic_env.register_extension name category;
- Hashtbl.add typer_tbl name (status,typer)
- end
+ let initialized = ref false
+ let ref_is_extension = ref (fun _ -> assert false)
+ let ref_typer = ref (fun _ _ _ _ -> assert false)
- let typer name ~typing_context:typing_context ~loc p =
- let status,typer =
- try find_typer name
- with Not_found ->
- Kernel.fatal ~source:(fst loc) "unsupported clause of name '%s'" name
- in
- let normal_error = ref false in
- let has_error () = normal_error := true in
- let wrapper =
- typing_context.on_error (typer ~typing_context ~loc) has_error
- in
- try
- status, wrapper p
- with
- | (Log.AbortError _ | Log.AbortFatal _) as exn -> raise exn
- | exn when not !normal_error ->
- Kernel.fatal "Typechecking ACSL extension %s raised exception %s"
- name (Printexc.to_string exn)
+ let set_handler ~is_extension ~typer =
+ assert (not !initialized) ;
+ ref_is_extension := is_extension ;
+ ref_typer := typer ;
+ initialized := true
+
+ let is_extension name = !ref_is_extension name
+
+ let typer name ~typing_context:typing_context ~loc =
+ !ref_typer name typing_context loc
+
+ (* For deprecated functions *)
+ let ref_deprecated_handler = ref (fun _ _ _ _ -> assert false)
+
+ let set_deprecated_handler ~handler =
+ ref_deprecated_handler := handler
+
+ let deprecated_register name category status typer =
+ let typer typing_context loc = typer ~typing_context ~loc in
+ !ref_deprecated_handler name category status typer
end
+let set_extension_handler = Extensions.set_handler
+
+(* Deprecated ACSL extensions functions *)
+let set_deprecated_extension_handler =
+ Extensions.set_deprecated_handler
let register_behavior_extension name f =
- Extensions.register name Ext_contract f
+ Extensions.deprecated_register name Ext_contract f
let register_global_extension name f =
- Extensions.register name Ext_global f
+ Extensions.deprecated_register name Ext_global f
let register_code_annot_extension name f =
- Extensions.register name (Ext_code_annot Ext_here) f
+ Extensions.deprecated_register name (Ext_code_annot Ext_here) f
let register_code_annot_next_stmt_extension name f =
- Extensions.register name (Ext_code_annot Ext_next_stmt) f
+ Extensions.deprecated_register name (Ext_code_annot Ext_next_stmt) f
let register_code_annot_next_loop_extension name f =
- Extensions.register name (Ext_code_annot Ext_next_loop) f
+ Extensions.deprecated_register name (Ext_code_annot Ext_next_loop) f
let register_code_annot_next_both_extension name f =
- Extensions.register name (Ext_code_annot Ext_next_both) f
+ Extensions.deprecated_register name (Ext_code_annot Ext_next_both) f
let rec arithmetic_conversion ty1 ty2 =
match unroll_type ty1, unroll_type ty2 with
@@ -3821,28 +3819,34 @@ struct
let kind = Logic_env.extension_category name in
let pre_state, post_state =
match kind,is_loop with
- | Some (Ext_code_annot Ext_here), false ->
+ | exception Not_found ->
+ Kernel.(
+ warning
+ ~source ~wkey:wkey_acsl_extension
+ "%s is not an extension" name);
+ code_annot_env (), fun _ -> Lenv.empty()
+ | Ext_code_annot Ext_here, false ->
code_annot_env (), fun _ -> Lenv.empty ()
- | Some (Ext_code_annot (Ext_next_stmt | Ext_next_both)), false ->
+ | Ext_code_annot (Ext_next_stmt | Ext_next_both), false ->
let env = append_old_and_post_labels (code_annot_env()) in
(env, function [Normal] -> env | _ -> Lenv.empty ())
- | Some (Ext_code_annot (Ext_next_loop | Ext_next_both)), true ->
+ | Ext_code_annot (Ext_next_loop | Ext_next_both), true ->
loop_annot_env(), fun _ -> Lenv.empty ()
- | Some (Ext_code_annot Ext_next_loop), false ->
+ | Ext_code_annot Ext_next_loop, false ->
Kernel.(
warning
~source ~wkey:wkey_acsl_extension
"%s is a loop annotation extension, \
but used here as code annotation" name);
code_annot_env (), fun _ -> Lenv.empty()
- | Some (Ext_code_annot (Ext_here | Ext_next_stmt)), true ->
+ | Ext_code_annot (Ext_here | Ext_next_stmt), true ->
Kernel.(
warning
~source ~wkey:wkey_acsl_extension
"%s is a code annotation extension, \
but used here as loop annotation" name);
code_annot_env (), fun _ -> Lenv.empty()
- | (Some (Ext_global | Ext_contract) | None),_ ->
+ | (Ext_global | Ext_contract),_ ->
Kernel.(
warning
~source ~wkey:wkey_acsl_extension
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index e6c6c5460f6373b9a5681550d8ec601875ac4e5d..4da856c7c0cb43c80edf19cdc615eafd77636d38 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -177,22 +177,26 @@ type typing_context = {
@since Carbon-20101201
@modify Silicon-20161101 change type of the function
@modify 19.0-Potassium add [status] argument
+ @deprecated Frama-C+dev
*)
val register_behavior_extension:
string -> bool ->
(typing_context:typing_context -> loc:location ->
Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
+[@@ deprecated "Use Acsl_extension.register_behavior instead"]
(** register an extension for global annotation.
@plugin development guide
@since 18.0-Argon
+ @deprecated Frama-C+dev
*)
val register_global_extension:
string -> bool ->
(typing_context:typing_context -> loc: location ->
Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
+[@@ deprecated "Use Acsl_extension.register_global instead"]
(** register an extension for code annotation to be evaluated at _current_
program point.
@@ -200,11 +204,13 @@ val register_global_extension:
@plugin development guide
@since 18.0-Argon
+ @deprecated Frama-C+dev
*)
val register_code_annot_extension:
string -> bool ->
(typing_context: typing_context -> loc: location ->
Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
+[@@ deprecated "Use Acsl_extension.register_code_annot instead"]
(** register an extension for code annotation to be evaluated for the _next_
statement.
@@ -212,22 +218,26 @@ val register_code_annot_extension:
@plugin development guide
@since 18.0-Argon
+ @deprecated Frama-C+dev
*)
val register_code_annot_next_stmt_extension:
string -> bool ->
(typing_context: typing_context -> loc: location ->
Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
+[@@ deprecated "Use Acsl_extension.register_code_annot_next_stmt instead"]
(** register an extension for loop annotation.
@plugin development guide
@since 18.0-Argon
+ @deprecated Frama-C+dev
*)
val register_code_annot_next_loop_extension:
string -> bool ->
(typing_context: typing_context -> loc: location ->
Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
+[@@ deprecated "Use Acsl_extension.register_code_annot_next_loop instead"]
(** register an extension both for code and loop annotations.
@@ -235,11 +245,13 @@ val register_code_annot_next_loop_extension:
@plugin development guide
@since 18.0-Argon
+ @deprecated Frama-C+dev
*)
val register_code_annot_next_both_extension:
string -> bool ->
(typing_context: typing_context -> loc: location ->
Logic_ptree.lexpr list -> acsl_extension_kind) -> unit
+[@@ deprecated "Use Acsl_extension.register_code_annot_next_both instead"]
module Make
(C :
@@ -371,6 +383,26 @@ val enter_post_state: Lenv.t -> termination_kind -> Lenv.t
val post_state_env: termination_kind -> logic_type -> Lenv.t
+(** {2 Internal use} *)
+
+val set_extension_handler:
+ is_extension:(string -> bool) ->
+ typer:(string -> typing_context -> location -> Logic_ptree.lexpr list ->
+ (bool * acsl_extension_kind)) ->
+ unit
+(** Used to setup references related to the handling of ACSL extensions.
+ If your name is not [Acsl_extension], do not call this
+ @since Frama-C+dev
+*)
+
+(**/**)
+val set_deprecated_extension_handler:
+ handler:(string -> ext_category -> bool ->
+ (typing_context -> location -> Logic_ptree.lexpr list ->
+ acsl_extension_kind) ->
+ unit) ->
+ unit
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/gui/filetree.ml b/src/plugins/gui/filetree.ml
index 6de5eb7f770e4a32d80c8f34ac81f9f89f7f50d1..92c21975c78aae90b60c2f0cb40f77779a794875 100644
--- a/src/plugins/gui/filetree.ml
+++ b/src/plugins/gui/filetree.ml
@@ -313,6 +313,7 @@ module MYTREE = struct
}
let global_name s = Pretty_utils.to_string Printer.pp_varname s
+ let extension_name e = Pretty_utils.to_string Printer.pp_short_extended e
let ga_name = function
| Dfun_or_pred (li, _) ->
@@ -325,7 +326,7 @@ module MYTREE = struct
| Dtype_annot (li, _) -> Some (global_name li.l_var_info.lv_name)
| Dmodel_annot (mf, _) -> Some (global_name mf.mi_name)
| Dcustom_annot _ -> Some "custom clause"
- | Dextended ({ext_name},_,_) -> Some ("ACSL extension " ^ ext_name)
+ | Dextended (e,_,_) -> Some ("ACSL extension " ^ (extension_name e))
let make_list_globals hide sort_order globs =
(* Association list binding names to globals. *)
diff --git a/src/plugins/value/utils/eva_annotations.ml b/src/plugins/value/utils/eva_annotations.ml
index 767cf487636ff235b6e01cd46d9b498eb3c9c624..6e60ba02654ba94bab07162cf19fbb78e24e21be 100644
--- a/src/plugins/value/utils/eva_annotations.ml
+++ b/src/plugins/value/utils/eva_annotations.ml
@@ -69,22 +69,19 @@ module Register (M : Annotation) =
struct
include M
- let typing_ext ~typing_context ~loc args =
+ let typer typing_context loc args =
try export (parse ~typing_context args)
with Parse_error ->
typing_context.Logic_typing.error loc "Invalid %s directive" name
- let printer_ext _pp fmt lp =
+ let printer _pp fmt lp =
print fmt (import lp)
let () =
- if is_loop_annot then begin
- Logic_typing.register_code_annot_next_loop_extension name false typing_ext;
- Cil_printer.register_loop_annot_extension name printer_ext
- end else begin
- Logic_typing.register_code_annot_next_stmt_extension name false typing_ext;
- Cil_printer.register_code_annot_extension name printer_ext
- end
+ if is_loop_annot then
+ Acsl_extension.register_code_annot_next_loop name typer ~printer false
+ else
+ Acsl_extension.register_code_annot_next_stmt name typer ~printer false
let get stmt =
let filter_add _emitter annot acc =
diff --git a/src/plugins/value/utils/widen_hints_ext.ml b/src/plugins/value/utils/widen_hints_ext.ml
index 743fc237c94b8db4fe15f4689cf34d6b9ec2da5c..4de7c3a8090fc8f346afa4bb45afdde942dbee6a 100644
--- a/src/plugins/value/utils/widen_hints_ext.ml
+++ b/src/plugins/value/utils/widen_hints_ext.ml
@@ -137,30 +137,30 @@ let widen_hint_terms_of_terms terms =
with
Invalid_hint -> None
-let () = Logic_typing.register_code_annot_next_both_extension "widen_hints" false
- (fun ~typing_context ~loc args ->
- let var_term, hint_terms =
- terms_of_parsed_widen_hints typing_context loc args
- in
- let terms = var_term :: hint_terms in
- Ext_terms terms
- )
-
-let () = Cil_printer.register_code_annot_extension "widen_hints"
- (fun _pp fmt ext ->
- match ext with
- | Ext_id _ -> assert false
- | Ext_preds _ -> assert false
- | Ext_terms terms ->
- match widen_hint_terms_of_terms terms with
- | Some (hint_lval, hint_terms) ->
- Format.fprintf fmt "%a%a, %a"
- (Pretty_utils.pp_list ~sep:" " ~suf:":" Format.pp_print_string)
- hint_lval.names pp_hvars hint_lval.vars
- (Pretty_utils.pp_list ~sep:", " Printer.pp_term) hint_terms
- | None ->
- Format.fprintf fmt "<invalid widen_hints>"
- )
+let typer typing_context loc args =
+ let var_term, hint_terms =
+ terms_of_parsed_widen_hints typing_context loc args
+ in
+ let terms = var_term :: hint_terms in
+ Ext_terms terms
+
+let printer _pp fmt ext =
+ match ext with
+ | Ext_id _ -> assert false
+ | Ext_preds _ -> assert false
+ | Ext_terms terms ->
+ match widen_hint_terms_of_terms terms with
+ | Some (hint_lval, hint_terms) ->
+ Format.fprintf fmt "%a%a, %a"
+ (Pretty_utils.pp_list ~sep:" " ~suf:":" Format.pp_print_string)
+ hint_lval.names pp_hvars hint_lval.vars
+ (Pretty_utils.pp_list ~sep:", " Printer.pp_term) hint_terms
+ | None ->
+ Format.fprintf fmt "<invalid widen_hints>"
+
+let () =
+ Acsl_extension.register_code_annot_next_both
+ "widen_hints" typer ~printer false
let get_widen_hints_annots stmt =
Annotations.fold_code_annot
diff --git a/src/plugins/wp/RegionAnnot.ml b/src/plugins/wp/RegionAnnot.ml
index 5ada4f4dc9434380e19dfa9d69147f562c6ecb12..b50e79470f8aeb6aff210abce0198e507f367bb4 100644
--- a/src/plugins/wp/RegionAnnot.ml
+++ b/src/plugins/wp/RegionAnnot.ml
@@ -440,7 +440,7 @@ let rec parse_region env p =
let path = parse_lpath env p in
env.paths <- path :: env.paths
-let typecheck ~typing_context ~loc:_loc ps =
+let typecheck typing_context _loc ps =
let env = {
name = None ;
declared = [] ;
@@ -484,10 +484,8 @@ let register () =
if Wp.Region.get () || Wp.Region_annot.get () ||
List.exists specified (Wp.Model.get ())
then
- begin
- Logic_typing.register_behavior_extension "region" true typecheck ;
- Cil_printer.register_behavior_extension "region" pp_extension ;
- end
+ Acsl_extension.register_behavior
+ "region" typecheck ~printer:pp_extension false
let () = Cmdline.run_after_configuring_stage register
diff --git a/src/plugins/wp/dyncall.ml b/src/plugins/wp/dyncall.ml
index 8b0dedf82a8033484a5732a5f6ae3d59563ff7c9..06b27c6e5df7951b731e9bca88a990f5e5645581 100644
--- a/src/plugins/wp/dyncall.ml
+++ b/src/plugins/wp/dyncall.ml
@@ -37,7 +37,7 @@ let find_call env loc f =
with Not_found ->
env.error loc "Unknown function '%s'" f
-let typecheck ~typing_context ~loc ps =
+let typecheck typing_context loc ps =
ignore loc ;
let fs =
List.map
@@ -261,8 +261,8 @@ let register =
if (not !once) &&
Wp_parameters.DynCall.get () then begin
once := true;
- Logic_typing.register_code_annot_next_stmt_extension "calls" true typecheck;
- Logic_typing.register_behavior_extension "instanceof" true typecheck ;
+ Acsl_extension.register_code_annot_next_stmt "calls" typecheck true ;
+ Acsl_extension.register_behavior "instanceof" typecheck true ;
end
let () = Cmdline.run_after_configuring_stage register
diff --git a/tests/spec/Extend.ml b/tests/spec/Extend.ml
index af9696e583520f9dcabb3cbdf15118eeb53e1d7d..99c5ea7064b6b8ad3de11702dafa936b3320e5e6 100644
--- a/tests/spec/Extend.ml
+++ b/tests/spec/Extend.ml
@@ -2,8 +2,7 @@ open Logic_ptree
open Cil_types
open Logic_typing
-let type_foo ~typing_context ~loc l =
- let _loc = loc in
+let type_foo typing_context _loc l =
let preds =
List.map
(typing_context.type_predicate
@@ -24,8 +23,7 @@ module Bar_table =
let size = 3
end)
-let type_bar ~typing_context ~loc l =
- let _loc = loc in
+let type_bar typing_context _loc l =
let i = Count.next() in
let p =
List.map
@@ -61,7 +59,7 @@ let visit_bar vis ext =
| Ext_terms _ | Ext_preds _ ->
Kernel.fatal "bar extension should have ids as arguments"
-let type_baz ~typing_context ~loc:_loc l =
+let type_baz typing_context _loc l =
let t =
List.map
(typing_context.type_term typing_context typing_context.pre_state) l
@@ -88,7 +86,7 @@ let add_builtin () =
let () = add_builtin ()
-let type_bla ~typing_context ~loc:_loc l =
+let type_bla typing_context _loc l =
let type_predicate ctxt env p =
match p.lexpr_node with
| PLapp("\\trace", [], [pred]) ->
@@ -107,16 +105,15 @@ let type_bla ~typing_context ~loc:_loc l =
Ext_preds l
let () =
- Logic_typing.register_behavior_extension "foo" false type_foo;
- Logic_typing.register_behavior_extension "bar" false type_bar;
- Logic_typing.register_behavior_extension "bla" false type_bla;
- Cil_printer.register_behavior_extension "bar" print_bar;
- Cil.register_behavior_extension "bar" visit_bar;
- Logic_typing.register_code_annot_next_both_extension "baz" false type_baz;
- Logic_typing.register_code_annot_next_loop_extension "lfoo" false type_foo;
- Logic_typing.register_code_annot_extension "ca_foo" false type_foo;
- Logic_typing.register_code_annot_next_stmt_extension "ns_foo" false type_foo;
- Logic_typing.register_global_extension "global_foo" false type_foo
+ Acsl_extension.register_behavior "foo" type_foo false ;
+ Acsl_extension.register_code_annot_next_loop "lfoo" type_foo false ;
+ Acsl_extension.register_code_annot "ca_foo" type_foo false ;
+ Acsl_extension.register_code_annot_next_stmt "ns_foo" type_foo false ;
+ Acsl_extension.register_global "global_foo" type_foo false ;
+ Acsl_extension.register_behavior
+ "bar" type_bar ~printer:print_bar ~visitor:visit_bar false ;
+ Acsl_extension.register_behavior "bla" type_bla false ;
+ Acsl_extension.register_code_annot_next_both "baz" type_baz false
let run () =
Ast.compute ();
diff --git a/tests/spec/Extend_preprocess.i b/tests/spec/Extend_preprocess.i
new file mode 100644
index 0000000000000000000000000000000000000000..24b2d061048798182dd865eb746bead6b33d6fa9
--- /dev/null
+++ b/tests/spec/Extend_preprocess.i
@@ -0,0 +1,31 @@
+/* run.config
+MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+OPT: -no-autoload-plugins -kernel-warn-key=annot-error=active -print
+*/
+
+/*@ bhv_foo must_replace(x); */
+int f(int x);
+
+/*@ behavior test:
+ bhv_foo must_replace(x);
+*/
+int g(int x);
+
+
+int f(int x) {
+ int s = 0;
+ /*@ loop nl_foo must_replace(x); */
+ for (int i = 0; i < x; i++) s+=g(i);
+ /*@ ca_foo must_replace(x); */
+ return s;
+}
+
+int k(int z) {
+ int x = z;
+ int y = 0;
+ /*@ ns_foo must_replace(x); */
+ y = x++;
+ return y;
+}
+
+/*@ gl_foo must_replace(x); */
diff --git a/tests/spec/Extend_preprocess.ml b/tests/spec/Extend_preprocess.ml
new file mode 100644
index 0000000000000000000000000000000000000000..51e60d554404dca8e533abfada8cadc183efc44c
--- /dev/null
+++ b/tests/spec/Extend_preprocess.ml
@@ -0,0 +1,53 @@
+open Logic_ptree
+open Logic_const
+
+(* For each kind of extension:
+ - behavior: bhv
+ - next loop: nl
+ - code annotation: ca
+ - next statement: ns
+ - global: gl
+ replaces node "must_replace(x)" with "<kind>_ok(x)". The typing phase
+ validates that we find the right "<kind>_ok" for each kind of extension:
+ - if a must_replace is found, it fails,
+ - if the wrong kind is found, a "\false" is generated
+ - if everything is ok "\true" is generated
+*)
+
+let validate kind call =
+ assert (not (String.equal "must_replace" call)) ;
+ match String.split_on_char '_' call with
+ | [ lkind ; lok ] -> String.equal kind lkind && String.equal lok "ok"
+ | _ -> false
+
+let ext_typing kind typing_context loc l =
+ let _ = loc in
+ let _ = typing_context in
+ let type_lexpr = function
+ | { lexpr_node = PLapp(s, [], [ _ ]) } when validate kind s -> ptrue
+ | _ -> pfalse
+ in
+ Cil_types.Ext_preds (List.map type_lexpr l)
+
+let preprocess_foo_ptree_element kind = function
+ | { lexpr_node = PLapp("must_replace", [], [ v ]) } as x ->
+ { x with lexpr_node = PLapp(kind ^ "_ok", [], [ v ]) }
+ | x -> x
+
+let preprocess_foo_ptree kind = List.map (preprocess_foo_ptree_element kind)
+
+let register registration ?visitor ?printer ?short_printer kind =
+ let registration ?preprocessor typer =
+ registration
+ (kind ^ "_foo") ?preprocessor typer ?visitor ?printer ?short_printer false
+ in
+ registration ~preprocessor:(preprocess_foo_ptree kind) (ext_typing kind)
+
+
+let () =
+ let open Acsl_extension in
+ register register_behavior "bhv";
+ register register_code_annot_next_loop "nl";
+ register register_code_annot "ca";
+ register register_code_annot_next_stmt "ns";
+ register register_global "gl"
diff --git a/tests/spec/Extend_short_print.i b/tests/spec/Extend_short_print.i
new file mode 100644
index 0000000000000000000000000000000000000000..568f3561f8b22dbb8022ed9baed7acb122ed7f0e
--- /dev/null
+++ b/tests/spec/Extend_short_print.i
@@ -0,0 +1,9 @@
+/* run.config
+EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+OPT: -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+*/
+
+/*@
+ without_short \true ;
+ has_short \true ;
+*/
\ No newline at end of file
diff --git a/tests/spec/Extend_short_print.ml b/tests/spec/Extend_short_print.ml
new file mode 100644
index 0000000000000000000000000000000000000000..386cc1080b5165c554a3b574e3b3834605e35360
--- /dev/null
+++ b/tests/spec/Extend_short_print.ml
@@ -0,0 +1,14 @@
+open Cil_types
+
+let typer _context _loc _tree = Ext_id 42
+let short_printer _printer fmt _kind = Format.fprintf fmt "HS: some content"
+
+let () =
+ Acsl_extension.register_global "without_short" typer false ;
+ Acsl_extension.register_global "has_short" typer ~short_printer false
+
+let process_global _ = function
+ | Dextended(e, _, _) -> Kernel.feedback "%a" Cil_printer.pp_short_extended e
+ | _ -> ()
+
+let () = Db.Main.extend (fun () -> Annotations.iter_global process_global)
\ No newline at end of file
diff --git a/tests/spec/extend_extern.ml b/tests/spec/extend_extern.ml
index c60a714b9bf921abd03047c7e87337548365b108..50dc6941ce3f3691e515f2d9bc04f59f1db844c9 100644
--- a/tests/spec/extend_extern.ml
+++ b/tests/spec/extend_extern.ml
@@ -6,7 +6,7 @@ let load_theory = function
raise Not_found
| _ -> assert false
-let typing ~typing_context ~loc lexprs =
+let typer typing_context loc lexprs =
ignore loc ;
let type_predicate =
typing_context.type_predicate typing_context (Lenv.empty ())
@@ -17,7 +17,7 @@ let typing ~typing_context ~loc lexprs =
let () =
- Logic_typing.register_global_extension "why3" false typing
+ Acsl_extension.register_global "why3" typer false
let main () =
try
diff --git a/tests/spec/oracle/Extend_preprocess.res.oracle b/tests/spec/oracle/Extend_preprocess.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..843b1e4bc8d731e44039e38c89f3c20b99510e88
--- /dev/null
+++ b/tests/spec/oracle/Extend_preprocess.res.oracle
@@ -0,0 +1,43 @@
+[kernel] Parsing tests/spec/Extend_preprocess.i (no preprocessing)
+/* Generated by Frama-C */
+int f(int x);
+
+/*@ behavior test:
+ bhv_foo \true; */
+int g(int x);
+
+/*@ bhv_foo \true; */
+int f(int x)
+{
+ int s = 0;
+ {
+ int i = 0;
+ /*@ loop nl_foo \true; */
+ while (i < x) {
+ int tmp;
+ tmp = g(i);
+ s += tmp;
+ i ++;
+ }
+ }
+ /*@ ca_foo \true; */ ;
+ return s;
+}
+
+int k(int z)
+{
+ int tmp;
+ int x = z;
+ int y = 0;
+ /*@ ns_foo \true; */
+ { /* sequence */
+ tmp = x;
+ x ++;
+ y = tmp;
+ }
+ return y;
+}
+
+/*@ gl_foo \true;
+*/
+
diff --git a/tests/spec/oracle/Extend_short_print.res.oracle b/tests/spec/oracle/Extend_short_print.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a44980575a80753ebf40c3733a19109048fe3203
--- /dev/null
+++ b/tests/spec/oracle/Extend_short_print.res.oracle
@@ -0,0 +1,3 @@
+[kernel] Parsing tests/spec/Extend_short_print.i (no preprocessing)
+[kernel] HS: some content
+[kernel] without_short