Skip to content
Snippets Groups Projects
Commit 7a9c5718 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] slight refactoring of command-line run

parent 15583fa9
No related branches found
No related tags found
No related merge requests found
......@@ -759,49 +759,48 @@ let dkey_refusage = Wp_parameters.register_category "refusage"
let dkey_builtins = Wp_parameters.register_category "builtins"
let cmdline_run () =
let wp_main fct =
Wp_parameters.feedback ~ontty:`Feedback "Running WP plugin...";
Ast.compute ();
Dyncall.compute ();
if Wp_parameters.has_dkey dkey_logicusage then
begin
LogicUsage.compute ();
LogicUsage.dump ();
end ;
if Wp_parameters.has_dkey dkey_refusage then
begin
RefUsage.compute ();
RefUsage.dump ();
end ;
let bhv = Wp_parameters.Behaviors.get () in
let prop = Wp_parameters.Properties.get () in
(** TODO entry point *)
let computer = computer () in
if Wp_parameters.has_dkey dkey_builtins then
begin
WpContext.on_context (computer#model,WpContext.Global)
LogicBuiltins.dump ();
end ;
wp_compute_memory_context computer#model ;
if Wp_parameters.CheckModelHypotheses.get () then
wp_insert_memory_context computer#model fct ;
Generator.compute_selection computer ~fct ~bhv ~prop ()
in
if Wp_parameters.CachePrint.get () then
Kernel.feedback "Cache directory: %s" (Cache.get_dir ()) ;
let fct = Wp_parameters.get_wp () in
if fct <> Wp_parameters.Fct_none then
begin
let goals = wp_main fct in
do_wp_proofs goals ;
begin
if Wp_parameters.CachePrint.get () then
Kernel.feedback "Cache directory: %s" (Cache.get_dir ()) ;
let fct = Wp_parameters.get_fct () in
if fct <> Wp_parameters.Fct_none then
begin
if fct <> Wp_parameters.Fct_all then
do_wp_print_for goals
else
do_wp_print () ;
end ;
do_wp_report () ;
end
Wp_parameters.feedback ~ontty:`Feedback "Running WP plugin...";
Ast.compute ();
Dyncall.compute ();
if Wp_parameters.has_dkey dkey_logicusage then
begin
LogicUsage.compute ();
LogicUsage.dump ();
end ;
if Wp_parameters.has_dkey dkey_refusage then
begin
RefUsage.compute ();
RefUsage.dump ();
end ;
let bhv = Wp_parameters.Behaviors.get () in
let prop = Wp_parameters.Properties.get () in
(** TODO entry point *)
let computer = computer () in
if Wp_parameters.has_dkey dkey_builtins then
begin
WpContext.on_context (computer#model,WpContext.Global)
LogicBuiltins.dump ();
end ;
wp_compute_memory_context computer#model ;
if Wp_parameters.CheckModelHypotheses.get () then
wp_insert_memory_context computer#model fct ;
let goals = Generator.compute_selection computer ~fct ~bhv ~prop () in
do_wp_proofs goals ;
begin
if fct <> Wp_parameters.Fct_all then
do_wp_print_for goals
else
do_wp_print () ;
end ;
do_wp_report () ;
end
end
(* ------------------------------------------------------------------------ *)
(* --- Register external functions --- *)
......
......@@ -155,21 +155,20 @@ let iter_fct phi = function
(fun kf -> if not (Fct.mem kf fs) then phi kf)
| Fct_list fs -> Fct.iter phi fs
let get_kf () =
let get_kfs () =
if Functions.is_empty() then
if SkipFunctions.is_empty () then Fct_all
else Fct_skip (SkipFunctions.get())
else
Fct_list (Fct.diff (Functions.get()) (SkipFunctions.get()))
let get_wp () =
let get_fct () =
if WP.get () || not (Functions.is_empty()) ||
not (Behaviors.is_empty()) || not (Properties.is_empty())
then get_kf ()
then get_kfs ()
else Fct_none
let iter_wp f = iter_fct f (get_wp ())
let iter_kf f = iter_fct f (get_kf ())
let iter_kf f = iter_fct f (get_fct ())
(* ------------------------------------------------------------------------ *)
(* --- Memory Models --- *)
......
......@@ -32,11 +32,9 @@ type functions =
| Fct_skip of Cil_datatype.Kf.Set.t
| Fct_list of Cil_datatype.Kf.Set.t
val get_kf : unit -> functions
val get_wp : unit -> functions
val get_fct : unit -> functions
val iter_fct : (Kernel_function.t -> unit) -> functions -> unit
val iter_kf : (Kernel_function.t -> unit) -> unit
val iter_wp : (Kernel_function.t -> unit) -> unit
(** {2 Goal Selection} *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment