package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Module `Wp.TacInstance`Source

Built-in Instance Tactical (auto-registered)

Sourceval tactical : Tactical.t

Sourceval fields : Tactical.selection Tactical.field list

Sourceval params : Tactical.parameter list

Sourceval filter : Lang.F.tau -> Lang.F.term -> bool

Sourcetype bindings = (Lang.F.var * Tactical.selection) list

Sourceval complexity : bindings -> Frama_c_kernel.Integer.t

Sourceval 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