functor (W : Mcfg.S) -> sig exception NonNaturalLoop of Cil_types.location val compute : mode:CfgCalculus.mode -> props:CfgCalculus.props -> W.t_prop end