Control.AnalyzeCFGGiven a Cfg, a Spec, and an Inc, computes the solution to MCP.Path
module Cfg : MyCFG.CfgBidirmodule Spec : Analyses.Specmodule Inc : Constraints.Incrementmodule SpecSys : Analyses.SpecSys with module Spec = Specmodule PostSolverArg : sig ... endmodule Slvr : sig ... endmodule CompareGlobSys : sig ... endmodule RT : sig ... endmodule LT : sig ... endmodule Result : sig ... endmodule Query : sig ... endval solver2source_result : SpecSys.Spec.D.t SpecSys.LHT.t -> Result.tval analyze :
GoblintCil.file ->
Analyses.fundecs ->
GoblintCil.stmt list CfgTools.CfgEdgeH.t ->
unitThe main function to preform the selected analyses.