--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on September 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Separate proof-files for separate C-files



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>