--- layout: fc_discuss_archives title: Message 51 from Frama-C-discuss on March 2009 ---
Hello, Le jeu 19 mar 2009 09:40:47 CET, David MENTRE <dmentre at linux-france.org> a ?crit : > > I realized that more or less by trial and error. Is this written > somewhere in Jessie documentation? I have probably read it but > overlooked it. There are a few words about loop invariants in section 2.1 of the manual, but that could be more precise indeed. > > 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 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. Best regards, -- E tutto per oggi, a la prossima volta. Virgile