Module `Wp.Strategy`Source

Strategies Entry Points

Term & Predicate Selection

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.

Strategy

Sourcetype argument =

| ARG : 'a Tactical.field * 'a -> argument

Sourcetype strategy = {

priority : float;
tactical : Tactical.tactical;
selection : Tactical.selection;
arguments : argument list;

}

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

Factory

Sourcetype t = strategy

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

Source

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/Strategy/index.html

Module `Wp.Strategy`Source

Term & Predicate Selection

Strategy

Factory

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/Strategy/index.html

Module Wp.StrategySource

Term & Predicate Selection

Strategy

Factory

Module `Wp.Strategy`Source