sig
type mode = {
kf : Cil_types.kernel_function;
bhv : Cil_types.funbehavior;
infos : CfgInfos.t;
}
type props = [ `All | `Names of string list | `PropId of Property.t ]
module Make :
functor (W : Mcfg.S) ->
sig
exception NonNaturalLoop of Cil_types.location
val compute :
mode:CfgCalculus.mode -> props:CfgCalculus.props -> W.t_prop
end
end