diff --git a/src/plugins/eva/utils/export.ml b/src/plugins/eva/utils/export.ml index a4b5b21de6b0f4a430beaadf04c482e92e1fc7f0..30c2168756cbb1c2fe15332c85cb97b1f5b17c23 100644 --- a/src/plugins/eva/utils/export.ml +++ b/src/plugins/eva/utils/export.ml @@ -72,7 +72,7 @@ let predicate ~loc ?(name=[]) (p : pred) : predicate = let ts = List.map (Exp.cil_term ~loc) es in let ls = Logic_env.find_all_logic_functions f in match List.find_opt (matches_params ts) ls with - | None -> raise (Invalid_argument ("Eva.Annot." ^ f)) + | None -> invalid_arg "Eva.Export.predicate" | Some li -> Logic_const.papp ~loc (li,[],ts) in { (aux p) with pred_name = name } @@ -333,26 +333,30 @@ let cleaner () = (new cleaner :> visitor) (* -------------------------------------------------------------------------- *) let main () = - if Analysis.is_computed () then - let ast = Ast.get () in - let cleaner = cleaner () in - Self.feedback ~ontty:`Transient "Cleaning annotations..." ; - Visitor.visitFramacFile cleaner ast ; - let generator = new generator in - Parameters.Annot.iter - begin fun kf -> - if Kernel_function.has_definition kf then - if Results.are_available kf then - let fundec = Kernel_function.get_definition kf in - Self.feedback "Annotate %a" Kernel_function.pretty kf ; - ignore @@ Visitor.visitFramacFunction generator fundec - else - Self.warning "Can not annotate %a (no available results)" - Kernel_function.pretty kf + let generator = lazy + begin + Analysis.compute () ; + let ast = Ast.get () in + let cleaner = cleaner () in + Self.feedback ~ontty:`Transient "Cleaning annotations..." ; + Visitor.visitFramacFile cleaner ast ; + new generator + end + in Parameters.Annot.iter + begin fun kf -> + let generator = Lazy.force generator in + if Kernel_function.has_definition kf then + if Results.are_available kf then + let fundec = Kernel_function.get_definition kf in + Self.feedback "Annotate %a" Kernel_function.pretty kf ; + ignore @@ Visitor.visitFramacFunction generator fundec else - Self.warning "Can not annotate %a (no definition)" + Self.warning "Can not annotate %a (no available results)" Kernel_function.pretty kf - end + else + Self.warning "Can not annotate %a (no definition)" + Kernel_function.pretty kf + end let () = Boot.Main.extend main