Newer
Older
(**************************************************************************)
(* *)
(* This file is part of WP plug-in of Frama-C. *)
(* *)
(* CEA (Commissariat a l'energie atomique et aux energies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
let () = Plugin.is_share_visible ()
let () = Plugin.is_session_visible ()
include Plugin.Register
(struct
let name = "WP"
let shortname = "wp"
let help = "Proof by Weakest Precondition Calculus"
end)
(* localize all warnings inside WP *)
let warning ?wkey ?current = match current with
| None -> warning ?wkey ~current:true
| Some b -> warning ?wkey ~current:b
let wkey_hyp = register_warn_category "hypothesis"
let hypothesis ?current ?source ?emitwith ?echo ?once ?append text =
warning ~wkey:wkey_hyp ?current ?source ?emitwith ?echo ?once ?append text
let resetdemon = ref []
let on_reset f = resetdemon := f :: !resetdemon
let reset () = List.iter (fun f -> f ()) !resetdemon
let has_dkey (k:category) = is_debug_key_enabled k
(* ------------------------------------------------------------------------ *)
(* --- WP Generation --- *)
(* ------------------------------------------------------------------------ *)
let wp_generation = add_group "Goal Generator"
let () = Parameter_customize.set_group wp_generation
let () = Parameter_customize.do_not_save ()
module WP =
Action(struct
let option_name = "-wp"
let help = "Generate proof obligations for all (selected) properties."
end)
let () = on_reset WP.clear
let () = Parameter_customize.set_group wp_generation
module Dump =
Action(struct
let option_name = "-wp-dump"
let help = "Dump WP calculus graph."
end)
let () = on_reset Dump.clear
let () = Parameter_customize.set_group wp_generation
let () = Parameter_customize.do_not_save ()
module Functions =
Kernel_function_set
(struct
let option_name = "-wp-fct"
let arg_name = "f,..."
let help = "Select properties of given functions (defaults to all functions)."
end)
let () = on_reset Functions.clear
let () = Parameter_customize.set_group wp_generation
let () = Parameter_customize.do_not_save ()
module SkipFunctions =
Kernel_function_set
(struct
let option_name = "-wp-skip-fct"
let arg_name = "f,..."
let help = "Skip the specified functions (defaults to none)."
end)
let () = on_reset SkipFunctions.clear
let () = Parameter_customize.set_group wp_generation
let () = Parameter_customize.do_not_save ()
module Behaviors =
String_list
(struct
let option_name = "-wp-bhv"
let arg_name = "b,..."
let help = "Select only properties belonging to listed behaviors (the name \"default!\" can be used to select the default anonymous behavior) of the selected functions (defaults to all behaviors)."
end)
let () = on_reset Behaviors.clear
let () = Parameter_customize.set_group wp_generation
let () = Parameter_customize.do_not_save ()
let () = Parameter_customize.no_category ()
module Properties =
String_list
(struct
let option_name = "-wp-prop"
let arg_name = "p,..."
let help =
"Select properties based names and category.\n\
Use +name or +category to select properties and -name or -category \
to remove them from the selection. The '+' sign can be omitted.\n\
Categories are: @lemma, @requires, @assigns, @ensures, @exits, \
@assert, @invariant, @variant, @breaks, @continues, @returns, \
@complete_behaviors, @disjoint_behaviors, @terminates, \
@decreases and @check (which includes all check clauses)."
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
end)
let () = on_reset Properties.clear
let () = Parameter_customize.set_group wp_generation
module StatusAll =
False(struct
let option_name = "-wp-status-all"
let help = "Select properties with any status."
end)
let () = Parameter_customize.set_group wp_generation
module StatusTrue =
False(struct
let option_name = "-wp-status-valid"
let help = "Select properties with status 'Valid'."
end)
let () = Parameter_customize.set_group wp_generation
module StatusFalse =
False(struct
let option_name = "-wp-status-invalid"
let help = "Select properties with status 'Invalid'."
end)
let () = Parameter_customize.set_group wp_generation
module StatusMaybe =
True(struct
let option_name = "-wp-status-maybe"
let help = "Select properties with status 'Maybe'."
end)
(* ------------------------------------------------------------------------ *)
(* --- Selected Functions --- *)
(* ------------------------------------------------------------------------ *)
module Fct = Cil_datatype.Kf.Set
type functions =
| Fct_none
| Fct_all
| Fct_skip of Fct.t
| Fct_list of Fct.t
let iter_fct phi = function
| Fct_none -> ()
| Fct_all -> Globals.Functions.iter phi
| Fct_skip fs ->
Globals.Functions.iter
(fun kf -> if not (Fct.mem kf fs) then phi kf)
| Fct_list fs -> Fct.iter phi fs
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()))
if WP.get () || not (Functions.is_empty()) ||
not (Behaviors.is_empty()) || not (Properties.is_empty())
let iter_kf f = iter_fct f (get_fct ())
(* ------------------------------------------------------------------------ *)
(* --- Memory Models --- *)
(* ------------------------------------------------------------------------ *)
let wp_model = add_group "Model Selection"
let () = Parameter_customize.set_group wp_model
module Model =
String_list
(struct
let option_name = "-wp-model"
let arg_name = "model+..."
let help = "Memory model selection. Available selectors:\n\
* 'Hoare' logic variables only\n\
* 'Typed' typed pointers only\n\
* '+nocast' no pointer cast\n\
* '+cast' unsafe pointer casts\n\
* '+raw' no logic variable\n\
* '+ref' by-reference-style pointers detection\n\
* '+nat/+int' natural / machine-integers arithmetics\n\
* '+real/+float' real / IEEE floating point arithmetics\n\
* 'Eva' (experimental) based on the results from Eva plugin"
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
end)
let () = Parameter_customize.set_group wp_model
module ByValue =
String_set
(struct
let option_name = "-wp-unalias-vars"
let arg_name = "var,..."
let help = "Consider variable names non-aliased."
end)
let () = Parameter_customize.set_group wp_model
module ByRef =
String_set
(struct
let option_name = "-wp-ref-vars"
let arg_name = "var,..."
let help = "Consider variable names by reference."
end)
let () = Parameter_customize.set_group wp_model
module InHeap =
String_set
(struct
let option_name = "-wp-alias-vars"
let arg_name = "var,..."
let help = "Consider variable names aliased."
end)
let () = Parameter_customize.set_group wp_model
module AliasInit =
False(struct
let option_name = "-wp-alias-init"
let help = "Use initializers for aliasing propagation."
end)
let () = Parameter_customize.set_group wp_model
module InCtxt =
String_set
(struct
let option_name = "-wp-context-vars"
let arg_name = "var,..."
let help = "Consider variable names in isolated context."
end)
let () = Parameter_customize.set_group wp_model
module ExternArrays =
False(struct
let option_name = "-wp-extern-arrays"
let help = "Put some default size for extern arrays."
end)
let () = Parameter_customize.set_group wp_model
module WeakIntModel =
False(struct
let option_name = "-wp-weak-int-model"
let help = "Suppress integral type side conditions within lemmas\n\
(possibly unsound)"
end)
let () = Parameter_customize.set_group wp_model
module Literals =
False(struct
let option_name = "-wp-literals"
let help = "Export content of string literals."
end)
let () = Parameter_customize.set_group wp_model
module Volatile =
True(struct
let option_name = "-wp-volatile"
let help = "Sound modeling of volatile access.\n\
Use -wp-no-volatile to ignore volatile attributes."
end)
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
(* -------------------------------------------------------------------------- *)
(* --- Region Model --- *)
(* -------------------------------------------------------------------------- *)
let wp_region = add_group "Region Analysis"
let () = Parameter_customize.set_group wp_region
let () = Parameter_customize.do_not_save ()
module Region =
False
(struct
let option_name = "-wp-region"
let help = "Perform Region Analysis (experimental)"
end)
let () = Parameter_customize.set_group wp_region
let () = Parameter_customize.do_not_save ()
module Region_fixpoint =
True
(struct
let option_name = "-wp-region-fixpoint"
let help = "Compute region aliasing fixpoint"
end)
let () = Parameter_customize.set_group wp_region
let () = Parameter_customize.do_not_save ()
module Region_cluster =
True
(struct
let option_name = "-wp-region-cluster"
let help = "Compute region clustering fixpoint"
end)
let () = Parameter_customize.set_group wp_region
let () = Parameter_customize.do_not_save ()
module Region_inline =
True
(struct
let option_name = "-wp-region-inline"
let help = "Inline aliased sub-clusters"
end)
let () = Parameter_customize.set_group wp_region
let () = Parameter_customize.do_not_save ()
module Region_rw =
True
(struct
let option_name = "-wp-region-rw"
let help = "Written region are considered read-write by default"
end)
let () = Parameter_customize.set_group wp_region
let () = Parameter_customize.do_not_save ()
module Region_pack =
True
(struct
let option_name = "-wp-region-pack"
let help = "Pack clusters by default"
end)
let () = Parameter_customize.set_group wp_region
let () = Parameter_customize.do_not_save ()
module Region_flat =
False
(struct
let option_name = "-wp-region-flat"
let help = "Flatten arrays by default"
end)
let () = Parameter_customize.set_group wp_region
module Region_annot =
False
(struct
let option_name = "-region-annot"
let help = "Register '@region' ACSL Annotations (auto with -wp-region)"
end)
let () = Parameter_customize.set_group wp_region
let () = Parameter_customize.is_invisible ()
module Region_output_dot =
Filepath
(struct
let option_name = "-wp-region-output-dot"
let arg_name = "output.dot"
let file_kind = "DOT"
let existence = Fc_Filepath.Indifferent
let help = "Outputs the region graph in DOT format to the specified file."
end)
(* ------------------------------------------------------------------------ *)
(* --- WP Strategy --- *)
(* ------------------------------------------------------------------------ *)
let wp_strategy = add_group "Computation Strategies"
let () = Parameter_customize.set_group wp_strategy
module Init =
let option_name = "-wp-init-const"
let help = "Use initializers for global const variables."
end)
let () = Parameter_customize.set_group wp_strategy
module CalleePreCond =
True(struct
let option_name = "-wp-callee-precond"
let help = "Use pre-conditions of callee."
end)
let () = Parameter_customize.set_group wp_strategy
module RTE =
False(struct
let option_name = "-wp-rte"
let help = "Generate RTE guards before WP."
end)
let () = Parameter_customize.set_group wp_strategy
module SmokeTests =
False(struct
let option_name = "-wp-smoke-tests"
let help = "Smoke-tests : look for inconsistent contracts (best effort)"
end)
let () = Parameter_customize.set_group wp_strategy
module SmokeDeadassumes =
True(struct
let option_name = "-wp-smoke-dead-assumes"
let help = "When generating smoke tests, look for dead assumes"
end)
let () = Parameter_customize.set_group wp_strategy
module SmokeDeadcode =
True(struct
let option_name = "-wp-smoke-dead-code"
let help = "When generating smoke tests, look for unreachable code"
end)
let () = Parameter_customize.set_group wp_strategy
module SmokeDeadcall =
True(struct
let option_name = "-wp-smoke-dead-call"
let help = "When generating smoke tests, look for non-terminating calls"
end)
let () = Parameter_customize.set_group wp_strategy
module SmokeDeadlocalinit =
False(struct
let option_name = "-wp-smoke-dead-local-init"
let help = "When generating smoke tests, look for dead local variables \
initialization"
end)
let () = Parameter_customize.set_group wp_strategy
module SmokeDeadloop =
True(struct
let option_name = "-wp-smoke-dead-loop"
let help = "When generating smoke tests, look for inconsistent loop invariants"
let () = Parameter_customize.set_group wp_strategy
module Split =
False(struct
let option_name = "-wp-split"
let help = "Split conjunctions into sub-goals."
end)
let () = Parameter_customize.set_group wp_strategy
module UnfoldAssigns =
let option_name = "-wp-unfold-assigns"
let default = 0
let arg_name = "n"
let help = "Unfold up to <n> levels of aggregates and arrays in assigns.\n\
Value -1 means unlimited depth (default 0)"
end)
let () = Parameter_customize.set_group wp_strategy
module SplitDepth =
Int(struct
let option_name = "-wp-split-depth"
let default = 0
let arg_name = "p"
let help = "Set depth for splitting conjunctions into sub-goals.\n\
Value -1 means unlimited depth (default 0)"
end)
let () = Parameter_customize.set_group wp_strategy
module SplitMax =
Int(struct
let option_name = "-wp-max-split"
let default = 1000
let arg_name = "n"
let help = "Set maximum number of splitted sub-goals (default 1000)"
end)
let () = Parameter_customize.set_group wp_strategy
let () = Parameter_customize.is_invisible ()
module DynCall =
True(struct
let option_name = "-wp-dynamic"
let help = "Handle dynamic calls with specific annotations."
end)
(* NOT use DynCall.add_set_hook: it won't work for the positive version of
the option, as the default is already true. *)
let () =
Cmdline.run_after_configuring_stage
(fun () ->
if DynCall.is_set () then
warning ~current:false
"Option -wp-dynamic is obsolete and will be removed \
at some point in the future. @@calls annotations are now handled \
directly in the kernel")
let () = Parameter_customize.set_group wp_strategy
module PrecondWeakening =
False(struct
let option_name = "-wp-precond-weakening"
let help = "Discard pre-conditions of side behaviours (sound but incomplete optimisation)."
end)
let () = Parameter_customize.set_group wp_strategy
module TerminatesExtDeclarations =
let option_name = "-wp-declarations-terminate"
let help = "Undefined external functions without terminates specification \
are considered to terminate when called."
end)
let () = Parameter_customize.set_group wp_strategy
module TerminatesDefinitions =
False(struct
let option_name = "-wp-definitions-terminate"
let help = "Defined functions without terminates specification are \
considered to terminate when called."
end)
module TerminatesStdlibDeclarations =
False(struct
let option_name = "-wp-frama-c-stdlib-terminate"
let help = "Frama-C stdlib functions without terminates specification \
are considered to terminate when called."
end)
let () = Parameter_customize.set_group wp_strategy
module TerminatesVariantHyp =
False(struct
let option_name = "-wp-variant-with-terminates"
let help = "Prove loop variant under the termination hypothesis."
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
(* ------------------------------------------------------------------------ *)
(* --- Qed Simplifications --- *)
(* ------------------------------------------------------------------------ *)
let wp_simplifier = add_group "Qed Simplifications"
let () = Parameter_customize.set_group wp_simplifier
module Simpl =
True(struct
let option_name = "-wp-simpl"
let help = "Enable Qed Simplifications."
end)
let () = Parameter_customize.set_group wp_simplifier
module Let =
True(struct
let option_name = "-wp-let"
let help = "Use variable elimination."
end)
let () = Parameter_customize.set_group wp_simplifier
module Core =
True(struct
let option_name = "-wp-core"
let help = "Lift core facts through branches."
end)
let () = Parameter_customize.set_group wp_simplifier
module Prune =
True(struct
let option_name = "-wp-pruning"
let help = "Prune trivial branches."
end)
let () = Parameter_customize.set_group wp_simplifier
module FilterInit =
True(struct
let option_name = "-wp-filter-init"
let help = "Use aggressive filtering of initialization hypotheses."
end)
let () = Parameter_customize.set_group wp_simplifier
module Clean =
True(struct
let option_name = "-wp-clean"
let help = "Use a simple cleaning in case of -wp-no-let."
end)
let () = Parameter_customize.set_group wp_simplifier
module Ground =
True(struct
let option_name = "-wp-ground"
let help = "Use aggressive ground simplifications."
end)
let () = Parameter_customize.set_group wp_simplifier
module Reduce =
True(struct
let option_name = "-wp-reduce"
let help = "Reduce function equalities with precedence to constructors."
end)
let () = Parameter_customize.set_group wp_simplifier
module ExtEqual =
True(struct
let option_name = "-wp-extensional"
let help = "Use extensional equality on compounds (hypotheses only)."
end)
let () = Parameter_customize.set_group wp_simplifier
module Filter =
True(struct
let option_name = "-wp-filter"
let help = "Filter non-used variables and related hypotheses."
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
end)
let () = Parameter_customize.set_group wp_simplifier
module Parasite =
True(struct
let option_name = "-wp-parasite"
let help = "Use singleton-variable filtering."
end)
let () = Parameter_customize.set_group wp_simplifier
module Prenex =
False(struct
let option_name = "-wp-prenex"
let help = "Normalize nested foralls into prenex-form"
end)
let () = Parameter_customize.set_group wp_simplifier
module SimplifyIsCint =
True(struct
let option_name = "-wp-simplify-is-cint"
let help = "Remove redundant machine integer range hypothesis."
end)
let () = Parameter_customize.set_group wp_simplifier
module SimplifyLandMask =
True(struct
let option_name = "-wp-simplify-land-mask"
let help = "Tight logical masks on unsigned integers."
end)
let () = Parameter_customize.set_group wp_simplifier
module SimplifyForall =
False(struct
let option_name = "-wp-simplify-forall"
let help = "Remove machine integer ranges in quantifiers."
end)
let () = Parameter_customize.set_group wp_simplifier
module SimplifyType =
False(struct
let option_name = "-wp-simplify-type"
let help = "Remove all `Type` constraints."
end)
let () = Parameter_customize.set_group wp_simplifier
module InitWithForall =
True(struct
let option_name = "-wp-init-summarize-array"
let help = "Summarize contiguous initializers with quantifiers."
end)
let () = Parameter_customize.set_group wp_simplifier
module BoundForallUnfolding =
Int(struct
let option_name = "-wp-bound-forall-unfolding"
let help = "Instantiate up to <n> forall-integers hypotheses."
let arg_name="n"
let default = 1000
end)
(* ------------------------------------------------------------------------ *)
(* --- Prover Interface --- *)
(* ------------------------------------------------------------------------ *)
let wp_prover = add_group "Prover Interface"
let () = Parameter_customize.set_group wp_prover
module Provers = String_list
(struct
let option_name = "-wp-prover"
let arg_name = "dp,..."
let help =
"Submit proof obligations to prover(s):\n\
- 'none' (no prover run)\n\
- 'script' (replay all session scripts)\n\
- 'tip' (replay or init scripts for failed goals)\n\
- '<why3-prover>' (any Why-3 prover, see -wp-detect)\n\
let () = Parameter_customize.set_group wp_prover
module Interactive = String
(struct
let option_name = "-wp-interactive"
let arg_name = "mode"
let default = "batch"
let help =
"WP mode for interactive Why-3 provers (eg: Coq):\n\
- 'batch': check current proof (default)\n\
- 'update': update and check proof\n\
- 'edit': edit proof before check\n\
- 'fix': check and edit proof if necessary\n\
- 'fixup': update proof and fix\n\
let () = Parameter_customize.set_group wp_prover
module RunAllProvers =
False(struct
let option_name = "-wp-run-all-provers"
let help = "Run all specified provers on each goal not proved by Qed. \
Do not stop when a prover succeeds. (default: no)"
end)
let () = Parameter_customize.set_group wp_prover
module Cache = String
(struct
let option_name = "-wp-cache"
let arg_name = "mode"
let help =
"WP cache mode:\n\
- 'none': no cache, run provers (default)\n\
- 'update': use cache or run provers and update cache\n\
- 'cleanup': update mode with garbage collection\n\
- 'replay': update mode with no cache update\n\
- 'rebuild': always run provers and update cache\n\
- 'offline': use cache but never run provers\n\
You can also use the environment variable FRAMAC_WP_CACHE instead."
end)
let () = Parameter_customize.set_group wp_prover
(struct
let option_name = "-wp-cache-env"
let help = "Gives environment variables precedence over command line\n\
for cache management:\n\
- FRAMAC_WP_CACHE overrides -wp-cache\n\
- FRAMAC_WP_CACHEDIR overrides -wp-cache-dir\n\
let () = Parameter_customize.set_group wp_prover
module CacheDir = String
(struct
let option_name = "-wp-cache-dir"
let arg_name = "dir"
let default = ""
let help =
"Specify global cache directory (no cleanup mode).\n\
By default, cache entries are stored in the WP session directory.\n\
You can also use the environment variable FRAMAC_WP_CACHEDIR instead."
let () = Parameter_customize.set_group wp_prover
module CachePrint = False
(struct
let option_name = "-wp-cache-print"
let help = "Show cache directory"
end)
let () = Parameter_customize.set_group wp_prover
module Generate = False
(struct
let option_name = "-wp-gen"
let help = "Only generate prover files (default: no)."
end)
let () = on_reset Generate.clear
let () = Parameter_customize.set_group wp_prover
module ScriptOnStdout = False
(struct
let option_name = "-wp-script-on-stdout"
let help = "When enabled (default: no), display scripts on stdout \
instead of writing them on disk."
end)
let () = Parameter_customize.set_group wp_prover
module PrepareScripts = Action
(struct
let option_name = "-wp-prepare-scripts"
let help = "Initialize a script tracking directory in the session \
directory."
end)
let () = Parameter_customize.set_group wp_prover
module FinalizeScripts = Action
(struct
let option_name = "-wp-finalize-scripts"
let help = "Remove untracked scripts according to the tracking directory \
if it does exist (does not remove anything otherwise)."
end)
let () = Parameter_customize.set_group wp_prover
module DryFinalizeScripts = False
(struct
let option_name = "-wp-dry-finalize-scripts"
let help = "Scripts that might be removed by -wp-finalize-scripts are \
kept, a message is printed instead for each file. The marks \
directory is kept."
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
let () = Parameter_customize.set_group wp_prover
module Detect = Action
(struct
let option_name = "-wp-detect"
let help = "List installed provers."
end)
let () = on_reset Detect.clear
let () = Parameter_customize.set_group wp_prover
module Drivers =
String_list
(struct
let option_name = "-wp-driver"
let arg_name = "file,..."
let help = "Load drivers for linking to external libraries"
end)
let () = Parameter_customize.set_group wp_prover
module Steps =
Int(struct
let option_name = "-wp-steps"
let default = 0
let arg_name = "n"
let help = "Set number of steps for provers."
end)
let () = Parameter_customize.set_group wp_prover
module Timeout =
Int(struct
let option_name = "-wp-timeout"
let default = 10
let arg_name = "n"
let help =
Printf.sprintf
"Set the timeout (in seconds) for provers (default: %d)." default
end)
let () = Parameter_customize.set_group wp_prover
module FctTimeout =
Kernel_function_map
(struct
include Datatype.Int
type key = Cil_types.kernel_function
let of_string ~key:_ ~prev:_ s =
Option.map
(fun s ->
try int_of_string s
with Failure _ ->
raise (Cannot_build ("'" ^ s ^ "' is not an integer")))
s
let to_string ~key:_ = Option.map string_of_int
end)
(struct
let option_name = "-wp-fct-timeout"
let arg_name = "f1:t1,...,fn:tn"
let help = "Customize the WP timeout (in secondes) for each specified \
function (t1 seconds for f1, t2 for f2, etc)."
let default = Kernel_function.Map.empty
end)
let () = Parameter_customize.set_group wp_prover
module SmokeTimeout =
Int(struct
let option_name = "-wp-smoke-timeout"
let default = 2
let arg_name = "n"
let help =
Printf.sprintf
"Set the timeout (in seconds) for provers (default: %d)." default
end)
let () = Parameter_customize.set_group wp_prover
module InteractiveTimeout =
Int(struct
let option_name = "-wp-interactive-timeout"
let default = 30
let arg_name = "n"
let help =
Printf.sprintf
"Set the timeout (in seconds) for checking scripts\n\
of interactive provers (default: %d)." default
end)
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
let () = Parameter_customize.set_group wp_prover
module TimeExtra =
Int(struct
let option_name = "-wp-time-extra"
let default = 5
let arg_name = "n"
let help =
Printf.sprintf
"Set extra-time (in seconds) for proof replay (default: %d)." default
end)
let () = Parameter_customize.set_group wp_prover
module TimeMargin =
Int(struct
let option_name = "-wp-time-margin"
let default = 2
let arg_name = "n"
let help =
Printf.sprintf
"Set margin-time (in seconds) for considering a proof automatic.\n\
When using the 'tip' prover, scripts are created or cancelled\n\
if the proof time is greater or lower than (timeout - margin).\n\
(default: %d)." default
end)
let () = Parameter_customize.set_group wp_prover
module Procs =
Int(struct
let option_name = "-wp-par"
let arg_name = "p"
let default = 4
let help =
Printf.sprintf
"Number of parallel proof process (default: %d)" default
end)
let () = Parameter_customize.set_group wp_prover
module ProofTrace =
False
(struct
let option_name = "-wp-proof-trace"
let help = "Keeps output of provers for valid POs (default: no)"
end)
(* ------------------------------------------------------------------------ *)
(* --- Prover Options --- *)
(* ------------------------------------------------------------------------ *)
let wp_prover_options = add_group "Prover Options"
let () = Parameter_customize.set_group wp_prover
module Auto = String_list
(struct
let option_name = "-wp-auto"
let arg_name = "s"
let help =
"Activate auto-search with strategy <s>.\n\
Use '-wp-auto <?>' for available strategies."
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
end)
let () = Parameter_customize.set_group wp_prover
module AutoDepth = Int
(struct
let option_name = "-wp-auto-depth"
let arg_name = "n"
let default = 5
let help =
"Depth of auto-search (-wp-auto only, default 5).\n\
Limits the number of nested level in strategies."
end)
let () = Parameter_customize.set_group wp_prover
module AutoWidth = Int
(struct
let option_name = "-wp-auto-width"
let arg_name = "n"
let default = 10
let help =
"Width of auto-search (-wp-auto only, default 10).\n\
Limits the number of pending goals in strategies."
end)
let () = Parameter_customize.set_group wp_prover
module BackTrack = Int
(struct
let option_name = "-wp-auto-backtrack"
let arg_name = "n"
let default = 0
let help =
"Backtracking limit (-wp-auto only, de-activated by default).\n\
Limits backtracking when applying strategies."
end)
let () = Parameter_customize.set_group wp_prover_options
let () = Parameter_customize.no_category ()
String_list
(struct
let option_name = "-wp-why3-opt"
let arg_name = "option,..."
let help = "Additional options for Why3"
end)
Virgile Prevosto
committed
let () = Parameter_customize.set_group wp_prover_options
let () = Parameter_customize.no_category ()
module Why3ExtraConfig =
String_list
(struct
let option_name = "-wp-why3-extra-config"
let arg_name = "file,..."
let help = "Additional config files for Why3"
end)
(* ------------------------------------------------------------------------ *)
(* --- PO Management --- *)
(* ------------------------------------------------------------------------ *)
let wp_po = add_group "Proof Obligations"