C++: Fixed false negative

This commit is contained in:
Mathias Vorreiter Pedersen
2020-01-07 22:20:04 +01:00
parent 229da0a9c0
commit db08076fed
2 changed files with 7 additions and 4 deletions

View File

@@ -132,6 +132,8 @@ class SubAnalyzableExpr extends AnalyzableExpr, SubExpr {
}
class VarAnalyzableExpr extends AnalyzableExpr, VariableAccess {
VarAnalyzableExpr() { not exists(this.getQualifier()) }
override float maxValue() {
exists(SsaDefinition def, Variable v |
def.getAUse(v) = this and
@@ -140,7 +142,7 @@ class VarAnalyzableExpr extends AnalyzableExpr, VariableAccess {
// variable the largest possible value it can hold
if exists(def.getDefiningValue(v))
then result = def.getDefiningValue(v).(AnalyzableExpr).maxValue()
else result = exprMaxVal(this)
else result = upperBound(this)
)
}
@@ -149,7 +151,7 @@ class VarAnalyzableExpr extends AnalyzableExpr, VariableAccess {
def.getAUse(v) = this and
if exists(def.getDefiningValue(v))
then result = def.getDefiningValue(v).(AnalyzableExpr).minValue()
else result = exprMinVal(this)
else result = lowerBound(this)
)
}
}
@@ -206,9 +208,9 @@ where
) and
e.(Literal).getType().getSize() = t2.getSize()
) and
// only report if cannot prove that the result of the
// only report if we cannot prove that the result of the
// multiplication will be less (resp. greater) than the
// maximum (resp. minimum) number we can store.
// maximum (resp. minimum) number we can compute.
overflows(me, t1)
select me,
"Multiplication result may overflow '" + me.getType().toString() + "' before it is converted to '"

View File

@@ -10,3 +10,4 @@
| IntMultToLong.c:99:14:99:35 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'unsigned long'. |
| IntMultToLong.c:103:14:103:46 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'unsigned long'. |
| IntMultToLong.c:108:14:108:78 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'unsigned long'. |
| IntMultToLong.c:119:14:119:26 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'unsigned long'. |