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] Error on using pp-annot

  • Subject: [Frama-c-discuss] Error on using pp-annot
  • From: frank at dordowsky.de (Frank Dordowsky)
  • Date: Sun, 6 Apr 2014 17:38:01 +0200 (CEST)
  • In-reply-to: <CAOH62JizN7SNKizysEWehbjhVY81sgsfnaO=LxnuPZ8cYc8Htw@mail.gmail.com>
  • References: <alpine.LNX.2.03.1403300940120.3220@strato.de> <CAOH62JhJErP1S-T80t6TTWDj4DB+89aGb3BHSNM3=vAKEJMz-Q@mail.gmail.com> <CAOH62JiriPFVqKf1-ynK_5BurCv8WR0kNDUECH-tG_4gSnvbBA@mail.gmail.com> <alpine.LNX.2.03.1403301438460.3899@dordowsky.de> <CAOH62JiHCiHPUJRidjsvkv_1USR_qsStz1CYgOPak+HM6MCnMw@mail.gmail.com> <alpine.LNX.2.03.1404012134240.617@dordowsky.de> <CAOH62JizN7SNKizysEWehbjhVY81sgsfnaO=LxnuPZ8cYc8Htw@mail.gmail.com>
Yes, you are right, my success mail was premature. I discovered that
-fpreprocessed blocks all preprocessing, not only the pre-includes.

Here is my little example code:
//file: constant.h

#define MAX (10)
/*@
   @  requires 0 <= val;
   @  requires val <= MAX;
   @  ensures \result == 2*\old(val);
   @*/
int double_it(int val);
------
//file: constant.c

#include "constant.h"

int double_it(int val) {
   if ( (val < 0) || (val > MAX))
     {
       val=0;
     }
   return 2*val;
}

------------------

Here is my frama-c command with response:

frama-c -cpp-extra-args="-I /usr/share/frama-c/libc" \
> -cpp-extra-args="-nostdinc" -cpp-extra-args="-ffreestanding" \
> -wp -wp-rte -pp-annot constant.c -print
[kernel] preprocessing with "gcc -C -E -I. -ffreestanding -nostdinc -I /usr/share/frama-c/libc -dD constant.c"
/usr/include/stdc-predef.h:1:[kernel] user error: unexpected token '/'
[kernel] user error: skipping file "constant.c" that has errors.
[kernel] Frama-C aborted: invalid user input.
---

I will give Clang a try. And, by the way, thanks for dealing with the
problem.

Frank

----
/* Copyright (C) 1991-2014 Free Software Foundation, Inc.
    This file is part of the GNU C Library.

    The GNU C Library is free software; you can redistribute it and/or
    modify it under the terms of the GNU Lesser General Public
    License as published by the Free Software Foundation; either
    version 2.1 of the License, or (at your option) any later version.

    The GNU C Library is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
    Lesser General Public License for more details.

    You should have received a copy of the GNU Lesser General Public
    License along with the GNU C Library; if not, see
    <http://www.gnu.org/licenses/>.  */

#ifndef	_STDC_PREDEF_H
#define	_STDC_PREDEF_H	1

/* This header is separate from features.h so that the compiler can
    include it implicitly at the start of every compilation.  It must
    not itself include <features.h> or any other header that includes
    <features.h> because the implicit include comes before any feature
    test macros that may be defined in a source file before it first
    explicitly includes a system header.  GCC knows the name of this
    header in order to preinclude it.  */

/* glibc's intent is to support the IEC 559 math functionality, real
    and complex.  If the GCC (4.9 and later) predefined macros
    specifying compiler intent are available, use them to determine
    whether the overall intent is to support these features; otherwise,
    presume an older compiler has intent to support these features and
    define these macros by default.  */

#ifdef __GCC_IEC_559
# if __GCC_IEC_559 > 0
#  define __STDC_IEC_559__		1
# endif
#else
# define __STDC_IEC_559__		1
#endif

#ifdef __GCC_IEC_559_COMPLEX
# if __GCC_IEC_559_COMPLEX > 0
#  define __STDC_IEC_559_COMPLEX__	1
# endif
#else
# define __STDC_IEC_559_COMPLEX__	1
#endif

/* wchar_t uses ISO/IEC 10646 (2nd ed., published 2011-03-15) /
    Unicode 6.0.  */
#define __STDC_ISO_10646__		201103L

/* We do not support C11 <threads.h>.  */
#define __STDC_NO_THREADS__		1

#endif