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: pascal.cuoq at gmail.com (Pascal Cuoq)
- Date: Tue, 14 Sep 2010 15:04:07 +0300
- In-reply-to: <AANLkTi=OfN8ixwzT4NFxaJPTsbX5igSLx-BMYWTxeygW@mail.gmail.com>
- References: <4C8BD4B6.70101@googlemail.com> <AANLkTi=Hr_q1foSZ_cdLPfL+cL8uMNqd5qVr5geaxm_F@mail.gmail.com> <AANLkTi=OfN8ixwzT4NFxaJPTsbX5igSLx-BMYWTxeygW@mail.gmail.com>
Hello, On Tue, Sep 14, 2010 at 2:57 PM, Michael Schausten <michaelschausten at googlemail.com> wrote: > 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" This is a C question more than a Frama-C question. Here is the standard way it is traditionally solved, from the file stdlib.h on my system: _____ #ifndef _STDLIB_H_ #define _STDLIB_H_ ... definitions ... definitions ... definitions #endif /* _STDLIB_H_ */ _____ The first inclusion defines everything contained in the header file. Later (and often unavoidable, as you found out) inclusions do nothing because the symbol _STDLIB_H_ has already been defined, meaning the definitions are already available. Pascal
- References:
- [Frama-c-discuss] Separate proof-files for separate C-files
- From: michaelschausten at googlemail.com (Michael Schausten)
- [Frama-c-discuss] Separate proof-files for separate C-files
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] Separate proof-files for separate C-files
- From: michaelschausten at googlemail.com (Michael Schausten)
- [Frama-c-discuss] Separate proof-files for separate C-files
- Prev by Date: [Frama-c-discuss] Separate proof-files for separate C-files
- Next by Date: [Frama-c-discuss] problems with plugin-integration
- Previous by thread: [Frama-c-discuss] Separate proof-files for separate C-files
- Next by thread: [Frama-c-discuss] problems with plugin-integration
- Index(es):