C++: Fix an inequality that should be strict, but wasn't.

This commit is contained in:
Mathias Vorreiter Pedersen
2023-08-11 11:43:55 +01:00
parent 9aae174942
commit c0a54e90c9
5 changed files with 28 additions and 3 deletions

View File

@@ -167,7 +167,7 @@ private module SizeBarrier {
pragma[inline_late] pragma[inline_late]
Instruction getABarrierInstruction(int state) { Instruction getABarrierInstruction(int state) {
exists(int delta, int k | exists(int delta, int k |
state >= k + delta and state > k + delta and
// result <= "size of allocation" + delta + k // result <= "size of allocation" + delta + k
// <= "size of allocation" + state // <= "size of allocation" + state
result = getABarrierInstruction0(delta, k) result = getABarrierInstruction0(delta, k)
@@ -195,7 +195,7 @@ private module SizeBarrier {
ValidForStateFlow::flow(source, result) and ValidForStateFlow::flow(source, result) and
hasSize(_, source, state) and hasSize(_, source, state) and
ValidForStateConfig::isSink(result, delta, k) and ValidForStateConfig::isSink(result, delta, k) and
state >= k + delta state > k + delta
// so now we have: // so now we have:
// result <= "size of allocation" + delta + k // result <= "size of allocation" + delta + k
// <= "size of allocation" + state // <= "size of allocation" + state

View File

@@ -1,2 +1,6 @@
failures failures
testFailures testFailures
| test.cpp:308:5:308:11 | PointerAdd: access to array | Unexpected result: alloc=L304 |
| test.cpp:308:5:308:11 | PointerAdd: access to array | Unexpected result: alloc=L304-1 |
| test.cpp:725:5:725:11 | PointerAdd: access to array | Unexpected result: alloc=L722 |
| test.cpp:725:5:725:11 | PointerAdd: access to array | Unexpected result: alloc=L722-1 |

View File

@@ -129,6 +129,7 @@ edges
| test.cpp:271:14:271:21 | ... + ... | test.cpp:271:14:271:21 | ... + ... | | test.cpp:271:14:271:21 | ... + ... | test.cpp:271:14:271:21 | ... + ... |
| test.cpp:271:14:271:21 | ... + ... | test.cpp:274:5:274:10 | ... = ... | | test.cpp:271:14:271:21 | ... + ... | test.cpp:274:5:274:10 | ... = ... |
| test.cpp:271:14:271:21 | ... + ... | test.cpp:274:5:274:10 | ... = ... | | test.cpp:271:14:271:21 | ... + ... | test.cpp:274:5:274:10 | ... = ... |
| test.cpp:304:15:304:26 | new[] | test.cpp:308:5:308:29 | ... = ... |
| test.cpp:355:14:355:27 | new[] | test.cpp:356:15:356:23 | ... + ... | | test.cpp:355:14:355:27 | new[] | test.cpp:356:15:356:23 | ... + ... |
| test.cpp:355:14:355:27 | new[] | test.cpp:356:15:356:23 | ... + ... | | test.cpp:355:14:355:27 | new[] | test.cpp:356:15:356:23 | ... + ... |
| test.cpp:355:14:355:27 | new[] | test.cpp:357:24:357:30 | ... + ... | | test.cpp:355:14:355:27 | new[] | test.cpp:357:24:357:30 | ... + ... |
@@ -222,6 +223,7 @@ edges
| test.cpp:705:18:705:18 | q | test.cpp:706:12:706:13 | * ... | | test.cpp:705:18:705:18 | q | test.cpp:706:12:706:13 | * ... |
| test.cpp:711:13:711:26 | new[] | test.cpp:714:11:714:11 | q | | test.cpp:711:13:711:26 | new[] | test.cpp:714:11:714:11 | q |
| test.cpp:714:11:714:11 | q | test.cpp:705:18:705:18 | q | | test.cpp:714:11:714:11 | q | test.cpp:705:18:705:18 | q |
| test.cpp:722:13:722:22 | new[] | test.cpp:725:5:725:15 | ... = ... |
nodes nodes
| test.cpp:4:15:4:20 | call to malloc | semmle.label | call to malloc | | test.cpp:4:15:4:20 | call to malloc | semmle.label | call to malloc |
| test.cpp:5:15:5:22 | ... + ... | semmle.label | ... + ... | | test.cpp:5:15:5:22 | ... + ... | semmle.label | ... + ... |
@@ -314,6 +316,8 @@ nodes
| test.cpp:271:14:271:21 | ... + ... | semmle.label | ... + ... | | test.cpp:271:14:271:21 | ... + ... | semmle.label | ... + ... |
| test.cpp:271:14:271:21 | ... + ... | semmle.label | ... + ... | | test.cpp:271:14:271:21 | ... + ... | semmle.label | ... + ... |
| test.cpp:274:5:274:10 | ... = ... | semmle.label | ... = ... | | test.cpp:274:5:274:10 | ... = ... | semmle.label | ... = ... |
| test.cpp:304:15:304:26 | new[] | semmle.label | new[] |
| test.cpp:308:5:308:29 | ... = ... | semmle.label | ... = ... |
| test.cpp:355:14:355:27 | new[] | semmle.label | new[] | | test.cpp:355:14:355:27 | new[] | semmle.label | new[] |
| test.cpp:356:15:356:23 | ... + ... | semmle.label | ... + ... | | test.cpp:356:15:356:23 | ... + ... | semmle.label | ... + ... |
| test.cpp:356:15:356:23 | ... + ... | semmle.label | ... + ... | | test.cpp:356:15:356:23 | ... + ... | semmle.label | ... + ... |
@@ -372,6 +376,8 @@ nodes
| test.cpp:706:12:706:13 | * ... | semmle.label | * ... | | test.cpp:706:12:706:13 | * ... | semmle.label | * ... |
| test.cpp:711:13:711:26 | new[] | semmle.label | new[] | | test.cpp:711:13:711:26 | new[] | semmle.label | new[] |
| test.cpp:714:11:714:11 | q | semmle.label | q | | test.cpp:714:11:714:11 | q | semmle.label | q |
| test.cpp:722:13:722:22 | new[] | semmle.label | new[] |
| test.cpp:725:5:725:15 | ... = ... | semmle.label | ... = ... |
subpaths subpaths
#select #select
| test.cpp:6:14:6:15 | * ... | test.cpp:4:15:4:20 | call to malloc | test.cpp:6:14:6:15 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:4:15:4:20 | call to malloc | call to malloc | test.cpp:5:19:5:22 | size | size | | test.cpp:6:14:6:15 | * ... | test.cpp:4:15:4:20 | call to malloc | test.cpp:6:14:6:15 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:4:15:4:20 | call to malloc | call to malloc | test.cpp:5:19:5:22 | size | size |
@@ -393,6 +399,7 @@ subpaths
| test.cpp:254:9:254:16 | ... = ... | test.cpp:248:24:248:30 | call to realloc | test.cpp:254:9:254:16 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:248:24:248:30 | call to realloc | call to realloc | test.cpp:254:11:254:11 | i | i | | test.cpp:254:9:254:16 | ... = ... | test.cpp:248:24:248:30 | call to realloc | test.cpp:254:9:254:16 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:248:24:248:30 | call to realloc | call to realloc | test.cpp:254:11:254:11 | i | i |
| test.cpp:264:13:264:14 | * ... | test.cpp:260:13:260:24 | new[] | test.cpp:264:13:264:14 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:260:13:260:24 | new[] | new[] | test.cpp:261:19:261:21 | len | len | | test.cpp:264:13:264:14 | * ... | test.cpp:260:13:260:24 | new[] | test.cpp:264:13:264:14 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:260:13:260:24 | new[] | new[] | test.cpp:261:19:261:21 | len | len |
| test.cpp:274:5:274:10 | ... = ... | test.cpp:270:13:270:24 | new[] | test.cpp:274:5:274:10 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:270:13:270:24 | new[] | new[] | test.cpp:271:19:271:21 | len | len | | test.cpp:274:5:274:10 | ... = ... | test.cpp:270:13:270:24 | new[] | test.cpp:274:5:274:10 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:270:13:270:24 | new[] | new[] | test.cpp:271:19:271:21 | len | len |
| test.cpp:308:5:308:29 | ... = ... | test.cpp:304:15:304:26 | new[] | test.cpp:308:5:308:29 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:304:15:304:26 | new[] | new[] | test.cpp:308:8:308:10 | ... + ... | ... + ... |
| test.cpp:358:14:358:26 | * ... | test.cpp:355:14:355:27 | new[] | test.cpp:358:14:358:26 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@ + 1. | test.cpp:355:14:355:27 | new[] | new[] | test.cpp:356:20:356:23 | size | size | | test.cpp:358:14:358:26 | * ... | test.cpp:355:14:355:27 | new[] | test.cpp:358:14:358:26 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@ + 1. | test.cpp:355:14:355:27 | new[] | new[] | test.cpp:356:20:356:23 | size | size |
| test.cpp:359:14:359:32 | * ... | test.cpp:355:14:355:27 | new[] | test.cpp:359:14:359:32 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@ + 2. | test.cpp:355:14:355:27 | new[] | new[] | test.cpp:356:20:356:23 | size | size | | test.cpp:359:14:359:32 | * ... | test.cpp:355:14:355:27 | new[] | test.cpp:359:14:359:32 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@ + 2. | test.cpp:355:14:355:27 | new[] | new[] | test.cpp:356:20:356:23 | size | size |
| test.cpp:384:13:384:16 | * ... | test.cpp:377:14:377:27 | new[] | test.cpp:384:13:384:16 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:377:14:377:27 | new[] | new[] | test.cpp:378:20:378:23 | size | size | | test.cpp:384:13:384:16 | * ... | test.cpp:377:14:377:27 | new[] | test.cpp:384:13:384:16 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:377:14:377:27 | new[] | new[] | test.cpp:378:20:378:23 | size | size |
@@ -406,3 +413,4 @@ subpaths
| test.cpp:647:5:647:19 | ... = ... | test.cpp:642:14:642:31 | new[] | test.cpp:647:5:647:19 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:642:14:642:31 | new[] | new[] | test.cpp:647:8:647:14 | src_pos | src_pos | | test.cpp:647:5:647:19 | ... = ... | test.cpp:642:14:642:31 | new[] | test.cpp:647:5:647:19 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:642:14:642:31 | new[] | new[] | test.cpp:647:8:647:14 | src_pos | src_pos |
| test.cpp:701:15:701:16 | * ... | test.cpp:695:13:695:26 | new[] | test.cpp:701:15:701:16 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:695:13:695:26 | new[] | new[] | test.cpp:696:19:696:22 | size | size | | test.cpp:701:15:701:16 | * ... | test.cpp:695:13:695:26 | new[] | test.cpp:701:15:701:16 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:695:13:695:26 | new[] | new[] | test.cpp:696:19:696:22 | size | size |
| test.cpp:706:12:706:13 | * ... | test.cpp:711:13:711:26 | new[] | test.cpp:706:12:706:13 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:711:13:711:26 | new[] | new[] | test.cpp:712:19:712:22 | size | size | | test.cpp:706:12:706:13 | * ... | test.cpp:711:13:711:26 | new[] | test.cpp:706:12:706:13 | * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:711:13:711:26 | new[] | new[] | test.cpp:712:19:712:22 | size | size |
| test.cpp:725:5:725:15 | ... = ... | test.cpp:722:13:722:22 | new[] | test.cpp:725:5:725:15 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:722:13:722:22 | new[] | new[] | test.cpp:725:8:725:10 | ... + ... | ... + ... |

View File

@@ -1,2 +1,4 @@
failures failures
testFailures testFailures
| test.cpp:308:5:308:29 | ... = ... | Unexpected result: deref=L308 |
| test.cpp:725:5:725:15 | ... = ... | Unexpected result: deref=L725 |

View File

@@ -305,7 +305,7 @@ void test21() {
for (int i = 0; i < n; i += 2) { for (int i = 0; i < n; i += 2) {
xs[i] = test21_get(i); // GOOD xs[i] = test21_get(i); // GOOD
xs[i+1] = test21_get(i+1); // GOOD xs[i+1] = test21_get(i+1); // GOOD [FALSE POSITIVE]
} }
} }
@@ -714,3 +714,14 @@ void test35(unsigned long size, char* q)
deref(q); deref(q);
} }
} }
void test21_simple(bool b) {
int n = 0;
if (b) n = 2;
int* xs = new int[n];
for (int i = 0; i < n; i += 2) {
xs[i+1] = 0; // GOOD [FALSE POSITIVE]
}
}