--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on April 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] question about treatment of assigns clauses in WP (Neon)



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