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