On Sunday, 2 November 2014 at 08:39:26 UTC, Ola Fosheim Grøstad
wrote:
There are also some proprietary C compilers for embedded
programming that claim to support bound checks, but I don't
know how far they go or if they require language
extensions/restrictions.
Btw, related to this is the efforts on bounded model checking:
http://llbmc.org/files/papers/VSTTE12.pdf
LLBMC apparently takes LLVM IR as input and checks the program
using a SMT solver. Basically the same type of solver that proof
systems use.
This is of course a more challenging problem than arrays as it
aims to check a lot of things at the cost of putting some limits
on recursion depth etc:
- Arithmetic overflow and underflow
- Logic or arithmetic shift exceeding the bit-width
- Memory access at invalid addresses
- Invalid memory allocation
- Invalid memory de-allocation
- Overlapping memory regions in memcpy
- Memory leaks
- User defined assertions
- Insufficient specified bounds for the checker
- C assert()
