[analyzer] Support generating and reasoning over more symbolic constraint types
Summary: Generate more IntSymExpr constraints, perform SVal simplification for IntSymExpr and SymbolCast constraints, and create fully symbolic SymExprs
Reviewers: zaks.anna, dcoughlin, NoQ, xazax.hun
Subscribers: mgorny, cfe-commits
Differential Revision: https://reviews.llvm.org/D28953
llvm-svn: 307833
diff --git a/clang/test/Analysis/analyzer_test.py b/clang/test/Analysis/analyzer_test.py
index 0aa2dbc..468bb24 100644
--- a/clang/test/Analysis/analyzer_test.py
+++ b/clang/test/Analysis/analyzer_test.py
@@ -1,3 +1,4 @@
+import copy
import lit.formats
import lit.TestRunner
@@ -8,18 +9,21 @@
results = []
# Parse any test requirements ('REQUIRES: ')
- saved_test = test
+ saved_test = copy.deepcopy(test)
lit.TestRunner.parseIntegratedTestScript(test)
+ # If the test does not require z3, drop it from the available features
+ # to satisfy tests that explicitly require !z3
if 'z3' not in test.requires:
+ test.config.available_features.discard('z3')
results.append(self.executeWithAnalyzeSubstitution(
- saved_test, litConfig, '-analyzer-constraints=range'))
+ test, litConfig, '-analyzer-constraints=range'))
- if results[-1].code == lit.Test.FAIL:
+ if results[-1].code != lit.Test.PASS:
return results[-1]
# If z3 backend available, add an additional run line for it
- if test.config.clang_staticanalyzer_z3 == '1':
+ if test.config.clang_staticanalyzer_z3 == '1' and '!z3' not in test.requires:
results.append(self.executeWithAnalyzeSubstitution(
saved_test, litConfig, '-analyzer-constraints=z3 -DANALYZER_CM_Z3'))