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