--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on January 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problems with Frama-C libc



On Wed, Jan 18, 2012 at 10:41 AM, Anne Pacalet <anne.pacalet at free.fr> wrote:
> More precisely, it seems that the value analysis detect that
> the call to [printf] is unreachable because [strncpy] doesn't return
> properly. I thought that maybe it was because of [strncpy] precondition, so
> I tried to add:
> //@ assert \valid_range(s,0,len-1) && valid_string(argv[1]);
> just before the call to [strncpy], but it doesn't change anything.

Hi Anne,

This actually works in the development version, with the same
specifications as in Nitrogen. I'm however puzzled as to why this is
so: most of the changes in the handling of assigns clauses occurred
before Nitrogen, and Value will not interpret anything else in the
specification of strncpy. I will try to have a closer look as soon as
possible.

-- 
Boris