Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000541Frama-CKernel > ACSL implementationpublic2010-07-13 15:472014-02-12 16:55
Reporterpascal 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000541: When using -pp-annot and including stdbool.h, can't parse \false in annotations
DescriptionOn 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.
TagsNo tags attached.
Attached Filesc file icon t3.c [^] (4,463 bytes) 2010-07-13 15:47 [Show Content]

- Relationships
related to 0000530closedcmarche crash 

-  Notes
(0001008)
monate (reporter)
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 (developer)
2010-07-30 16:34

Logic pre-pre-processor might do something about it.
(0001024)
virgile (developer)
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 (reporter)
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 <stdbool.h>
#include <stdint.h>
#include <stdlib.h>
#include <string.h>

because this happens quite a bit more often than whatever specialized test case you are writing.

We could even #include <limit.h> and use any of the macros defined there. That would again be representative of what typical programs do.
(0001026)
virgile (developer)
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 (reporter)
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 (developer)
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).

- Issue History
Date Modified Username Field Change
2010-07-13 15:47 pascal New Issue
2010-07-13 15:47 pascal Status new => assigned
2010-07-13 15:47 pascal Assigned To => virgile
2010-07-13 15:47 pascal File Added: t3.c
2010-07-16 13:26 pascal Summary When using -jessie, can't parse \ in annotations => When using -pp-annot, can't parse \ in annotations
2010-07-16 13:26 pascal Description Updated
2010-07-16 13:46 pascal Summary When 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:10 monate Note Added: 0001008
2010-07-30 16:34 virgile Note Added: 0001023
2010-07-30 16:34 virgile Status assigned => acknowledged
2010-07-30 16:34 virgile Relationship added related to 0000530
2010-07-30 16:45 virgile Note Added: 0001024
2010-07-30 16:56 pascal Note Added: 0001025
2010-07-30 17:17 virgile Note Added: 0001026
2010-07-30 17:21 pascal Note Added: 0001027
2010-07-30 17:31 virgile Note Added: 0001028
2010-08-16 14:39 svn Checkin
2010-08-16 14:39 svn Status acknowledged => resolved
2010-08-16 14:39 svn Resolution open => fixed
2010-12-10 15:45 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:36 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker