Module `Wp.Auto`Source

Basic Strategies

It is always safe to apply strategies to any goal.

Sourceval array : ?priority:float -> Tactical.selection -> Strategy.strategy

Sourceval choice : ?priority:float -> Tactical.selection -> Strategy.strategy

Sourceval absurd : ?priority:float -> Tactical.selection -> Strategy.strategy

Sourceval contrapose : ?priority:float -> Tactical.selection -> Strategy.strategy

Sourceval compound : ?priority:float -> Tactical.selection -> Strategy.strategy

val cut : 
  ?priority:float ->
  ?modus:bool ->
  Tactical.selection ->
  Strategy.strategy

Sourceval filter : ?priority:float -> ?anti:bool -> unit -> Strategy.strategy

Sourceval havoc : ?priority:float -> Tactical.selection -> Strategy.strategy

Sourceval separated : ?priority:float -> Tactical.selection -> Strategy.strategy

Source

val instance : 
  ?priority:float ->
  Tactical.selection ->
  Tactical.selection list ->
  Strategy.strategy

Source

val lemma : 
  ?priority:float ->
  ?at:Tactical.selection ->
  string ->
  Tactical.selection list ->
  Strategy.strategy

Sourceval intuition : ?priority:float -> Tactical.selection -> Strategy.strategy

Source

val range : 
  ?priority:float ->
  Tactical.selection ->
  vmin:int ->
  vmax:int ->
  Strategy.strategy

Sourceval split : ?priority:float -> Tactical.selection -> Strategy.strategy

Sourceval definition : ?priority:float -> Tactical.selection -> Strategy.strategy

Sourceval compute : ?priority:float -> Tactical.selection -> Strategy.strategy

Registered Heuristics

Sourceval auto_split : Strategy.heuristic

Sourceval auto_range : Strategy.heuristic

Sourcemodule Range : sig ... end

Trusted Tactical Process

Tacticals with hand-written process are not safe. However, the combinators below are guarantied to be sound.

Sourceval t_absurd : Tactical.process

Find a contradiction.

Sourceval t_id : Tactical.process

Keep goal unchanged.

Sourceval t_finally : string -> Tactical.process

Apply a description to a leaf goal. Same as t_descr "..." t_id.

Sourceval t_descr : string -> Tactical.process -> Tactical.process

Apply a description to each sub-goal

Sourceval t_split : ?pos:string -> ?neg:string -> Lang.F.pred -> Tactical.process

Split with p and not p.

Sourceval t_cut : ?by:string -> Lang.F.pred -> Tactical.process -> Tactical.process

Prove condition p and use-it as a forward hypothesis.

Source

val t_case : 
  Lang.F.pred ->
  Tactical.process ->
  Tactical.process ->
  Tactical.process

Case analysis: t_case p a b applies process a under hypothesis p and process b under hypothesis not p.

Source

val t_cases : 
  ?complete:string ->
  (Lang.F.pred * Tactical.process) list ->
  Tactical.process

Complete analysis: applies each process under its guard, and proves that all guards are complete.

Sourceval t_chain : Tactical.process -> Tactical.process -> Tactical.process

Apply second process to every goal generated by the first one.

Source

val t_range : 
  Lang.F.term ->
  int ->
  int ->
  upper:Tactical.process ->
  lower:Tactical.process ->
  range:Tactical.process ->
  Tactical.process

raises Invalid_argument
when range is empty

Source

val t_replace : 
  ?equal:string ->
  src:Lang.F.term ->
  tgt:Lang.F.term ->
  Tactical.process ->
  Tactical.process

Prove src=tgt then replace src by tgt.

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Wp.Auto`Source

Basic Strategies

Registered Heuristics

Trusted Tactical Process

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module Wp.AutoSource

Basic Strategies

Registered Heuristics

Trusted Tactical Process

Module `Wp.Auto`Source