Module Conditions

module Conditions: sig .. end
Bundles

type step = {
   vars : Lang.F.Vars.t;
   stmt : Cil_types.stmt option;
   descr : string option;
   deps : Property.t list;
   warn : Warning.Set.t;
   condition : condition;
}
type sequence = Lang.F.Vars.t * step list 
type condition = 
| Type of Lang.F.pred
| Have of Lang.F.pred
| When of Lang.F.pred
| Branch of Lang.F.pred * sequence * sequence
| Either of sequence list
val is_cond_true : condition -> Qed.Logic.maybe
val is_seq_true : step list -> Qed.Logic.maybe
val vars_list : (Lang.F.Vars.t * 'a) list -> Lang.F.Vars.t
val vars_seq : step list -> Lang.F.Vars.t
val vars_cond : condition -> Lang.F.Vars.t
val vars_sequent : step list * Lang.F.pred -> Lang.F.Vars.t
module Bundle: sig .. end
type bundle = Bundle.t 
type hypotheses = step list 
type sequent = hypotheses * Lang.F.pred 
type link = 
| Lstmt of Cil_types.stmt
| Lprop of Property.t
type linker = (string, link) Hashtbl.t 
val glinker : (string, link) Hashtbl.t option Pervasives.ref
val pid : int Pervasives.ref
val linker : unit -> ('a, 'b) Hashtbl.t
val get_link : ('a, 'b) Hashtbl.t -> 'a -> 'b
val pp_link : link ->
(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a -> unit
val pp_loc : Format.formatter -> Lexing.position -> unit
val pp_stmt : Format.formatter -> Cil_datatype.Stmt.t option -> unit
val pp_descr : Format.formatter -> step -> unit
val pp_depend : Format.formatter -> step -> Property.t -> unit
val pp_warning : Format.formatter -> Warning.t -> unit
val pp_clause : Format.formatter -> Lang.F.env -> string -> Lang.F.pred -> unit
val mark_seq : Lang.F.marks -> step list -> unit
val pp_step : Format.formatter -> Lang.F.env -> step -> unit
val pp_condition : Format.formatter -> Lang.F.env -> condition -> unit
val pp_sequence : Format.formatter -> string -> Lang.F.env -> step list -> unit
val pp_block : Format.formatter -> Lang.F.env -> step list -> unit
val dump : Format.formatter -> bundle -> unit
val pp_seq : string -> Format.formatter -> step list -> unit
val pred_cond : condition -> Lang.F.pred
val pred_seq : sequence -> Lang.F.pred
val extract : Bundle.t -> Lang.F.pred list
val hypotheses : Bundle.t -> step list
val intersect : Lang.F.pred -> Bundle.t -> bool
val occurs : Lang.F.Vars.elt -> Bundle.t -> bool
val pretty : ?linker:(string, link) Hashtbl.t ->
Format.formatter -> step list * Lang.F.pred -> unit
val empty : Bundle.t
val step : ?descr:string ->
?stmt:Cil_types.stmt ->
?deps:Property.t list ->
?warn:Warning.Set.t -> condition -> step
type 'a disjunction = 
| TRUE
| FALSE
| EITHER of 'a list
val disjunction : ('a -> Qed.Logic.maybe) -> 'a list -> 'a disjunction
type 'a attributed = ?descr:string ->
?stmt:Cil_types.stmt -> ?deps:Property.t list -> ?warn:Warning.Set.t -> 'a
val domain : Lang.F.pred list -> Bundle.t -> Bundle.t
val intros : Lang.F.pred list -> Bundle.t -> Bundle.t
val assume : ?descr:string ->
?stmt:Cil_types.stmt ->
?deps:Property.t list ->
?warn:Warning.Set.t ->
Lang.F.pred -> Bundle.t -> Bundle.t
val branch : ?descr:string ->
?stmt:Cil_types.stmt ->
?deps:Property.t list ->
?warn:Warning.Set.t ->
Lang.F.pred ->
Bundle.t -> Bundle.t -> Bundle.t
val either : ?descr:string ->
?stmt:Cil_types.stmt ->
?deps:Property.t list ->
?warn:Warning.Set.t -> Bundle.t list -> Bundle.t
val merge : Bundle.t list -> Bundle.t
val flat_cons : step -> step list -> step list
val flat_concat : step list -> step list -> step list
val flatten_sequence : bool Pervasives.ref -> step list -> step list
module Sigma: Letify.Sigma
module Defs: Letify.Defs
val used_of_dseq : (Lang.F.Vars.t * Defs.t * step) array -> Lang.F.Vars.t
val bind_dseq : Lang.F.Vars.t -> 'a * Defs.t * 'b -> Letify.Sigma.t -> Letify.Sigma.t
val locals : Sigma.t ->
target:Lang.F.Vars.t ->
required:Lang.F.Vars.t ->
?step:Lang.F.Vars.t ->
int -> (Lang.F.Vars.t * 'a * 'b) array -> Lang.F.Vars.t * Lang.F.Vars.t
val dseq_of_step : Sigma.t -> step -> Lang.F.Vars.t * Defs.t * step
val letify_assume : Sigma.t Pervasives.ref -> 'a * 'b * step -> Sigma.t
val letify_type : Sigma.t -> Lang.F.Vars.t -> Lang.F.pred -> Lang.F.pred
val letify_seq : Sigma.t ->
target:Lang.F.Vars.t ->
export:Lang.F.Vars.t ->
step list -> bool * Sigma.t * Sigma.t * step list
val letify_step : (Lang.F.Vars.t * Defs.t * step) array ->
Sigma.t array ->
required:Lang.F.Vars.t ->
target:Lang.F.Vars.t ->
used:Lang.F.Vars.t ->
int -> Lang.F.Vars.t * Defs.t * step -> step
val letify_case : Sigma.t ->
target:Lang.F.Vars.t ->
export:Lang.F.Vars.t -> sequence -> sequence
exception Contradiction
class type simplifier = object .. end
val apply_hyp : < assume : Lang.F.pred -> unit; target : Lang.F.pred -> unit; .. > list ->
step -> unit
val simplify : simplifier list ->
step list * Lang.F.pred -> outcome
val decide_branch : bool Pervasives.ref ->
< simplify : Lang.F.pred -> Lang.F.pred; .. > list ->
step -> step
val add_infer : bool Pervasives.ref ->
< infer : Lang.F.pred list; name : string; .. > ->
step list -> step list
type outcome = 
| NoSimplification
| Simplified of sequent
| Trivial
val simplify : simplifier list ->
step list * Lang.F.pred -> outcome
val fixpoint : int ->
simplifier list ->
Sigma.t -> sequent -> step list * Lang.F.pred
val letify : ?solvers:simplifier list ->
sequent -> step list * Lang.F.pred
val residual : Lang.F.pred -> step
val add_case : Lang.F.pred -> step list -> step list
val is_absurd : step -> bool
val is_trivial : sequent -> bool
val test_case : Lang.F.pred ->
sequent -> (step list * Lang.F.pred) option
val tc : int Pervasives.ref
val test_cases : sequent -> (Lang.F.pred * 'a) list -> sequent
val collect_cond : Cleaning.usage -> condition -> unit
val collect_seq : Cleaning.usage -> sequence -> unit
val collect_steps : Cleaning.usage -> step list -> unit
val pruning : ?solvers:'a list -> sequent -> sequent
val collect_cond : Cleaning.usage -> condition -> unit
val collect_seq : Cleaning.usage -> sequence -> unit
val collect_steps : Cleaning.usage -> step list -> unit
val clean_cond : Cleaning.usage -> condition -> condition
val clean_seq : Cleaning.usage -> sequence -> sequence
val clean_steps : Cleaning.usage -> step list -> step list
val clean : step list * Lang.F.pred -> step list * Lang.F.pred
val close : step list * Lang.F.pred -> Lang.F.pred