--- layout: fc_discuss_archives title: Message 52 from Frama-C-discuss on March 2009 ---
[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



Hello,

On Thu, Mar 19, 2009 at 13:18, Virgile Prevosto <virgile.prevosto at cea.fr> wrote:
>> By the way, I have seen that some "global" knowledge is also kept
>> (assertions about global variables? function pre-condition?). Is this
>> correct? Is this described somewhere?
>
> 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(char_P___string_c_evote_log_2_alloc_table,
     char_P_char_M___string_c_evote_log_2) and
     valid___string_c_evote_log_0(char_P___string_c_evote_log_2_alloc_table) and
     valid___string_v(char_P___string_v_3_alloc_table,
     char_P_char_M___string_v_3) and
     valid___string_v_0(char_P___string_v_3_alloc_table) and
     valid___string_end_of_vote(char_P___string_end_of_vote_4_alloc_table,
     char_P_char_M___string_end_of_vote_4) and
     valid___string_end_of_vote_0(char_P___string_end_of_vote_4_alloc_table) and
     valid___string_y(char_P___string_y_5_alloc_table,
     char_P_char_M___string_y_5) and
     valid___string_y_0(char_P___string_y_5_alloc_table) and
     valid___string_None_of_those_candidates(char_P___string_None_of_those_candidates_6_alloc_table,
     char_P_char_M___string_None_of_those_candidates_6) and
     valid___string_None_of_those_candidates_0
"""


>> I have a side question: I usually write \forall assertions with an
>> int: "\forall int i; [...]". You write your assertion with "integer",
>> "\forall integer i; [...]". Is there any difference? Any reason to
>> prefer one over the other?
>
> Technically, there are only integers in the logic, int is only a
> shortcut to say 'I have an integer and it is between MIN_INT and
> MAX_INT'. It exists mainly to be able to lift C lval in the logic, but
> purely ACSL values should use the primitive type directly.

Ok, I'll fix my code.

Many thanks for the explanations, it helps a lot!

Yours,
david