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