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