--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on November 2013 ---
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 >