summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
l---------clang/include/clang/Analysis/Analyses/.#Interval.h1
l---------clang/include/clang/Analysis/Analyses/.#Interval_flymake.h1
-rw-r--r--clang/include/clang/Analysis/Analyses/Interval.h2
-rw-r--r--clang/lib/Analysis/Interval.cpp34
l---------clang/lib/StaticAnalyzer/Checkers/.#IntervalTest.cpp1
-rw-r--r--clang/lib/StaticAnalyzer/Checkers/IntervalTest.cpp2
-rw-r--r--impl/test/14.eqns3
-rw-r--r--impl/test/14.soln3
8 files changed, 36 insertions, 11 deletions
diff --git a/clang/include/clang/Analysis/Analyses/.#Interval.h b/clang/include/clang/Analysis/Analyses/.#Interval.h
deleted file mode 120000
index 235903b..0000000
--- a/clang/include/clang/Analysis/Analyses/.#Interval.h
+++ /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/include/clang/Analysis/Analyses/.#Interval_flymake.h b/clang/include/clang/Analysis/Analyses/.#Interval_flymake.h
deleted file mode 120000
index 235903b..0000000
--- a/clang/include/clang/Analysis/Analyses/.#Interval_flymake.h
+++ /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/include/clang/Analysis/Analyses/Interval.h b/clang/include/clang/Analysis/Analyses/Interval.h
index 6c0d5cf..8bb8d0f 100644
--- a/clang/include/clang/Analysis/Analyses/Interval.h
+++ b/clang/include/clang/Analysis/Analyses/Interval.h
@@ -33,7 +33,7 @@ public:
IntervalAnalysis(AnalysisDeclContext &analysisContext);
virtual ~IntervalAnalysis();
- void runOnAllBlocks();
+ void runOnAllBlocks(const Decl&);
static IntervalAnalysis *create(AnalysisDeclContext &analysisContext) {
return new IntervalAnalysis(analysisContext);
diff --git a/clang/lib/Analysis/Interval.cpp b/clang/lib/Analysis/Interval.cpp
index 3a82344..7096d75 100644
--- a/clang/lib/Analysis/Interval.cpp
+++ b/clang/lib/Analysis/Interval.cpp
@@ -637,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;
@@ -667,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());
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);
}
}
};
diff --git a/impl/test/14.eqns b/impl/test/14.eqns
new file mode 100644
index 0000000..6c28481
--- /dev/null
+++ b/impl/test/14.eqns
@@ -0,0 +1,3 @@
+x = 0
+y = max(x, z)
+z = y + 1
diff --git a/impl/test/14.soln b/impl/test/14.soln
new file mode 100644
index 0000000..c0301bb
--- /dev/null
+++ b/impl/test/14.soln
@@ -0,0 +1,3 @@
+x = 0
+y = inf
+z = inf