module Wp_parameters:sig
..end
include Plugin.S
val reset : unit -> unit
module WP: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
type
job =
| |
WP_None |
| |
WP_All |
| |
WP_SkipFct of |
| |
WP_Fct of |
val job : unit -> job
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 InCtxt:Parameter_sig.String_set
module ExternArrays:Parameter_sig.Bool
module ExtEqual:Parameter_sig.Bool
module Literals:Parameter_sig.Bool
module Volatile:Parameter_sig.Bool
module Init:Parameter_sig.Bool
module InitAlias: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 Clean:Parameter_sig.Bool
module Filter:Parameter_sig.Bool
module Parasite:Parameter_sig.Bool
module Prenex:Parameter_sig.Bool
module Bits:Parameter_sig.Bool
module Ground:Parameter_sig.Bool
module Reduce:Parameter_sig.Bool
module QedChecks:Parameter_sig.String_set
module UnfoldAssigns:Parameter_sig.Bool
module Split:Parameter_sig.Bool
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 Detect:Parameter_sig.Bool
module Generate:Parameter_sig.Bool
module Provers:Parameter_sig.String_list
module Drivers:Parameter_sig.String_list
module Script:Parameter_sig.String
module UpdateScript:Parameter_sig.Bool
module Timeout:Parameter_sig.Int
module TimeExtra:Parameter_sig.Int
module TimeMargin:Parameter_sig.Int
module CoqTimeout:Parameter_sig.Int
module CoqCompiler:Parameter_sig.String
module CoqIde:Parameter_sig.String
module CoqProject:Parameter_sig.String
module Depth:Parameter_sig.Int
module Steps:Parameter_sig.Int
module Procs:Parameter_sig.Int
module ProofTrace:Parameter_sig.Bool
module CoqLibs:Parameter_sig.String_list
module CoqTactic:Parameter_sig.String
module Hints:Parameter_sig.Int
module TryHints:Parameter_sig.Bool
module Why3:Parameter_sig.String
module WhyLibs:Parameter_sig.String_list
module WhyFlags:Parameter_sig.String_list
module AltErgo:Parameter_sig.String
module AltGrErgo:Parameter_sig.String
module AltErgoLibs:Parameter_sig.String_list
module AltErgoFlags: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
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 Check:Parameter_sig.Bool
val get_env : ?default:string -> string -> string
val is_out : unit -> bool
val get_session : unit -> string
val get_session_dir : string -> string
val get_output : unit -> string
val get_output_dir : string -> string
val get_includes : unit -> string list
val make_output_dir : string -> unit
val get_overflows : unit -> bool
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