Nathan Chong

Reading uninitialized memory gives symbolic value rather than error

4

In the following program we read from uninitialized memory so the program is undefined [0]. Using CBMC as our symbolic engine means Kani does not warn of this error. Instead...

1. In `thread.h` the doc for `aws_thread_clean_up` currently reads: ``` /** * Cleans up the thread handle. Either detach or join must be called * before calling this function. */...

Consider adding a thread-local storage system in common that everything else hangs off of so that the CRT's usage is always a single slot. Current use of thread-local storage: -...

Requested feature: Allow quantifiers in Kani asserts and assumes Use case: CBMC supports bounded quantification under constant lower and upper bounds [0]. It would be great to have this in...