--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] preprocessor problems with jessie



I see the same thing: the problem triggered by a trivial ACSL annotation.

This is a little confusing since CPP gives the same output for a 
compilation unit containing a trivial annotation as it does for an empty 
compilation unit.

But perhaps this output helps us understand the problem:

$ cat tiny.c
/*@ ; @*/
$ cpp-4.7 tiny.c
# 1 "tiny.c"
# 1 "<command-line>"
# 1 "tiny.c"
$ cpp tiny.c
# 1 "tiny.c"
# 1 "<command-line>"
# 1 "/usr/include/stdc-predef.h" 1 3 4
# 30 "/usr/include/stdc-predef.h" 3 4
# 1 "/usr/include/x86_64-linux-gnu/bits/predefs.h" 1 3 4
# 31 "/usr/include/stdc-predef.h" 2 3 4
# 1 "<command-line>" 2
# 1 "tiny.c"

John



On Thu, 7 Nov 2013, Guillaume Melquiond wrote:

> On 07/11/2013 14:27, Pascal Cuoq wrote:
>
>> could we see what is an example of output of cpp-4.8 that Frama-C dies
>> on for a simple C file ?
>
> Attached is the output of a file containing the following single line:
>
> /*@ ; */
>
> In case you wonder, putting an actual ACSL declaration instead of the 
> semi-colon does not help.
>
>> John, if you end up being the one doing the exercise, special assignment
>> : what is a minimal C99-compliant C file as per ?gcc -std=c99 -pedantic?
>> that Frama-C dies on the output of cpp-4.8 of, and the output of cpp-4.8
>> on this file?
>
> The file above is not strictly compliant, since it is an empty translation 
> unit. But adding declarations does not help either.
>
> Best regards,
>
> Guillaume
>