package frama-c

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

Module Wp.LetifySource

Sourcemodule Ground : sig ... end
Sourcemodule Sigma : sig ... end
Sourcemodule Defs : sig ... end

bind sigma defs xs select definitions in defs targeting variables xs. The result is a new substitution that potentially augment sigma with definitions for xs (and others).

Sourceval add_definitions : Sigma.t -> Defs.t -> Lang.F.Vars.t -> Lang.F.pred list -> Lang.F.pred list

add_definitions sigma defs xs ps keep all definitions of variables xs from sigma that comes from defs. They are added to ps.

Sourcemodule Split : sig ... end

Pruning strategy ; selects most occurring literals to split cases.