This project is read-only.

verification of strcpy

Sep 4, 2014 at 4:08 AM
Edited Sep 4, 2014 at 4:09 AM
Hi every body
i'm looking for a good way for verifying lib functions like strcpy. i want to check that the space allocated for the first parameter is greater than the length of second parameter.
since i can't write contracts for this functions (because they are library functions) i write this:
  _(writes \array_range(d ,4))
strcpy(d , "string");
i should face an error, but VCC doesn't report any error. i think this is for modular deductive of VCC.
does anyone have idea for this problem??