--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on August 2013 ---
Hello Pierre-Lo?c, 2013/8/9 Pierre-Lo?c Garoche <Pierre-Loic.Garoche at onera.fr>: > How do global variables interact with contracts? When used in ensures, it seems > that the global variable appear as a typed free variable. No knwoledge at all > about its value, even when it is just a constant. For example, the following > ensures is not proved automatically. > > int x = 0; > > /*@ requires y >= 0; > @ ensures \result > x; > @*/ > int f(int y) { return y +1; } Well, we don't have any information about the value of x when entering function f: it can very well be modified between initialization and call site. Admittedly, if x was declared const int, it could be said to be 0, but since this is can easily be defeated by a cast, we chose not to rely on it in Frama-C. On the other hand, if you explicitly say that f is the main entry point of your program, then we know that in the pre-state x is 0, and the ensures is easily discharged, as you can see with frama-c -wp -main f file.c > > * Additional ghost field in a struct > > The manuel mentions ghost fields: If a structure has ghost fields, the sizeof of > the structure is the same has the structure without ghost fields. Also, > alignment of fields remains unchanged > > However, it doesn't seems accepted by the Fluorine (June release) and it is not > colored in red in the ACSL implementation document. > This is a bug in the implementation notes. Thanks for having reported it. Best regards, -- E tutto per oggi, a la prossima volta Virgile