3 files changed, 32 insertions, 40 deletions

diff --git a/clang/lib/Analysis/Interval.cpp b/clang/lib/Analysis/Interval.cpp
index ac96107..7096d75 100644
--- a/clang/lib/Analysis/Interval.cpp
+++ b/clang/lib/Analysis/Interval.cpp
@@ -221,11 +221,6 @@ M merge_maps_with(const F& f, const M& left, const M& right) {
   return result;
 }
 
-template<>
-Vector minimum(const Vector& l, const Vector& r) {
-  return (l < r ? l : r);
-  return merge_maps_with(minimum<ZBar>, l, r);
-}
 template<class T>
 T max(const T& l, const T& r) {
   return (l < r ? l : r);
@@ -642,10 +637,16 @@ void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) {
 	  std::vector<EqnExpr*> plusArgs;
 	  for (int negate = 0; negate < 2; ++negate) {
 	    std::string var_name = negate ? negate_string(variables->first) : variables->first;
-	    std::vector<EqnExpr*> minArgs;
-	    minArgs.push_back(vars[var_name]);
-	    minArgs.push_back(&system.constant(cond[var_name]));
-	    plusArgs.push_back(&system.expression(new Minimum<ZBar>(), minArgs));
+            if (cond[var_name] == infinity<ZBar>()) {
+              plusArgs.push_back(vars[var_name]);
+            } else if (cond[var_name] == -infinity<ZBar>()) {
+              plusArgs.push_back(&system.constant(-infinity<ZBar>()));
+            } else {
+              std::vector<EqnExpr*> minArgs;
+              minArgs.push_back(vars[var_name]);
+              minArgs.push_back(&system.constant(cond[var_name]));
+              plusArgs.push_back(&system.expression(new Minimum<ZBar>(), minArgs));
+            }
 	  }
 
 	  std::vector<EqnExpr*> guard_args;
@@ -672,15 +673,31 @@ IntervalAnalysis :: IntervalAnalysis(AnalysisDeclContext &context)
 IntervalAnalysis :: ~IntervalAnalysis() {
 }
 
-void IntervalAnalysis::runOnAllBlocks() {
+void IntervalAnalysis::runOnAllBlocks(const Decl& decl) {
   const CFG *cfg = this->context->getCFG();
 
   cfg->dump(context->getASTContext().getLangOpts(),
             llvm::sys::Process::StandardErrHasColors());
 
-  EqnSys system;
+  EqnSys system; 
   BlockVars block_vars;
 
+  std::vector<EqnExpr*> infArg; 
+  infArg.push_back(&system.constant(infinity<ZBar>()));
+  std::set<std::string>& function_arguments = block_vars[&cfg->getEntry()];
+  std::string block_id = toString(cfg->getEntry().getBlockID());
+  if (const FunctionDecl* func = dyn_cast<const FunctionDecl>(&decl)) {
+    for (unsigned int i = func->getNumParams(); i > 0; i--) {
+      std::string name = func->getParamDecl(i-1)->getNameAsString();
+
+      function_arguments.insert(name); // add it to the first block's vars
+      function_arguments.insert(negate_string(name));  // add it to the first block's vars
+
+      system[system.variable(name + '-' + block_id + "-pre")] = &system.maxExpression(infArg); // set the vars to infinity in the system here
+      system[system.variable(negate_string(name) + '-' + block_id + "-pre")] = &system.maxExpression(infArg); // set the vars to infinity in the system here
+    }
+  }
+
   std::set<const CFGBlock*> seen;
   std::deque<const CFGBlock*> todo;
   todo.push_back(&cfg->getEntry());
@@ -702,39 +719,15 @@ void IntervalAnalysis::runOnAllBlocks() {
     }
   }
 
-  std::vector<EqnExpr*> a;
-
-  a.push_back(&system.constant(-infinity<ZBar>()));
-  a.push_back(&system.constant(0));
-  system[system.variable("x")] = &system.maxExpression(a);
-  a.clear();
-  
-  system.variable("y");
-
-  a.push_back(&system.variable("x"));
-  a.push_back(&system.variable("z"));
-  EqnExpr* minExpr = &system.expression(new Maximum<ZBar>(), a);
-  a.clear();
-
-  a.push_back(&system.constant(-infinity<ZBar>()));
-  a.push_back(minExpr);
-  system[system.variable("y")] = &system.maxExpression(a);
-  a.clear();
-
-  a.push_back(&system.constant(-infinity<ZBar>()));
-  a.push_back(&system.variable("y"));
-  system[system.variable("z")] = &system.maxExpression(a);
-
   llvm::errs() << toString(system) << "\n";
 
   system.indexMaxExpressions();
-  DynamicMaxStrategy<ZBar> strategy(system);
-  DynamicVariableAssignment<ZBar> rho(system, strategy);
-  strategy.setRho(rho);
+
+  Solver<ZBar> solver(system);
 
   for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
     EqnVar& var = system.variable(size - i - 1);
-    llvm::errs() << toString(var.name()) << " = " << toString(rho[var]) << "\n";
+    llvm::errs() << toString(var.name()) << " = " << toString(solver.solve(var)) << "\n";
   }
 }
 
diff --git a/clang/lib/StaticAnalyzer/Checkers/.#IntervalTest.cpp b/clang/lib/StaticAnalyzer/Checkers/.#IntervalTest.cpp
deleted file mode 120000
index 235903b..0000000
--- a/clang/lib/StaticAnalyzer/Checkers/.#IntervalTest.cpp
+++ /dev/null
@@ -1 +0,0 @@
-carlo@pc-4w14-0.cs.usyd.edu.au.1585:1347012043
\ No newline at end of file
diff --git a/clang/lib/StaticAnalyzer/Checkers/IntervalTest.cpp b/clang/lib/StaticAnalyzer/Checkers/IntervalTest.cpp
index 2f3e155..badb671 100644
--- a/clang/lib/StaticAnalyzer/Checkers/IntervalTest.cpp
+++ b/clang/lib/StaticAnalyzer/Checkers/IntervalTest.cpp
@@ -14,7 +14,7 @@ public:
   void checkASTCodeBody(const Decl *D, AnalysisManager& mgr,
                         BugReporter &BR) const {
     if (IntervalAnalysis *a = mgr.getAnalysis<IntervalAnalysis>(D)) {
-      a->runOnAllBlocks();
+      a->runOnAllBlocks(*D);
     }
   }
 };