diff --git a/src/main/scala/leon/CallGraph.scala b/src/main/scala/leon/CallGraph.scala new file mode 100644 index 0000000000000000000000000000000000000000..952e8499ed0a9898af06b6ae1383518b625ee4ca --- /dev/null +++ b/src/main/scala/leon/CallGraph.scala @@ -0,0 +1,30 @@ +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 + } + + +}