package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Wp.AutoSource

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
Sourceval 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
Sourceval instance : ?priority:float -> Tactical.selection -> Tactical.selection list -> Strategy.strategy
Sourceval lemma : ?priority:float -> ?at:Tactical.selection -> string -> Tactical.selection list -> Strategy.strategy
Sourceval intuition : ?priority:float -> Tactical.selection -> Strategy.strategy
Sourceval 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.

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.

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

Sourceval 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.

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

Sourceval t_range : Lang.F.term -> int -> int -> upper:Tactical.process -> lower:Tactical.process -> range:Tactical.process -> Tactical.process
Sourceval t_replace : ?equal:string -> src:Lang.F.term -> tgt:Lang.F.term -> Tactical.process -> Tactical.process

Prove src=tgt then replace src by tgt.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct