Frama-C Bug Tracking System - Frama-C
View Issue Details
0001573Frama-CKernelpublic2013-11-27 15:552014-03-13 15:57
Frama-C Neon-20140301 
0001573: Syntax error because of pause instruction in inline assebly
Presence of construction like ----------------------------------------- static inline void cpu_pause(void) { __asm__ volatile ("pause":::); } ----------------------------------------- lead to syntax error Adding some "changed" (like <:::"memory");>) improves the situation
GUI output ----------------------------------------- Current source was: :0 The full backtrace is: Raised at file "", line 353, characters 18-27 Called from file "", line 361, characters 22-38 Unexpected error (Parsing.Parse_error). Please report as 'crash' at Your Frama-C version is Fluorine-20130601. Note that a version and a backtrace alone often do not contain enough information to understand the bug. Guidelines for reporting bugs are at: ---------------------------------------------
No tags attached.
Issue History
2013-11-27 15:55valorNew Issue
2013-11-27 16:36yakobowskiNote Added: 0004346
2013-11-27 20:55yakobowskiStatusnew => assigned
2013-11-27 20:55yakobowskiAssigned To => yakobowski
2013-11-28 11:04yakobowskiNote Added: 0004351
2013-11-28 11:04yakobowskiStatusassigned => feedback
2014-01-12 13:39yakobowskiStatusfeedback => closed
2014-01-12 13:39yakobowskiResolutionopen => fixed
2014-01-12 13:39yakobowskiStatusclosed => resolved
2014-03-13 15:56signolesFixed in Version => Frama-C Neon-20140301
2014-03-13 15:57signolesStatusresolved => closed

2013-11-27 16:36   
Thanks for your report; this bug has already been fixed in the development version, and the bugfix will be part of the next release.
2013-11-28 11:04   
On second thought, I do not obtain the same backtrace as you with Fluorine's GUI. Could you confirm that static inline void cpu_pause(void) { __asm__ volatile ("pause":::); } alone in a file is sufficient to get the crash you mention?