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

[Frama-c-discuss] [wp] unproved goals for strlen() function



On 9 January 2014 18:11, Xiao-lei Cui <x_cui at hotmail.com> wrote:
> frama-c -wp -wp-prover z3 str_len.c

/*@
    loop assigns \nothing;
     */
    while (*s++ !=((signed char) '\0'))
{
   ;
}

Hi,

The assigns clause is totally wrong here.
s is assigned in the loop, so you should use:
loop assigns s;
Besides, the axiomatic Strlen might also need to be modified. But I am
not very familiar with the ACSL spec language.

HTH,

-david