Control.AnalyzeCFG
Given a Cfg
, a Spec
, and an Inc
, computes the solution to MCP.Path
module Cfg : MyCFG.CfgBidirSkip
module Spec : Analyses.Spec
module Inc : Constraints.Increment
module SpecSys : Analyses.SpecSys with module Spec = Spec
module PostSolverArg : sig ... end
module Slvr : sig ... end
module CompareGlobSys : sig ... end
module RT : sig ... end
module LT : sig ... end
module Result : sig ... end
module Query : sig ... end
val solver2source_result : SpecSys.Spec.D.t SpecSys.LHT.t -> Result.t
val analyze : GoblintCil.file -> Analyses.fundecs -> unit
The main function to preform the selected analyses.