Frama-C API - Auto
Basic Strategies
It is always safe to apply strategies to any goal.
val array : ?priority:float -> Tactical.selection -> Strategy.strategy
val choice : ?priority:float -> Tactical.selection -> Strategy.strategy
val absurd : ?priority:float -> Tactical.selection -> Strategy.strategy
val contrapose : ?priority:float -> Tactical.selection -> Strategy.strategy
val compound : ?priority:float -> Tactical.selection -> Strategy.strategy
val cut : ?priority:float -> ?modus:bool -> Tactical.selection -> Strategy.strategy
val filter : ?priority:float -> ?anti:bool -> unit -> Strategy.strategy
val havoc : ?priority:float -> Tactical.selection -> Strategy.strategy
val separated : ?priority:float -> Tactical.selection -> Strategy.strategy
val instance : ?priority:float -> Tactical.selection -> Tactical.selection list -> Strategy.strategy
val lemma : ?priority:float -> ?at:Tactical.selection -> string -> Tactical.selection list -> Strategy.strategy
val intuition : ?priority:float -> Tactical.selection -> Strategy.strategy
val range : ?priority:float -> Tactical.selection -> vmin:int -> vmax:int -> Strategy.strategy
val split : ?priority:float -> Tactical.selection -> Strategy.strategy
val definition : ?priority:float -> Tactical.selection -> Strategy.strategy
val compute : ?priority:float -> Tactical.selection -> Strategy.strategy
Registered Heuristics
val auto_split : Strategy.heuristic
val auto_range : Strategy.heuristic
module Range : sig ... end
Trusted Tactical Process
Tacticals with hand-written process are not safe. However, the combinators below are guarantied to be sound.
val t_absurd : Tactical.process
Find a contradiction.
val t_id : Tactical.process
Keep goal unchanged.
val t_finally : string -> Tactical.process
Apply a description to a leaf goal. Same as t_descr "..." t_id
.
val t_descr : string -> Tactical.process -> Tactical.process
Apply a description to each sub-goal
val t_split : ?pos:string -> ?neg:string -> Lang.F.pred -> Tactical.process
Split with p
and not p
.
val t_cut : ?by:string -> Lang.F.pred -> Tactical.process -> Tactical.process
Prove condition p
and use-it as a forward hypothesis.
val t_case : Lang.F.pred -> Tactical.process -> Tactical.process -> Tactical.process
Case analysis: t_case p a b
applies process a
under hypothesis p
and process b
under hypothesis not p
.
val t_cases : ?complete:string -> (Lang.F.pred * Tactical.process) list -> Tactical.process
Complete analysis: applies each process under its guard, and proves that all guards are complete.
val t_chain : Tactical.process -> Tactical.process -> Tactical.process
Apply second process to every goal generated by the first one.
val t_range : Lang.F.term -> int -> int -> upper:Tactical.process -> lower:Tactical.process -> range:Tactical.process -> Tactical.process
val t_replace : ?equal:string -> src:Lang.F.term -> tgt:Lang.F.term -> Tactical.process -> Tactical.process
Prove src=tgt
then replace src
by tgt
.