--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on April 2014 ---
2014-04-22 10:47 GMT+02:00 Pascal Cuoq <pascal.cuoq at gmail.com>: > On Tue, Apr 22, 2014 at 10:30 AM, Virgile Prevosto > <virgile.prevosto at m4x.org> wrote: > /*@ ... > requires endptr == \null || \valid(endptr) ; > assigns *endptr \from nptr[0 ..] ; > ... > */ > double strtod(const char *restrict nptr, char **restrict endptr); > > /*@ ... > requires \valid_string(src) ; > requires \valid(dst + (0 .. max(n, \string_length(src))) ; > assigns dst[0 .. n-1] ; > ... > */ > char * strncpy(char *restrict dst, const char *restrict src, size_t n); > OK, so it seems that my example is not purely theoretical after all. I agree that under these conditions, emitting a warning that won't be triggered by perfectly legitimate specs too often will be tricky at best. Best regards, -- E tutto per oggi, a la prossima volta Virgile