package frama-c

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

Basic Strategies

It is always safe to apply strategies to any goal.

val array : ?priority:float -> Tactical.selection -> Strategy.strategy
val choice : ?priority:float -> Tactical.selection -> Strategy.strategy
val absurd : ?priority:float -> Tactical.selection -> Strategy.strategy
val contrapose : ?priority:float -> Tactical.selection -> Strategy.strategy
val compound : ?priority:float -> Tactical.selection -> Strategy.strategy
val cut : ?priority:float -> ?modus:bool -> Tactical.selection -> Strategy.strategy
val filter : ?priority:float -> ?anti:bool -> unit -> Strategy.strategy
val havoc : ?priority:float -> Tactical.selection -> Strategy.strategy
val separated : ?priority:float -> Tactical.selection -> Strategy.strategy
val instance : ?priority:float -> Tactical.selection -> Tactical.selection list -> Strategy.strategy
val lemma : ?priority:float -> ?at:Tactical.selection -> string -> Tactical.selection list -> Strategy.strategy
val intuition : ?priority:float -> Tactical.selection -> Strategy.strategy
val range : ?priority:float -> Tactical.selection -> vmin:int -> vmax:int -> Strategy.strategy
val split : ?priority:float -> Tactical.selection -> Strategy.strategy
val definition : ?priority:float -> Tactical.selection -> Strategy.strategy

Registered Heuristics

val auto_split : Strategy.heuristic
val auto_range : Strategy.heuristic
module Range : sig ... end

Trusted Tactical Process

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

val t_absurd : Tactical.process

Find a contradiction.

val t_id : Tactical.process

Keep goal unchanged.

val t_finally : string -> Tactical.process

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

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

Apply a description to each sub-goal

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

Split with p and not p.

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

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.

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

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

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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog 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