Frama-C Bug Tracking System - Frama-C
View Issue Details
0000714Frama-CKernel > ACSL implementationpublic2011-02-11 15:582014-02-12 16:59
patrick 
patrick 
normalminorhave not tried
closedfixed 
 
Frama-C Nitrogen-20111001 
0000714: Lexing of ACSL characters
frama-c cannot parse the ACSL expression: '\\' + 'a' The lexer considers, as a unique token, the expression: '\\' + '
No tags attached.
Issue History
2011-02-11 15:58patrickNew Issue
2011-02-11 15:58patrickStatusnew => assigned
2011-02-11 15:58patrickAssigned To => virgile
2011-02-11 16:06patrickAssigned Tovirgile => patrick
2011-02-11 16:21patrickNote Added: 0001475
2011-02-11 16:22patrickNote Added: 0001476
2011-02-15 12:39patrickNote Edited: 0001475
2011-02-15 12:47svnCheckin
2011-02-17 10:57patrickNote Edited: 0001475
2011-02-17 10:58patrickNote Edited: 0001475
2011-02-17 11:05patrickNote Added: 0001507
2011-02-17 12:33svnCheckin
2011-02-17 12:51svnCheckin
2011-02-17 12:51svnStatusassigned => resolved
2011-02-17 12:51svnResolutionopen => fixed
2011-02-17 13:00svnCheckin
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2014-02-12 16:59patrickNote Added: 0004833
2014-02-12 16:59patrickStatusclosed => resolved

Notes
(0001475)
patrick   
2011-02-11 16:21   
(edited on: 2011-02-17 10:58)
I started to correct the problem. The actual tests are ok The new following test is ok. //@ behavior esc: assumes c!= '\'' && c!='a'; void f(char c) { } But a problem is still there with the following expression when using -pp-annot option: //@behavior other: assumes c!='\\' && c!='a'; void f(char c) { } Note: I modified the lexing rule as follow: | ('L'? "'" as prelude) (([^ '\\' '\'' '\n']|("\\"[^ '\n']))+ as content) "'"
(0001476)
patrick   
2011-02-11 16:22   
A similar problem is there about strings. The following behavior cannot be parsed: /*@ behavior esc: assumes "" != "\"" && ""=="" ; */ void f(char c) { }
(0001507)
patrick   
2011-02-17 11:05   
Description of the problem with -pp-annot and '\\' character : > cat t.c //@behavior b: assumes c!='\\'; void f(char c) { } > frama-c t.c [kernel] preprocessing with "gcc -C -E -I. t.c" > frama-c -pp-annot t.c [kernel] preprocessing with "gcc -C -E -I. -dD t.c" "t.c":3:[kernel] user error: Can't preprocess annotation: eof while parsing a char literal Annotation will be kept as is t.c:1:[kernel] user error: syntax error [kernel] user error: skipping file "t.c" that has errors. [kernel] error occurring when exiting Frama-C: stopping exit procedure. Frama-C aborted because of invalid user input.
(0004833)
patrick   
2014-02-12 16:59   
Fix committed to stable/neon branch.