使用 JSON options

check_rules 文件除了能够指定哪些规则的检查器会被运行，还能够通过 JSON options 来单独控制某些检查器的行为。

对于 Z3 约束求解器，我们提供了三种模式：

（1）always

始终使用 Z3 约束求解器，这可能会降低检查的速度。

（2）cross check（默认模式）

只在发现了问题的时候使用 Z3 约束求解器再次检验，发挥其消除误报的能力。

（3）never

不使用 Z3 约束求解器。

对于每个使用了 Clang Static Analyzer 的检查器，都可以使用 JSON options 单独为其配置 Z3 约束求解器的使用模式。

以 MISRA C:2012 规则 18.1 为例，展示如何在 check_rules 中配置三种 Z3 约束求解器的使用模式：

（1）always

misra_c_2012/rule_18_1 {"use-z3":"always"}

（2）cross check

misra_c_2012/rule_18_1 {"use-z3":"crosscheck"}

（3）never

misra_c_2012/rule_18_1 {"use-z3":"never"}