C++: Remove 'TODO' now that the implementation has been fixed.

This commit is contained in:
Mathias Vorreiter Pedersen
2023-07-24 12:24:46 +02:00
parent 4345369e9b
commit 4a276c37ac

View File

@@ -20,11 +20,9 @@
* here). So this step is about identifying which of those out-of-bounds pointers identified from step 1 that are
* actually being dereferenced. We do this using a regular dataflow configuration (see `InvalidPointerToDerefConfig`).
*
* This dataflow traversal defines the set of sources as any dataflow node that is non-strictly upper-bounded by the
* pointer-arithmetic instruction identified by `AllocationToInvalidPointer.qll`. (TODO: I'm pretty sure this is incorrect,
* and we should define the set of sources as anything that is non-strictly _lower_ bounded by the pointer-arithmetic
* instruction). That is, the set of sources is any dataflow node `source` such that `source.asInstruction <= pai + delta1`
* for some `delta1 >= 0`.
* This dataflow traversal defines the set of sources as any dataflow node that is non-strictly lower-bounded by the
* pointer-arithmetic instruction identified by `AllocationToInvalidPointer.qll`. That is, the set of sources is any
* dataflow node `source` such that `source.asInstruction() >= pai + delta1` for some `delta1 >= 0`.
*
* The set of sinks is defined to be any address operand `addr` that is non-strictly upper-bounded by the sink. That is,
* any dataflow node `n` such that `addr <= sink.asInstruction() + delta2` for some `delta2`. We call the instruction that