package leon import leon.purescala.Definitions._ import leon.purescala.Trees._ import leon.purescala.TypeTrees._ import leon.purescala.Common._ class CallGraph(val program: Program) { sealed abstract class ProgramPoint case class FunctionStart(fd: FunDef) extends ProgramPoint case class ExpressionPoint(wp: Expr) extends ProgramPoint sealed abstract class EdgeLabel case class ConditionLabel(expr: Expr) extends EdgeLabel { require(expr.getType == BooleanType) } case class FunctionInvocLabel(fd: FunDef, args: List[Expr]) extends EdgeLabel { require(args.zip(fd.args).forall(p => p._1.getType == p._2.getType)) } private lazy val graph: Map[ProgramPoint, Set[EdgeLabel]] = buildGraph private def buildGraph: Map[ProgramPoint, Set[EdgeLabel]] = { null } }