Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001158Frama-CPlug-in > jessiepublic2012-04-16 11:422013-03-27 09:44
Reporternmuller 
Assigned Tocmarche 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001158: inlining of assembleur is not supported
Descriptionsuch a sequence triggers the message here below /*@ assigns five_times; ensures five_times == (int)(5 * x); */ asm ("leal (%1,%1,4), %0" : "=r" (five_times) : "r" (x) );
Additional Informationframa-c -jessie -jessie-atp alt-ergo statement_behavior.c [kernel] preprocessing with "gcc -C -E -I. -dD statement_behavior.c" [jessie] Starting Jessie translation statement_behavior.c:13:[jessie] failure: Unexpected failure. Please submit bug report (Ref. "interp.ml:1946:13"). [kernel] The full backtrace is: Raised at file "src/kernel/log.ml", line 507, characters 30-31 Called from file "src/kernel/log.ml", line 501, characters 2-9 Re-raised at file "src/kernel/log.ml", line 504, characters 8-9 Called from file "src/type/type.ml", line 600, characters 39-44 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 36, characters 4-20 Called from file "src/kernel/cmdline.ml", line 713, characters 2-9 Called from file "src/kernel/cmdline.ml", line 195, characters 4-8 Plug-in jessie aborted because of internal error. Please report as 'crash' at http://bts.frama-c.com/ Note that a backtrace alone often does not have information to understand the bug. Guidelines for reporting bugs are at: http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
TagsNo tags attached.
Attached Filesc file icon statement_behavior.c [^] (435 bytes) 2012-04-16 11:42 [Show Content]

- Relationships

-  Notes
(0002900)
nmuller (reporter)
2012-04-16 18:59

Under Nitrogen : frama-c -jessie file.c -> KO frama-c -jessie -jessie-atp file.c -> KO
(0002910)
virgile (developer)
2012-04-17 13:43

Jessie does not support inline assembly.
(0002918)
nmuller (reporter)
2012-04-17 13:50

it seems to work with wp on the gui
(0003494)
cmarche (developer)
2012-10-26 17:05

Jessie now displays a nice error message "not yet implemented ..." BTW, no need to submit a feature request for the support of inline assembly.
(0003776)
signoles (manager)
2013-03-27 09:43

Fixed in Frama-C Oxygen + Why 2.32.

- Issue History
Date Modified Username Field Change
2012-04-16 11:42 nmuller New Issue
2012-04-16 11:42 nmuller Status new => assigned
2012-04-16 11:42 nmuller Assigned To => virgile
2012-04-16 11:42 nmuller File Added: statement_behavior.c
2012-04-16 18:59 nmuller Note Added: 0002900
2012-04-17 13:43 virgile Note Added: 0002910
2012-04-17 13:43 virgile Assigned To virgile => cmarche
2012-04-17 13:43 virgile Severity minor => feature
2012-04-17 13:43 virgile Category Kernel > ACSL implementation => Plug-in > jessie
2012-04-17 13:43 virgile Product Version Frama-C Carbon-20110201 => Frama-C GIT, precise the release id
2012-04-17 13:43 virgile Additional Information Updated
2012-04-17 13:50 nmuller Note Added: 0002918
2012-10-26 17:05 cmarche Note Added: 0003494
2012-10-26 17:05 cmarche Status assigned => resolved
2012-10-26 17:05 cmarche Resolution open => fixed
2013-03-27 09:43 signoles Note Added: 0003776
2013-03-27 09:44 signoles Fixed in Version => Frama-C Oxygen-20120901
2013-03-27 09:44 signoles Status resolved => closed


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker