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