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 - 2019 MantisBT Team
Powered by Mantis Bugtracker