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 243757e9f388daf4411627f064d4dad8ddc2bd4f..cb3068846b093a6a5f2efe1e807fda896318128d 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -1392,15 +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)) ->
- let processed = Logic_env.preprocess_extension ext $3 in
- (ext, processed)
- | 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
}
@@ -1447,17 +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)) ->
- let processed = Logic_env.preprocess_extension ext $2 in
- Logic_ptree.AExtended(bhvs,false,(ext,processed))
- | 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
}
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_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index 0d3a497fd012a1238b8300b935d622f095d71385..ade873ecd952aa4710c8b03a9c3d3c139d9f327f 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -64,8 +64,9 @@ module Extensions = struct
with Not_found ->
Kernel.fatal ~current:true "unsupported clause of name '%s'" name
- let category name =
- Extlib.opt_map (fun e -> e.category) (Hashtbl.find_opt ext_tbl 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
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.mli b/src/kernel_services/ast_queries/logic_env.mli
index 3cf0a69b6a2c3cf03211a3b319edae1b98640f88..c7570841b400b1bc0feb5487e81b31d3e6320f38 100644
--- a/src/kernel_services/ast_queries/logic_env.mli
+++ b/src/kernel_services/ast_queries/logic_env.mli
@@ -30,7 +30,7 @@ open Cil_types
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
@@ -205,7 +205,7 @@ val builtin_types_as_typenames: unit -> unit
(** {2 Internal use} *)
val set_extension_handler:
- category:(string -> ext_category option) ->
+ category:(string -> ext_category) ->
is_extension:(string -> bool) ->
preprocess:(string -> Logic_ptree.lexpr list -> Logic_ptree.lexpr list) ->
unit
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index e7f783a7582d7dc2a2ae0ecb9e21932f47778aec..3b44f67953dd8194a2ccbad07acfff9d4dce6823 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3819,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