Skip to content

Commit 0f285cc

Browse files
committed
C++: Fix QLDoc.
1 parent c0828a4 commit 0f285cc

File tree

1 file changed

+8
-5
lines changed

1 file changed

+8
-5
lines changed

cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/InvalidPointerToDereference.qll

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -66,11 +66,14 @@
6666
* module. Since the node we are tracking is not necessarily _equal_ to the pointer-arithmetic instruction, but rather satisfies
6767
* `node.asInstruction() <= pai + deltaDerefSourceAndPai`, we need to account for the delta when checking if a guard is sufficiently
6868
* strong to infer that a future dereference is safe. To do this, we check that the guard guarantees that a node `n` satisfies
69-
* `n < node + k` where `node` is a node we know is equal to the value of the dereference source (i.e., it satisfies
70-
* `node.asInstruction() <= pai + deltaDerefSourceAndPai`) and `k <= deltaDerefSourceAndPai`. Combining this we have
71-
* `n < node + k <= node + deltaDerefSourceAndPai <= pai + 2*deltaDerefSourceAndPai` (TODO: Oops. This math doesn't quite work out.
72-
* I think this is because we need to redefine the `BarrierConfig` to start flow at the pointer-arithmetic instruction instead of
73-
* at the dereference source. When combined with TODO above it's easy to show that this guard ensures that the dereference is safe).
69+
* `n < node + k` where `node` is a node such that `node <= pai`. Thus, we know that any node `n'` such that `n' <= n + delta` where
70+
* `delta + k <= 0` will be safe because:
71+
* ```
72+
* n' <= n + delta
73+
* < node + k + delta
74+
* <= pai + k + delta
75+
* <= pai
76+
* ```
7477
*/
7578

7679
private import cpp

0 commit comments

Comments
 (0)