Frama-C Bug Tracking System - Frama-C
View Issue Details
0000541Frama-CKernel > ACSL implementationpublic2010-07-13 15:472014-02-12 16:55
pascal 
virgile 
normalminoralways
closedfixed 
Frama-C Boron-20100401 
Frama-C Carbon-20101201-beta1 
0000541: When using -pp-annot and including stdbool.h, can't parse \false in annotations
On the attached program (that came from bug report 530), when the -pp-annot option is used, the \false in annotations cause problems. Commandline (for me, adjust path as needed): frama-c -pp-annot -cpp-command "gcc -I/usr/local/Frama-C_B/share/frama-c/libc -C -E " t3.c Results: [kernel] preprocessing with "gcc -I/usr/local/share/frama-c/libc -C -E -dD t3.c" /usr/local/share/frama-c/libc/stdlib.h:127:[kernel] user error: lexical error, illegal character \ [kernel] user error: skipping file "t3.c" that has errors. [kernel] Frama-C aborted because of an invalid user input. More details are available at bug 530.
No tags attached.
related to 0000530closed cmarche crash 
c t3.c (4,463) 2010-07-13 15:47
https://bts.frama-c.com/file_download.php?file_id=109&type=bug
Issue History
2010-07-13 15:47pascalNew Issue
2010-07-13 15:47pascalStatusnew => assigned
2010-07-13 15:47pascalAssigned To => virgile
2010-07-13 15:47pascalFile Added: t3.c
2010-07-16 13:26pascalSummaryWhen using -jessie, can't parse \ in annotations => When using -pp-annot, can't parse \ in annotations
2010-07-16 13:26pascalDescription Updated
2010-07-16 13:46pascalSummaryWhen using -pp-annot, can't parse \ in annotations => When using -pp-annot and including stdbool.h, can't parse \false in annotations
2010-07-16 15:10monateNote Added: 0001008
2010-07-30 16:34virgileNote Added: 0001023
2010-07-30 16:34virgileStatusassigned => acknowledged
2010-07-30 16:34virgileRelationship addedrelated to 0000530
2010-07-30 16:45virgileNote Added: 0001024
2010-07-30 16:56pascalNote Added: 0001025
2010-07-30 17:17virgileNote Added: 0001026
2010-07-30 17:21pascalNote Added: 0001027
2010-07-30 17:31virgileNote Added: 0001028
2010-08-16 14:39svnCheckin
2010-08-16 14:39svnStatusacknowledged => resolved
2010-08-16 14:39svnResolutionopen => fixed
2010-12-10 15:45signolesFixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:36signolesStatusresolved => closed

Notes
(0001008)
monate   
2010-07-16 15:10   
The problem comes from the tokenization rules of the preprocessor: \ident is tokenized as \ ident and therefore macro expansion may occur on ident. In the above case we have : === #define false 0 //@ terminates \false ; === It is preprocessed as: terminates \0 This will also break for all \ prefixed identifiers in logic.
(0001023)
virgile   
2010-07-30 16:34   
Logic pre-pre-processor might do something about it.
(0001024)
virgile   
2010-07-30 16:45   
BTW, I'm making a test case from comment 1008. t3.c does not contain any annotation, much less a \false somewhere.
(0001025)
pascal   
2010-07-30 16:56   
I strongly disagree on the t3.c comment. I think it would be very useful to have a test based on t3.c, containing #include #include #include #include because this happens quite a bit more often than whatever specialized test case you are writing. We could even #include and use any of the macros defined there. That would again be representative of what typical programs do.
(0001026)
virgile   
2010-07-30 17:17   
There seems to be a misunderstanding. I'm perfectly happy with including stdbool. My remark was that t3.c alone is useless for detecting the bug as long as it does not contain any annotation. The #include in themselves cause no harm.
(0001027)
pascal   
2010-07-30 17:21   
Yes they do, try the commandline: frama-c -pp-annot -cpp-command "gcc -I/usr/local/Frama-C_B/share/frama-c/libc -C -E " t3.c Adjust path as needed.
(0001028)
virgile   
2010-07-30 17:31   
OK, I see it now, I didn't think about annotations in included files, sorry. Nevertheless, the main interest of t3.c are the #include, the code itself is just a distraction (from bug 541 point of view).