--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on September 2010 ---
Using header files worked for the simple example, thanks for that hint. I then tried in various ways to introduce global variables. However, none of them was successful. I always had either some files inclued twice, or missing. I have a file globals.h with some global variables and typedefs, and also some global invariants, predicates in ACSL. Furthermore I have file1.c and file2.c, both #include "globals.h" globals.h: int global1; typedef struct _struct {int x; int y} my_struct; /*@ global invariant ... */ file1.c: #include "globals.h" inline void func1() { // use some global variables and invariants func2(); } file1.h: /*@ requires ..., ensures ... for func1 */ inline void func1(); file2.c #include "globals.h" inline void func2() { // use some global variables and invariants } file2.h: /*@ requires ..., ensures ... for func2, also using global invariants*/ inline void func2(); frama-c -jessie -jessie-atp file1.c results in VCs for func1, but with the warning "No code for function func2, default assigns generated" If I additionally "#include file2.c" in file1, I get error messages because globals.h is included twice, and therefore global variables are redefined. If i "#include file2.h" in file1, I have the problem that in file2.h the global invariants are not known, although compiling file2.c (not file2.h) would work. How can I bypass this dilemma? Sincerely, 2010/9/13 Pascal Cuoq <pascal.cuoq at gmail.com> > Hello, > > On Sat, Sep 11, 2010 at 10:12 PM, Michael Schausten > <michaelschausten at googlemail.com> wrote: > > > I then tried to put the functions into separate c-files, including them > in a > > main file, e.g.: > > > > /*@ ensures ... */ > > file1.c: > > void func1() { /*...*/ } > > > > /*@ ensures ...*/ > > file2.c: > > void func2() { /*...*/ } > > I have no experience with the Coq back-end, but after a few hours of > thought (you might say I'm a slow thinker), I think that's irrelevant. > Jessie offers a modular verification methodology, and that should be > true regardless of the back-end. > > So, what happens if you... > > 1/ provide headers file1.h, ... with only the contract of the function > func1(), ... (the contract is the part of the ACSL annotations that > tells the rest of the program how to use it. requires, ensures, > assigns, this sort of things), > > 2/ include these headers in main.c, and use only the contracts of > func1(), ... to verify main(), > > 3/ use the separate commands: > > frama-c -jessie -jessie-atp coq file1.c > frama-c -jessie -jessie-atp coq file2.c > frama-c -jessie -jessie-atp coq main.c > > for the verification? > > I believe this is the intended usage for modular verification, > regardless of the back-end. > > Pascal > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100914/cb7b3958/attachment.htm>