--- layout: fc_discuss_archives title: Message 5 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



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