package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Module `Wp.Strategy`Source

Strategies Entry Points

Sourceval occurs_x : Lang.F.var -> Lang.F.term -> bool

Sourceval occurs_y : Lang.F.var -> Lang.F.pred -> bool

Sourceval occurs_e : Lang.F.term -> Lang.F.term -> bool

Sourceval occurs_p : Lang.F.term -> Lang.F.pred -> bool

Sourceval occurs_q : Lang.F.pred -> Lang.F.pred -> bool

Sourceval select_e : Conditions.sequent -> Lang.F.term -> Tactical.selection

Lookup the first occurrence of term in the sequent and returns the associated selection. Returns Empty is not found. Goal is lookup first.

Sourceval select_p : Conditions.sequent -> Lang.F.pred -> Tactical.selection

Same as select_e but for a predicate.

Sourcetype argument =

Sourcetype strategy = {

}

Sourceclass pool : object ... end

Sourceclass type heuristic = object ... end

Sourceval register : heuristic -> unit

Sourceval export : heuristic -> heuristic

Sourceval lookup : id:string -> heuristic

Sourceval iter : (heuristic -> unit) -> unit

Sourcetype t = strategy

Sourceval arg : 'a Tactical.field -> 'a -> argument

val make : 
  Tactical.tactical ->
  ?priority:float ->
  ?arguments:argument list ->
  Tactical.selection ->
  strategy