diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll index 7ee0a95513431c6c8a0df8879e402e7d6403537d..b58bfc4398cd718369747071d1b74b11581cc2d0 100644 --- a/src/kernel_internals/parsing/logic_lexer.mll +++ b/src/kernel_internals/parsing/logic_lexer.mll @@ -570,8 +570,9 @@ and comment = parse | Logic_utils.Not_well_formed (loc, m) -> output ~source:(fst loc) "%s" m; None - | Log.FeatureRequest(_,_,msg) -> - output ~source:(Cil_datatype.Position.of_lexing_pos lb.lex_curr_p) "unimplemented ACSL feature: %s" msg; 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 | 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_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml index acdcb97f4f8e164586cf04ede5818b183dbf9f07..1c6ad6e42edee54bc38398b71ff62daa79b08a36 100644 --- a/src/kernel_services/ast_queries/logic_utils.ml +++ b/src/kernel_services/ast_queries/logic_utils.ml @@ -417,7 +417,8 @@ let float_builtin prefix fkind = let name = match fkind with | FFloat -> Printf.sprintf "\\%s_float" prefix | FDouble -> Printf.sprintf "\\%s_double" prefix - | FLongDouble -> Kernel.not_yet_implemented "Builtins for long double type" + | FLongDouble -> + Kernel.not_yet_implemented ~current:true "Builtins for long double type" in match Logic_env.find_all_logic_functions name with | [ lf ] -> Some lf | _ -> Kernel.fatal "Missing or ambiguous builtin %S" name diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml index fc7aacc658214ccbc139ecf745e927da4faa72c9..edcb31d89330c83fb2d3cc470127fc24ac851fc1 100644 --- a/src/plugins/pdg/build.ml +++ b/src/plugins/pdg/build.ml @@ -1024,9 +1024,9 @@ let compute_pdg kf = | Pdg_state.Cannot_fold -> Pdg_parameters.warning "too imprecise value analysis : abort" ; degenerated true kf - | Log.FeatureRequest (_source, who, what) -> + | Log.FeatureRequest (source, who, what) -> (* [JS 2012/08/24] nobody should catch this exception *) - Pdg_parameters.warning "not implemented by %s yet: %s" who what ; + Pdg_parameters.warning ?source "not implemented by %s yet: %s" who what; degenerated true kf (*