From 2b4481f05baca3dbec62bbc68ce1750e3b68d20d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Mon, 14 May 2012 21:34:38 +0000
Subject: [PATCH] template for a call graph object
---
src/main/scala/leon/CallGraph.scala | 30 +++++++++++++++++++++++++++++
1 file changed, 30 insertions(+)
create mode 100644 src/main/scala/leon/CallGraph.scala
diff --git a/src/main/scala/leon/CallGraph.scala b/src/main/scala/leon/CallGraph.scala
new file mode 100644
index 000000000..952e8499e
--- /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
+ }
+
+
+}
--
GitLab