--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on January 2012 ---
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