package frama-c

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

Sequent Cleaning

Erase parts of a predicate that do not satisfies the condition. The erased parts are replaced by:

  • true when ~polarity:false (for hypotheses)
  • false when ~polarity:true (for goals)

Hence, we have:

  • filter ~polarity:true f p ==> p
  • p ==> filter ~polarity:false f p

See theory/filtering.why for proofs.

val filter : polarity:bool -> (Lang.F.pred -> bool) -> Lang.F.pred -> Lang.F.pred
val compute : ?anti:bool -> Conditions.sequent -> Conditions.sequent