TacInstance (frama-c-wp.Wp.TacInstance)

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