[PATCH] D83677: [analyzer] Rework Z3 requirements in the CSA testsuite

[Artem Dergachev via Phabricator via llvm-commits]

NoQ added a comment.

Folks, please announce your overall plan for Z3 (unless i missed it). It looks like you are planning to actively support Z3 as a //constraint manager//, i.e. invoke it on every `assume()`? Did you consider my usual suggestion to only apply it to refuting non-buggy states in order to combat your false negatives similarly to how our current Z3 refutation refutes buggy states to combat false positives?



================
Comment at: clang/www/analyzer/checker_dev_manual.html:534
     <pre class="code">
     $ <b>bin/llvm-lit -sv ../llvm/tools/clang/test/Analysis</b>
     </pre>
----------------
Yeah, just delete this :)


================
Comment at: llvm/utils/lit/lit/llvm/config.py:412-413
             ToolSubst('%clang', command=self.config.clang, extra_args=additional_flags),
-            ToolSubst('%clang_analyze_cc1', command='%clang_cc1', extra_args=['-analyze', '%analyze', '-setup-static-analyzer']+additional_flags),
+            ToolSubst('%clang_analyze_cc1_range', command='%clang_cc1', extra_args=['-analyze', '-analyzer-constraints=range', '-setup-static-analyzer']+additional_flags),
+            ToolSubst('%clang_analyze_cc1_z3', command='%clang_cc1', extra_args=['-analyze', '-analyzer-constraints=z3', '-setup-static-analyzer']+additional_flags),
+            ToolSubst('%clang_analyze_cc1', command='%clang_cc1', extra_args=['-analyze', '%constraint_manager', '-setup-static-analyzer']+additional_flags),
----------------
I'm for longer names, "range" is too vague, "z3" is already ambiguous (does it mean as constraint manager or for refutation?).

`%clang_analyze_cc1_range_cm_only` would probably make more sense. It also looks more like a FIXME and tells that something's wrong with the test.


CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D83677/new/

https://reviews.llvm.org/D83677