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] Unability to verify an arithmetic assertion disapears in a reduced but similar test case

Le jeu 19 mar 2009 13:51:56 CET,
David MENTRE <dmentre at linux-france.org> a ?crit :

> > I'm unsure what you mean by "global knowledge". assertion on variables
> > (and regions) that are not modified by the loop will still hold, but
> > that's all.
> 
> I'm using static strings in my code and I have assumptions like this
> in the upper-right corner of Jessie GUI:
> """
> H1: true = true and
>     (valid___string_w(char_P___string_w_1_alloc_table,
>      char_P_char_M___string_w_1) and
>      valid___string_w_0(char_P___string_w_1_alloc_table) and
>      valid___string_c_evote_log

OK, this is what I thought: these hypotheses refer to the
initial state of the function. If you don't modify your strings (and
Jessie is able to notice that), they may still be useful. Otherwise,
you might notice that the first argument of valid__string_w (which
intuitively correspond to the memory) is not the same as what you
have in the goal, so that the hypothesis alone can't tell anything
about the current state. You need additional properties that reflect the
various affectations that are made during the execution of the
function, and, in the case of loops, this means loop invariants.

Best regards,
-- 
E tutto per oggi, a la prossima volta.
Virgile