Wp.TacInstance
Built-in Instance Tactical (auto-registered)
val tactical : Tactical.t
val fields : Tactical.selection Tactical.field list
val params : Tactical.parameter list
val filter : Lang.F.tau -> Lang.F.term -> bool
type bindings = (Lang.F.var * Tactical.selection) list
val complexity : bindings -> Frama_c_kernel.Integer.t
val cardinal : int -> bindings -> int option
less than limit
val instance_goal :
?title:string ->
bindings ->
Lang.F.pred ->
Tactical.process
val instance_have :
?title:string ->
?at:int ->
bindings ->
Lang.F.pred ->
Tactical.process
val wrap :
Tactical.selection Tactical.field list ->
Tactical.selection list ->
Strategy.argument list
val strategy :
?priority:float ->
Tactical.selection ->
Tactical.selection list ->
Strategy.strategy