slayer
by Microsoft Research
Is this C program memory safe?
Ask slayer!
/* Free a stack variable. Expected result: POSSIBLY UNSAFE. */ #include "slayer.h" int main() { int x; free(&x); }
home
permalink
More samples
deref_NULL2
free_free
malloc
malloc_free_struct
if_pointer
create
reverse
copy
About SLAyer - Automatic formal verification for programs with heaps.
SLAyer is an automatic, separation-logic-based memory safety checker. It checks that its input C code doesn't deference dangling pointers, do double frees, nor leak memory.
home
tutorials
project map
live
developer
about
© 2012 Microsoft Corporation -
terms of use
-
privacy