Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000714Frama-CKernel > ACSL implementationpublic2011-02-11 15:582014-02-12 16:59
Reporterpatrick 
Assigned Topatrick 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000714: Lexing of ACSL characters
Descriptionframa-c cannot parse the ACSL expression: '\\' + 'a'

The lexer considers, as a unique token, the expression: '\\' + '
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0001475)
patrick (developer)
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 (developer)
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 (developer)
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 (developer)
2014-02-12 16:59

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2011-02-11 15:58 patrick New Issue
2011-02-11 15:58 patrick Status new => assigned
2011-02-11 15:58 patrick Assigned To => virgile
2011-02-11 16:06 patrick Assigned To virgile => patrick
2011-02-11 16:21 patrick Note Added: 0001475
2011-02-11 16:22 patrick Note Added: 0001476
2011-02-15 12:39 patrick Note Edited: 0001475
2011-02-15 12:47 svn Checkin
2011-02-17 10:57 patrick Note Edited: 0001475
2011-02-17 10:58 patrick Note Edited: 0001475
2011-02-17 11:05 patrick Note Added: 0001507
2011-02-17 12:33 svn Checkin
2011-02-17 12:51 svn Checkin
2011-02-17 12:51 svn Status assigned => resolved
2011-02-17 12:51 svn Resolution open => fixed
2011-02-17 13:00 svn Checkin
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2014-02-12 16:59 patrick Note Added: 0004833
2014-02-12 16:59 patrick Status closed => resolved


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker