Skip to content

Implement package FloatingPoint #887

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 4 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
@@ -1,3 +1,30 @@
problems
| test.c:12:8:12:9 | l2 | test.c:8:14:8:20 | ... / ... | test.c:12:8:12:9 | l2 | Possibly infinite float value $@ flows to divisor, which would silently underflow and produce zero. | test.c:8:14:8:20 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:13:8:13:9 | l3 | test.c:8:14:8:20 | ... / ... | test.c:13:8:13:9 | l3 | Possibly infinite float value $@ flows to divisor, which would silently underflow and produce zero. | test.c:8:14:8:20 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:18:8:18:9 | l2 | test.c:8:14:8:20 | ... / ... | test.c:18:3:18:9 | l2 | Possibly infinite float value $@ flows to cast to integer. | test.c:8:14:8:20 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:19:8:19:9 | l3 | test.c:8:14:8:20 | ... / ... | test.c:19:3:19:9 | l3 | Possibly infinite float value $@ flows to cast to integer. | test.c:8:14:8:20 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:27:19:27:20 | l2 | test.c:8:14:8:20 | ... / ... | test.c:27:19:27:20 | l2 | Possibly infinite float value $@ flows to divisor, which would silently underflow and produce zero. | test.c:8:14:8:20 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:28:19:28:20 | l3 | test.c:8:14:8:20 | ... / ... | test.c:28:19:28:20 | l3 | Possibly infinite float value $@ flows to divisor, which would silently underflow and produce zero. | test.c:8:14:8:20 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:38:8:38:9 | l7 | test.c:31:14:32:15 | ... / ... | test.c:38:3:38:9 | l7 | Possibly infinite float value $@ flows to cast to integer. | test.c:31:14:32:15 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:61:11:61:17 | ... / ... | test.c:61:5:61:18 | ... / ... | test.c:61:5:61:18 | ... / ... | Possibly infinite float value $@ flows to cast to integer. | test.c:61:11:61:17 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:66:11:66:19 | ... / ... | test.c:66:5:66:20 | ... / ... | test.c:66:5:66:20 | ... / ... | Possibly infinite float value $@ flows to cast to integer. | test.c:66:11:66:19 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:72:20:72:28 | ... / ... | test.c:72:14:72:29 | ... / ... | test.c:72:14:72:29 | ... / ... | Possibly infinite float value $@ flows to cast to integer. | test.c:72:20:72:28 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:75:24:75:32 | ... / ... | test.c:75:18:75:33 | ... / ... | test.c:75:18:75:33 | ... / ... | Possibly infinite float value $@ flows to cast to integer. | test.c:75:24:75:32 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:79:10:79:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:79:5:79:12 | l12 | Possibly infinite float value $@ flows to cast to integer. | test.c:77:15:77:21 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:87:10:87:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:87:5:87:12 | l12 | Possibly infinite float value $@ flows to cast to integer. | test.c:77:15:77:21 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:91:10:91:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:91:5:91:12 | l12 | Possibly infinite float value $@ flows to cast to integer. | test.c:77:15:77:21 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:93:10:93:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:93:5:93:12 | l12 | Possibly infinite float value $@ flows to cast to integer. | test.c:77:15:77:21 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:99:10:99:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:99:5:99:12 | l12 | Possibly infinite float value $@ flows to cast to integer. | test.c:77:15:77:21 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:105:10:105:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:105:5:105:12 | l12 | Possibly infinite float value $@ flows to cast to integer. | test.c:77:15:77:21 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:111:10:111:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:111:5:111:12 | l12 | Possibly infinite float value $@ flows to cast to integer. | test.c:77:15:77:21 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:114:21:114:23 | l12 | test.c:77:15:77:21 | ... / ... | test.c:114:16:114:23 | l12 | Possibly infinite float value $@ flows to cast to integer. | test.c:77:15:77:21 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:117:28:117:30 | l12 | test.c:77:15:77:21 | ... / ... | test.c:117:23:117:30 | l12 | Possibly infinite float value $@ flows to cast to integer. | test.c:77:15:77:21 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:120:25:120:27 | l12 | test.c:77:15:77:21 | ... / ... | test.c:120:20:120:27 | l12 | Possibly infinite float value $@ flows to cast to integer. | test.c:77:15:77:21 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:163:9:164:15 | ... / ... | test.c:163:3:164:16 | ... / ... | test.c:163:3:164:16 | ... / ... | Possibly infinite float value $@ flows to cast to integer. | test.c:163:9:164:15 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:175:32:175:32 | p | test.c:189:51:189:59 | ... / ... | test.c:175:27:175:32 | p | Possibly infinite float value $@ computed in function $@ flows to cast to integer. | test.c:189:51:189:59 | ... / ... | from division by zero | test.c:189:6:189:24 | addInfThenCastToInt | addInfThenCastToInt |
| test.c:175:32:175:32 | p | test.c:193:13:194:15 | ... / ... | test.c:175:27:175:32 | p | Possibly infinite float value $@ computed in function $@ flows to cast to integer. | test.c:193:13:194:15 | ... / ... | from division by zero | test.c:192:6:192:7 | f2 | f2 |
| test.c:175:32:175:32 | p | test.c:204:19:204:27 | ... / ... | test.c:175:27:175:32 | p | Possibly infinite float value $@ computed in function $@ flows to cast to integer. | test.c:204:19:204:27 | ... / ... | from division by zero | test.c:192:6:192:7 | f2 | f2 |
| test.c:185:18:185:18 | p | test.c:200:25:200:33 | ... / ... | test.c:185:13:185:18 | p | Possibly infinite float value $@ computed in function $@ flows to cast to integer. | test.c:200:25:200:33 | ... / ... | from division by zero | test.c:192:6:192:7 | f2 | f2 |
edges
| test.c:8:14:8:20 | ... / ... | test.c:8:14:8:20 | ... / ... | provenance | |
| test.c:8:14:8:20 | ... / ... | test.c:9:14:9:16 | - ... | provenance | Config |
Expand Down Expand Up @@ -83,31 +110,4 @@ nodes
| test.c:206:21:206:31 | ... + ... | semmle.label | ... + ... |
| test.c:208:13:208:21 | middleInf | semmle.label | middleInf |
| test.c:210:23:210:31 | middleInf | semmle.label | middleInf |
subpaths
#select
| test.c:12:8:12:9 | l2 | test.c:8:14:8:20 | ... / ... | test.c:12:8:12:9 | l2 | Possibly infinite float value $@ flows to divisor, which would silently underflow and produce zero. | test.c:8:14:8:20 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:13:8:13:9 | l3 | test.c:8:14:8:20 | ... / ... | test.c:13:8:13:9 | l3 | Possibly infinite float value $@ flows to divisor, which would silently underflow and produce zero. | test.c:8:14:8:20 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:18:8:18:9 | l2 | test.c:8:14:8:20 | ... / ... | test.c:18:3:18:9 | l2 | Possibly infinite float value $@ flows to cast to integer. | test.c:8:14:8:20 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:19:8:19:9 | l3 | test.c:8:14:8:20 | ... / ... | test.c:19:3:19:9 | l3 | Possibly infinite float value $@ flows to cast to integer. | test.c:8:14:8:20 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:27:19:27:20 | l2 | test.c:8:14:8:20 | ... / ... | test.c:27:19:27:20 | l2 | Possibly infinite float value $@ flows to divisor, which would silently underflow and produce zero. | test.c:8:14:8:20 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:28:19:28:20 | l3 | test.c:8:14:8:20 | ... / ... | test.c:28:19:28:20 | l3 | Possibly infinite float value $@ flows to divisor, which would silently underflow and produce zero. | test.c:8:14:8:20 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:38:8:38:9 | l7 | test.c:31:14:32:15 | ... / ... | test.c:38:3:38:9 | l7 | Possibly infinite float value $@ flows to cast to integer. | test.c:31:14:32:15 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:61:11:61:17 | ... / ... | test.c:61:5:61:18 | ... / ... | test.c:61:5:61:18 | ... / ... | Possibly infinite float value $@ flows to cast to integer. | test.c:61:11:61:17 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:66:11:66:19 | ... / ... | test.c:66:5:66:20 | ... / ... | test.c:66:5:66:20 | ... / ... | Possibly infinite float value $@ flows to cast to integer. | test.c:66:11:66:19 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:72:20:72:28 | ... / ... | test.c:72:14:72:29 | ... / ... | test.c:72:14:72:29 | ... / ... | Possibly infinite float value $@ flows to cast to integer. | test.c:72:20:72:28 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:75:24:75:32 | ... / ... | test.c:75:18:75:33 | ... / ... | test.c:75:18:75:33 | ... / ... | Possibly infinite float value $@ flows to cast to integer. | test.c:75:24:75:32 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:79:10:79:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:79:5:79:12 | l12 | Possibly infinite float value $@ flows to cast to integer. | test.c:77:15:77:21 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:87:10:87:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:87:5:87:12 | l12 | Possibly infinite float value $@ flows to cast to integer. | test.c:77:15:77:21 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:91:10:91:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:91:5:91:12 | l12 | Possibly infinite float value $@ flows to cast to integer. | test.c:77:15:77:21 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:93:10:93:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:93:5:93:12 | l12 | Possibly infinite float value $@ flows to cast to integer. | test.c:77:15:77:21 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:99:10:99:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:99:5:99:12 | l12 | Possibly infinite float value $@ flows to cast to integer. | test.c:77:15:77:21 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:105:10:105:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:105:5:105:12 | l12 | Possibly infinite float value $@ flows to cast to integer. | test.c:77:15:77:21 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:111:10:111:12 | l12 | test.c:77:15:77:21 | ... / ... | test.c:111:5:111:12 | l12 | Possibly infinite float value $@ flows to cast to integer. | test.c:77:15:77:21 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:114:21:114:23 | l12 | test.c:77:15:77:21 | ... / ... | test.c:114:16:114:23 | l12 | Possibly infinite float value $@ flows to cast to integer. | test.c:77:15:77:21 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:117:28:117:30 | l12 | test.c:77:15:77:21 | ... / ... | test.c:117:23:117:30 | l12 | Possibly infinite float value $@ flows to cast to integer. | test.c:77:15:77:21 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:120:25:120:27 | l12 | test.c:77:15:77:21 | ... / ... | test.c:120:20:120:27 | l12 | Possibly infinite float value $@ flows to cast to integer. | test.c:77:15:77:21 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:163:9:164:15 | ... / ... | test.c:163:3:164:16 | ... / ... | test.c:163:3:164:16 | ... / ... | Possibly infinite float value $@ flows to cast to integer. | test.c:163:9:164:15 | ... / ... | from division by zero | test.c:6:6:6:7 | f1 | f1 |
| test.c:175:32:175:32 | p | test.c:189:51:189:59 | ... / ... | test.c:175:27:175:32 | p | Possibly infinite float value $@ computed in function $@ flows to cast to integer. | test.c:189:51:189:59 | ... / ... | from division by zero | test.c:189:6:189:24 | addInfThenCastToInt | addInfThenCastToInt |
| test.c:175:32:175:32 | p | test.c:193:13:194:15 | ... / ... | test.c:175:27:175:32 | p | Possibly infinite float value $@ computed in function $@ flows to cast to integer. | test.c:193:13:194:15 | ... / ... | from division by zero | test.c:192:6:192:7 | f2 | f2 |
| test.c:175:32:175:32 | p | test.c:204:19:204:27 | ... / ... | test.c:175:27:175:32 | p | Possibly infinite float value $@ computed in function $@ flows to cast to integer. | test.c:204:19:204:27 | ... / ... | from division by zero | test.c:192:6:192:7 | f2 | f2 |
| test.c:185:18:185:18 | p | test.c:200:25:200:33 | ... / ... | test.c:185:13:185:18 | p | Possibly infinite float value $@ computed in function $@ flows to cast to integer. | test.c:200:25:200:33 | ... / ... | from division by zero | test.c:192:6:192:7 | f2 | f2 |
subpaths
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
// GENERATED FILE - DO NOT MODIFY
import codingstandards.cpp.rules.misuseofinfinitefloatingpointvalue.MisuseOfInfiniteFloatingPointValue

class TestFileQuery extends MisuseOfInfiniteFloatingPointValueSharedQuery, TestQuery { }
Original file line number Diff line number Diff line change
Expand Up @@ -33,10 +33,10 @@ void f1(float p1) {
float l8 = 0.0 / 0.0;

(int)l4; // COMPLIANT
(int)l5; // NON_COMPLIANT: Casting NaN to int
(int)l6; // NON_COMPLIANT: Casting NaN to int
(int)l7; // NON_COMPLIANT: Casting NaN to int
(int)l8; // NON_COMPLIANT: Casting NaN to int
(int)l5; // COMPLIANT: Casting NaN to int
(int)l6; // COMPLIANT: Casting NaN to int
(int)l7; // NON_COMPLIANT: Casting Infinity to int
(int)l8; // COMPLIANT: Casting NaN to int

l4 == 0; // COMPLIANT
l4 != 0; // COMPLIANT
Expand All @@ -58,21 +58,21 @@ void f1(float p1) {
if (l9 != 0) {
(int)(l9 / l9); // COMPLIANT: l9 is not zero
} else {
(int)(l9 / l9); // NON_COMPLIANT: Guarded to not be NaN
(int)(l9 / l9); // NON_COMPLIANT[False positive]: Guarded to not be NaN
}

float l10 = 0;
if (l10 == 0) {
(int)(l10 / l10); // NON_COMPLIANT: Casting NaN to integer
(int)(l10 / l10); // NON_COMPLIANT[False positive]: Casting NaN to integer
} else {
(int)(l10 / l10); // COMPLIANT: Guarded to not be NaN
}

float l11 = 0;
l11 == 0 ? (int)(l11 / l11) : 0; // NON_COMPLIANT
l11 == 0 ? (int)(l11 / l11) : 0; // NON_COMPLIANT[False positive]
l11 == 0 ? 0 : (int)(l11 / l11); // COMPLIANT
l11 != 0 ? (int)(l11 / l11) : 0; // COMPLIANT
l11 != 0 ? 0 : (int)(l11 / l11); // NON_COMPLIANT
l11 != 0 ? 0 : (int)(l11 / l11); // NON_COMPLIANT[False positive]

float l12 = 1.0 / 0;
if (isinf(l12)) {
Expand Down Expand Up @@ -123,29 +123,29 @@ void f1(float p1) {
if (isinf(l13)) {
(int)l13; // COMPLIANT: Guarded not to be NaN
} else {
(int)l13; // NON_COMPLIANT: Casting NaN to integer
(int)l13; // COMPLIANT: Casting NaN to integer
}

if (isinf(l13) == 1) {
(int)l13; // COMPLIANT: Guarded not to be NaN (must be +Infinity)
} else {
(int)l13; // NON_COMPLIANT: Casting NaN to integer
(int)l13; // COMPLIANT: Casting NaN to integer
}

if (isfinite(l13)) {
(int)l13; // COMPLIANT: Guarded not to be NaN
} else {
(int)l13; // NON_COMPLIANT: Casting NaN to integer
(int)l13; // COMPLIANT: Casting NaN to integer
}

if (isnormal(l13)) {
(int)l13; // COMPLIANT: Guarded not to be NaN
} else {
(int)l13; // NON_COMPLIANT: Casting NaN to integer
(int)l13; // COMPLIANT: Casting NaN to integer
}

if (isnan(l13)) {
(int)l13; // NON_COMPLIANT: Casting NaN to integer
(int)l13; // COMPLIANT: Casting NaN to integer
} else {
(int)l13; // COMPLIANT: Guarded not to be NaN
}
Expand All @@ -154,21 +154,21 @@ void f1(float p1) {
: 0; // COMPLIANT: Checked infinite, therefore not NaN, before use
isinf(l13) ? 0 : (int)l13; // COMPLIANT: Check on wrong branch
isfinite(l13) ? (int)l13 : 0; // COMPLIANT: Checked finite before use
isfinite(l13) ? 0 : (int)l13; // NON_COMPLIANT: Checked on wrong branch
isnan(l13) ? (int)l13 : 0; // NON_COMPLIANT: Check on wrong branch
isfinite(l13) ? 0 : (int)l13; // COMPLIANT: Checked on wrong branch
isnan(l13) ? (int)l13 : 0; // COMPLIANT: Check on wrong branch
isnan(l13) ? 0 : (int)l13; // COMPLIANT: Checked not NaN before use

(int)pow(2, p1); // NON_COMPLIANT: likely to be Infinity
(int)pow(2, p1); // NON_COMPLIANT[False negative]: likely to be Infinity
(int)pow(2, sin(p1)); // COMPLIANT: not likely to be Infinity
(int)(1 /
sin(p1)); // NON_COMPLIANT: possible infinity from zero in denominator
(int)(1 / log(p1)); // COMPLIANT: not possibly zero in denominator
(int)pow(p1, p1); // NON_COMPLIANT: NaN if p1 is zero
(int)pow(p1, p1); // COMPLIANT: NaN if p1 is zero
if (p1 != 0) {
(int)pow(p1, p1); // COMPLIANT: p1 is not zero
}

(int)acos(p1); // NON_COMPLIANT: NaN if p1 is not within -1..1
(int)acos(p1); // COMPLIANT: NaN if p1 is not within -1..1
(int)acos(cos(p1)); // COMPLIANT: cos(p1) is within -1..1
}

Expand All @@ -192,21 +192,21 @@ void addNaNThenCastToInt(float p) { castToInt(p + 0.0 / 0.0); }
void f2() {
castToInt(1.0 /
0.0); // NON_COMPLIANT: Infinity flows to denominator in division
castToInt(0.0 / 0.0); // NON_COMPLIANT: NaN flows to denominator in division
castToInt(0.0 / 0.0); // COMPLIANT
checkBeforeCastToInt(1.0 / 0.0); // COMPLIANT
checkBeforeCastToInt(0.0 / 0.0); // COMPLIANT
addOneThenCastToInt(1.0 / 0.0); // NON_COMPLIANT[False negative]
addOneThenCastToInt(0.0 / 0.0); // NON_COMPLIANT
castToIntToFloatToInt(1.0 / 0.0); // NON_COMPLIANT
castToIntToFloatToInt(0.0 / 0.0); // NON_COMPLIANT
castToIntToFloatToInt(0.0 / 0.0); // COMPLIANT

// Check that during flow analysis, we only report the true root cause:
float rootInf = 1.0 / 0.0;
float rootNaN = 0.0 / 0.0;
float middleInf = rootInf + 1;
float middleNaN = rootNaN + 1;
castToInt(middleInf); // NON_COMPLIANT
castToInt(middleNaN); // NON_COMPLIANT
castToInt(middleNaN); // COMPLIANT
addInfThenCastToInt(middleInf); // NON_COMPLIANT
addNaNThenCastToInt(middleNaN); // NON_COMPLIANT
addNaNThenCastToInt(middleNaN); // COMPLIANT
}
Loading
Loading