Letify (frama-c-wp.Wp.Letify)

module Ground : sig ... end

module Sigma : sig ... end

module Defs : sig ... end

val bind : Sigma.t -> Defs.t -> Lang.F.Vars.t -> Sigma.t

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

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

module Split : sig ... end

Pruning strategy ; selects most occurring literals to split cases.