mirror of
https://github.com/Z3Prover/z3
synced 2025-10-01 05:29:28 +00:00
add analysis
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
bda98d8da4
commit
ae55b6fa1e
2 changed files with 128 additions and 0 deletions
87
codeql/custom_queries/FindUnderspecified.ql
Normal file
87
codeql/custom_queries/FindUnderspecified.ql
Normal file
|
@ -0,0 +1,87 @@
|
|||
/**
|
||||
|
||||
* Finds function calls with arguments that have unspecified evaluation order.
|
||||
|
||||
*
|
||||
|
||||
* @name Unspecified argument evaluation order
|
||||
|
||||
* @kind problem
|
||||
|
||||
* @problem.severity warning
|
||||
|
||||
* @id cpp/z3/unspecevalorder
|
||||
|
||||
*/
|
||||
|
||||
|
||||
|
||||
import cpp
|
||||
|
||||
|
||||
|
||||
predicate isPureFunc(Function f) {
|
||||
|
||||
f.getName() = "m" or
|
||||
|
||||
not exists(Assignment a | a.getEnclosingFunction() = f) and
|
||||
|
||||
forall(FunctionCall g | g.getEnclosingFunction() = f | isPureFunc(g.getTarget()))
|
||||
|
||||
}
|
||||
|
||||
|
||||
|
||||
predicate sideEffectfulArgument(Expr a) {
|
||||
|
||||
exists(Function f | f = a.(FunctionCall).getTarget() |
|
||||
|
||||
not f instanceof ConstMemberFunction and
|
||||
|
||||
not isPureFunc(f)
|
||||
|
||||
)
|
||||
|
||||
or
|
||||
|
||||
exists(ArrayExpr b | b = a.(ArrayExpr) |
|
||||
|
||||
sideEffectfulArgument(b.getArrayBase()) or sideEffectfulArgument(b.getArrayOffset())
|
||||
|
||||
)
|
||||
|
||||
or
|
||||
|
||||
exists(Assignment b | b = a)
|
||||
|
||||
or
|
||||
|
||||
exists(BinaryOperation b | b = a | sideEffectfulArgument(b.getAnOperand()))
|
||||
|
||||
or
|
||||
|
||||
exists(UnaryOperation b | b = a | sideEffectfulArgument(b.getOperand()))
|
||||
|
||||
}
|
||||
|
||||
|
||||
|
||||
from FunctionCall f, Expr a, int i, Expr b, int j where
|
||||
|
||||
i < j and
|
||||
|
||||
f.getTarget().getName() != "operator&&" and
|
||||
|
||||
f.getTarget().getName() != "operator||" and
|
||||
|
||||
a = f.getArgument(i) and
|
||||
|
||||
b = f.getArgument(j) and
|
||||
|
||||
sideEffectfulArgument(a) and
|
||||
|
||||
sideEffectfulArgument(b)
|
||||
|
||||
select f, "potentially unspecified evaluation order of function arguments: $@ and $@", a,
|
||||
|
||||
i.toString(), b, j.toString()
|
Loading…
Add table
Add a link
Reference in a new issue