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] 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
>