diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index 876f7d98eb124a74204704059a26eb1561ba2225..e218020b3eeff9a0864db565efb08e7e9f6941fb 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -305,6 +305,37 @@
| ADMIT, INVARIANT -> true, ADMIT_INVARIANT
| ADMIT, LEMMA -> true, ADMIT_LEMMA
| _ -> false, current
+
+ let type_to_string = function
+ | TYPENAME s -> s
+ | REAL -> "real"
+ | BOOLEAN -> "boolean"
+ | INTEGER -> "integer"
+ | _ -> assert false
+
+ let check_ext_plugin source plugin tok =
+ match tok with
+ | IDENTIFIER s ->
+ if Plugin.is_present plugin then
+ Kernel.warning ~once:true ~wkey:Kernel.wkey_extension_unknown ~source
+ "Unregistered extension %s for plug-in %s" s plugin
+ else
+ Kernel.warning ~once:true ~wkey:Kernel.wkey_plugin_not_loaded ~source
+ "Ignored extensions for unregistered plug-in %s" plugin;
+ IDENTIFIER_EXT s
+ | EXT_CODE_ANNOT s
+ | EXT_GLOBAL s
+ | EXT_GLOBAL_BLOCK s
+ | EXT_CONTRACT s ->
+ let plugin_from = Logic_env.extension_from s in
+ if plugin_from <> plugin then
+ Kernel.abort ~source
+ "Extension %s is from %s and not %s" s plugin_from plugin;
+ tok
+ | _ ->
+ Kernel.abort ~source
+ "Type token \'%s\' received instead of extension identifier"
+ (type_to_string tok)
}
let space = [' ' '\t' '\012' '\r' '@' ]
@@ -341,7 +372,12 @@ rule token = parse
then comment lexbuf
else lex_error lexbuf "unexpected block-comment opening"
}
-
+ | '\\' ((rL (rL | rD)*) as plugin) "::" ((rL (rL | rD)*) as name) {
+ let loc = Lexing.(lexeme_start_p lexbuf, lexeme_end_p lexbuf) in
+ let cabsloc = Cil_datatype.Location.of_lexing_loc loc in
+ let tok = identifier name cabsloc in
+ check_ext_plugin (fst cabsloc) plugin tok
+ }
| '\\' rL (rL | rD)* { bs_identifier lexbuf }
| rL (rL | rD)* {
let loc = Lexing.(lexeme_start_p lexbuf, lexeme_end_p lexbuf) in
@@ -558,9 +594,12 @@ and comment = parse
| Logic_utils.Not_well_formed (loc, m) ->
output ~source:(fst loc) "%s" m;
None
+ | Logic_utils.Unknown_ext ->
+ None
| Log.FeatureRequest(source,_,msg) ->
let source = Option.value ~default:(Cil_datatype.Position.of_lexing_pos lb.lex_curr_p) source in
output ~source "unimplemented ACSL feature: %s" msg; None
+ | Log.AbortError _ as exn -> raise exn
| exn ->
Kernel.fatal ~source:(Cil_datatype.Position.of_lexing_pos lb.lex_curr_p) "Unknown error (%s)"
(Printexc.to_string exn)
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 134784e743d6d646456171bac3f2d4f957c20cee..cafa0e96b6bf360f0c103ca51cdb542520381f07 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -254,7 +254,7 @@
%token MODULE FUNCTION CONTRACT INCLUDE EXT_AT EXT_LET
/* ACSL extension for external spec file */
-%token <string> IDENTIFIER TYPENAME
+%token <string> IDENTIFIER TYPENAME IDENTIFIER_EXT
%token <bool*string> STRING_LITERAL
%token <string> INT_CONSTANT
%token <string> FLOAT_CONSTANT
@@ -917,8 +917,13 @@ full_identifier:
| id = EXT_CONTRACT { id }
| id = EXT_GLOBAL { id }
| id = EXT_GLOBAL_BLOCK { id }
+| id = IDENTIFIER_EXT { id }
;
+%inline unknown_extension:
+| id=IDENTIFIER_EXT content=extension_content { (id,content) }
+
+
/*** ACSL extension for external spec file ***/
ext_spec:
@@ -1052,7 +1057,7 @@ spec:
contract:
| requires terminates decreases simple_clauses behaviors complete_or_disjoint
{ let requires=$1 in
- let (allocation,assigns,post_cond,extended) = $4 in
+ let (empty,(allocation,assigns,post_cond,extended)) = $4 in
let behaviors = $5 in
let (completes,disjoints) = $6 in
let behaviors =
@@ -1066,7 +1071,11 @@ contract:
else if $2<>None || $3<>None ||
behaviors<>[] || completes<>[] ||disjoints<>[]
then behaviors
- else raise (Not_well_formed (loc $sloc,"Empty annotation is not allowed"))
+ else
+ if empty then
+ raise (Not_well_formed (loc $sloc,"Empty annotation is not allowed"))
+ else
+ raise Unknown_ext
in
{ spec_terminates = $2;
spec_variant = $3;
@@ -1137,6 +1146,7 @@ clause_kw:
| COMPLETE {"complete"}
| DISJOINT {"disjoint"}
| EXT_CONTRACT { $1 }
+| id=IDENTIFIER_EXT { id }
| EOF { "end of annotation" }
;
@@ -1180,8 +1190,8 @@ variant:
;
simple_clauses:
-| /* epsilon */ { FreeAllocAny,WritesAny,[],[] }
-| ne_simple_clauses { $1 }
+| /* epsilon */ { true,(FreeAllocAny,WritesAny,[],[]) }
+| ne_simple_clauses { false,$1 }
;
allocation:
@@ -1191,21 +1201,22 @@ allocation:
ne_simple_clauses:
| post_cond_kind lexpr SEMICOLON simple_clauses
{ let tp_kind, kind = $1 in
- let allocation,assigns,post_cond,extended = $4 in
+ let allocation,assigns,post_cond,extended = snd $4 in
allocation,assigns,
((kind,toplevel_pred tp_kind $2)::post_cond),extended }
| allocation SEMICOLON simple_clauses
- { let allocation,assigns,post_cond,extended = $3 in
+ { let allocation,assigns,post_cond,extended = snd $3 in
let a = concat_allocation allocation $1 in
a,assigns,post_cond,extended
}
| ASSIGNS assigns SEMICOLON simple_clauses
- { let allocation,assigns,post_cond,extended = $4 in
+ { let allocation,assigns,post_cond,extended = snd $4 in
let a = concat_assigns $sloc assigns $2
in allocation,a,post_cond,extended
}
+| unknown_extension SEMICOLON simple_clauses { snd $3 }
| EXT_CONTRACT extension_content SEMICOLON simple_clauses
- { let allocation,assigns,post_cond,extended = $4 in
+ { let allocation,assigns,post_cond,extended = snd $4 in
let processed = Logic_env.preprocess_extension $1 $2 in
allocation,assigns,post_cond,($1,processed)::extended
}
@@ -1246,7 +1257,7 @@ ne_behaviors:
;
behavior_body:
-| assumes requires simple_clauses { $1,$2,$3 }
+| assumes requires simple_clauses { $1,$2,snd $3 }
| assumes ne_requires ASSUMES
{ clause_order $loc($3) "assumes" "requires" }
| assumes requires ne_simple_clauses ASSUMES
@@ -1319,6 +1330,7 @@ annotation:
}
| identifier { Aattribute_annot (loc $sloc, $1) }
| BSGHOST { Aattribute_annot(loc $sloc,"\\ghost") }
+| unknown_extension SEMICOLON { raise Unknown_ext }
;
contract_or_code_annotation:
@@ -1396,6 +1408,7 @@ loop_annot_stack:
let (i,fa,a,b,v,p,e) = $2 in
(i,fa,a,b,v,p, $1::e)
}
+| LOOP unknown_extension SEMICOLON loop_annot_opt { $4 }
;
loop_annot_opt:
@@ -1542,7 +1555,7 @@ impact_pragma:
decl_list:
| decl { [loc_decl $sloc $1] }
-| decl decl_list { (loc_decl $loc($1) $1) :: $2 }
+| decl decl_list { (loc_decl $sloc $1) :: $2 }
;
decl:
@@ -1572,6 +1585,7 @@ ext_decl:
ext_decls:
| /* epsilon */
{ [] }
+| unknown_extension SEMICOLON ext_decls { $3 }
| ext_decl_loc ext_decls
{ $1::$2 }
;
@@ -1932,7 +1946,7 @@ post_cond:
is_acsl_spec:
| post_cond { snd $1 }
-| EXT_CONTRACT { $1 }
+| EXT_CONTRACT { $1 }
| ASSIGNS { "assigns" }
| ALLOCATES { "allocates" }
| FREES { "frees" }
@@ -1948,8 +1962,9 @@ is_acsl_spec:
is_acsl_decl_or_code_annot:
| EXT_CODE_ANNOT { $1 }
-| EXT_GLOBAL { $1 }
-| EXT_GLOBAL_BLOCK { $1 }
+| EXT_GLOBAL { $1 }
+| EXT_GLOBAL_BLOCK { $1 }
+| IDENTIFIER_EXT { $1 }
| ASSUMES { "assumes" }
| ASSERT { "assert" }
| CHECK { "check" }
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 5a8bd35caa31c3a9c990ecd4b123eab7163f4183..976d4f69902446793d8abf72bb75bdb15cd283fb 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -27,6 +27,7 @@ open Logic_const
open Cil_types
exception Not_well_formed of Cil_types.location * string
+exception Unknown_ext
let rec unroll_type ?(unroll_typedef=true) = function
| Ltype (tdef,_) as ty when Logic_const.is_unrollable_ltdef tdef ->
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index 9b9b0fac15224c8cfd0d899fcbb7b6337541c7ed..f17f5537f1b23fd4859c3f0f83ae960394f0ddc1 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -31,6 +31,9 @@ open Cil_types
syntactically not well-formed. *)
exception Not_well_formed of location * string
+(** exception raised when an unknown extension is called. *)
+exception Unknown_ext
+
(** basic utilities for logic terms and predicates. See also {! Logic_const}
to build terms and predicates.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 2cb8ce7036c7ed6070986cfa77a41c82064e7e7e..3bc9e2dc019e439fe3e8d918e0f172fbc419db0a 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -142,6 +142,12 @@ let dkey_visitor = register_category "visitor"
let wkey_annot_error = register_warn_category "annot-error"
let () = set_warn_status wkey_annot_error Log.Wabort
+let wkey_plugin_not_loaded = register_warn_category "plugin-not-loaded"
+let () = set_warn_status wkey_plugin_not_loaded Log.Wactive
+
+let wkey_extension_unknown = register_warn_category "extension-unknown"
+let () = set_warn_status wkey_extension_unknown Log.Werror
+
let wkey_ghost_already_ghost = register_warn_category "ghost:already-ghost"
let () = set_warn_status wkey_ghost_already_ghost Log.Wfeedback
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 21bc5342c779a0b5452235e65f16ec4ec46cadfa..5ad4840fcc27d9c0f5d602a70ab5993014731006 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -143,6 +143,12 @@ val dkey_visitor: category
val wkey_annot_error: warn_category
(** error in annotation. If only a warning, annotation will just be ignored. *)
+val wkey_plugin_not_loaded: warn_category
+(** Warning related to unloaded plugin. *)
+
+val wkey_extension_unknown: warn_category
+(** Warning related to the use of an unregistered ACSL extension. *)
+
val wkey_ghost_already_ghost: warn_category
(** ghost element is qualified with \ghost while this is already the case
by default *)