Module Wp.Wp_parameters

module Wp_parameters: sig .. end

include Plugin.S
val reset : unit -> unit
val hypothesis : 'a Log.pretty_printer

Function Selection

type functions = 
| Fct_none
| Fct_all
| Fct_skip of Cil_datatype.Kf.Set.t
| Fct_list of Cil_datatype.Kf.Set.t
val get_fct : unit -> functions
val iter_fct : (Kernel_function.t -> unit) -> functions -> unit
val iter_kf : (Kernel_function.t -> unit) -> unit

Goal Selection

module WP: Parameter_sig.Bool 
module Dump: Parameter_sig.Bool 
module Behaviors: Parameter_sig.String_list 
module Properties: Parameter_sig.String_list 
module StatusAll: Parameter_sig.Bool 
module StatusTrue: Parameter_sig.Bool 
module StatusFalse: Parameter_sig.Bool 
module StatusMaybe: Parameter_sig.Bool 

Model Selection

val has_dkey : category -> bool
module Model: Parameter_sig.String_list 
module ByValue: Parameter_sig.String_set 
module ByRef: Parameter_sig.String_set 
module InHeap: Parameter_sig.String_set 
module AliasInit: Parameter_sig.Bool 
module InCtxt: Parameter_sig.String_set 
module ExternArrays: Parameter_sig.Bool 
module Literals: Parameter_sig.Bool 
module Volatile: Parameter_sig.Bool 
module WeakIntModel: Parameter_sig.Bool 
module Region: Parameter_sig.Bool 
module Region_rw: Parameter_sig.Bool 
module Region_pack: Parameter_sig.Bool 
module Region_flat: Parameter_sig.Bool 
module Region_annot: Parameter_sig.Bool 
module Region_inline: Parameter_sig.Bool 
module Region_fixpoint: Parameter_sig.Bool 
module Region_cluster: Parameter_sig.Bool 
module Region_output_dot: Parameter_sig.Filepath 

Computation Strategies

module Init: Parameter_sig.Bool 
module InitWithForall: Parameter_sig.Bool 
module BoundForallUnfolding: Parameter_sig.Int 
module RTE: Parameter_sig.Bool 
module Simpl: Parameter_sig.Bool 
module Let: Parameter_sig.Bool 
module Core: Parameter_sig.Bool 
module Prune: Parameter_sig.Bool 
module FilterInit: Parameter_sig.Bool 
module Clean: Parameter_sig.Bool 
module Filter: Parameter_sig.Bool 
module Parasite: Parameter_sig.Bool 
module Prenex: Parameter_sig.Bool 
module Ground: Parameter_sig.Bool 
module Reduce: Parameter_sig.Bool 
module ExtEqual: Parameter_sig.Bool 
module UnfoldAssigns: Parameter_sig.Int 
module Split: Parameter_sig.Bool 
module SplitMax: Parameter_sig.Int 
module SplitDepth: Parameter_sig.Int 
module DynCall: Parameter_sig.Bool 
module SimplifyIsCint: Parameter_sig.Bool 
module SimplifyLandMask: Parameter_sig.Bool 
module SimplifyForall: Parameter_sig.Bool 
module SimplifyType: Parameter_sig.Bool 
module CalleePreCond: Parameter_sig.Bool 
module PrecondWeakening: Parameter_sig.Bool 
module TerminatesExtDeclarations: Parameter_sig.Bool 
module TerminatesStdlibDeclarations: Parameter_sig.Bool 
module TerminatesDefinitions: Parameter_sig.Bool 
module TerminatesVariantHyp: Parameter_sig.Bool 

Prover Interface

module Detect: Parameter_sig.Bool 
module Generate: Parameter_sig.Bool 
module ScriptOnStdout: Parameter_sig.Bool 
module Provers: Parameter_sig.String_list 
module Interactive: Parameter_sig.String 
module RunAllProvers: Parameter_sig.Bool 
module Cache: Parameter_sig.String 
module CacheEnv: Parameter_sig.Bool 
module CacheDir: Parameter_sig.String 
module CachePrint: Parameter_sig.Bool 
module Drivers: Parameter_sig.String_list 
module Timeout: Parameter_sig.Int 
module FctTimeout: Parameter_sig.Map 
  with type key = Cil_types.kernel_function
   and type value = int
module SmokeTimeout: Parameter_sig.Int 
module InteractiveTimeout: Parameter_sig.Int 
module TimeExtra: Parameter_sig.Int 
module TimeMargin: Parameter_sig.Int 
module Steps: Parameter_sig.Int 
module Procs: Parameter_sig.Int 
module ProofTrace: Parameter_sig.Bool 
module Why3Flags: Parameter_sig.String_list 
module Auto: Parameter_sig.String_list 
module AutoDepth: Parameter_sig.Int 
module AutoWidth: Parameter_sig.Int 
module BackTrack: Parameter_sig.Int 

Proof Obligations

module TruncPropIdFileName: Parameter_sig.Int 
module Print: Parameter_sig.Bool 
module Report: Parameter_sig.String_list 
module ReportJson: Parameter_sig.String 
module ReportName: Parameter_sig.String 
module MemoryContext: Parameter_sig.Bool 
module CheckMemoryContext: Parameter_sig.Bool 
module SmokeTests: Parameter_sig.Bool 
module SmokeDeadassumes: Parameter_sig.Bool 
module SmokeDeadcode: Parameter_sig.Bool 
module SmokeDeadcall: Parameter_sig.Bool 
module SmokeDeadlocalinit: Parameter_sig.Bool 
module SmokeDeadloop: Parameter_sig.Bool 

Getters

val has_out : unit -> bool
val has_session : unit -> bool
val get_session : force:bool -> unit -> Datatype.Filepath.t
val get_session_dir : force:bool -> string -> Datatype.Filepath.t
val get_output : unit -> Datatype.Filepath.t
val get_output_dir : string -> Datatype.Filepath.t
val make_output_dir : string -> unit

Debugging Categories

val has_print_generated : unit -> bool
val print_generated : ?header:string -> string -> unit

print the given file if the debugging category "print-generated" is set

val cat_print_generated : category
val protect : exn -> bool