template for a call graph object

src/main/scala/leon/CallGraph.scala

+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
+  }
+
+
+}