This PR adds the --check-invalid-derefs flag, which adds an assumption to each memory read/write in the original binary that the address is in a valid location (i.e. above RSP or below the bottom of the stack), and asserts this property at every read/write in the modified binary.
This PR adds the
--check-invalid-derefsflag, which adds an assumption to each memory read/write in the original binary that the address is in a valid location (i.e. above RSP or below the bottom of the stack), and asserts this property at every read/write in the modified binary.