Commit Graph

2 Commits

Author SHA1 Message Date
Cornelius Riemenschneider
3596ff7c51 Address review. 2020-05-10 19:34:16 +02:00
Cornelius Riemenschneider
1c9fa4eb1d This library proves that a subset of pointer dereferences in a program are safe, i.e. in-bounds.
It does so by first defining what a pointer dereference is (on the IR
`Instruction` level), and then using the array length analysis and the range
analysis together to prove that some of these pointer dereferences are safe.
2020-05-06 16:36:48 +02:00