Frama-C API - 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.