Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Separate proof-files for separate C-files
  • From: michaelschausten at googlemail.com (Michael Schausten)
  • Date: Tue, 14 Sep 2010 13:57:27 +0200
  • In-reply-to: <AANLkTi=Hr_q1foSZ_cdLPfL+cL8uMNqd5qVr5geaxm_F@mail.gmail.com>
  • References: <4C8BD4B6.70101@googlemail.com> <AANLkTi=Hr_q1foSZ_cdLPfL+cL8uMNqd5qVr5geaxm_F@mail.gmail.com>
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>