@@ -294,6 +294,26 @@ class FatPointer extends TFatPointer {
294294 }
295295}
296296
297+ /**
298+ * A table with headers (start pointer, end pointer, source offset, sink offset, length).
299+ * Consider the following code:
300+ * ``` C++
301+ * int buf[10];
302+ * int *p = buf;
303+ * int *p2 = p - 5;
304+ * int *p3 = p2 + 16;
305+ * ```
306+ * Then, this table is roughly populated with:
307+ * |-------------+----------------+------------+-------------+----------------+------------------|
308+ * | flow start | flow end | src offset | sink offset | length(exists) | valid? |
309+ * |-------------+----------------+------------+-------------+----------------+------------------|
310+ * | int buf[10] | p (∵ p - 5) | 0 | -5 | 10 | No, 0-5 < 10 |
311+ * | p | p2 (∵ p2 + 12) | -5 | 12 | 10 | Yes, -5+12 < 10 |
312+ * |-------------+----------------+------------+-------------+----------------+------------------|
313+ *
314+ * And then we can answer the question of whether the pointer is valid (last column `valid?`).
315+ * NOTE: Consult the configuration `TrackArrayConfig` for the actual definition of `src` and `sink`.
316+ */
297317predicate srcSinkLengthMap (
298318 FatPointer start , FatPointer end , int srcOffset , int sinkOffset , int length
299319) {
@@ -347,7 +367,7 @@ where
347367 srcOffset + sinkOffset > length // Overflow detection
348368 ) and
349369 message =
350- "start: " + start + ", end: " + end + "srcOffset: " + srcOffset + ", sinkOffset: " + sinkOffset +
351- ", length: " + length
370+ "start: " + start + ", end: " + end + "srcOffset: " + srcOffset + ", sinkOffset: " +
371+ sinkOffset + ", length: " + length
352372 )
353373select sink , src , sink , message
0 commit comments