Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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