View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0001158 | Frama-C | Plug-in > jessie | public | 2012-04-16 11:42 | 2013-03-27 09:44 | ||||
Reporter | nmuller | ||||||||
Assigned To | cmarche | ||||||||
Priority | normal | Severity | feature | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C GIT, precise the release id | ||||||||
Target Version | Fixed in Version | Frama-C Oxygen-20120901 | |||||||
Summary | 0001158: inlining of assembleur is not supported | ||||||||
Description | such 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 Information | frama-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 | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
nmuller (reporter) 2012-04-16 18:59 |
Under Nitrogen : frama-c -jessie file.c -> KO frama-c -jessie -jessie-atp file.c -> KO |
virgile (developer) 2012-04-17 13:43 |
Jessie does not support inline assembly. |
nmuller (reporter) 2012-04-17 13:50 |
it seems to work with wp on the gui |
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. |
signoles (manager) 2013-03-27 09:43 |
Fixed in Frama-C Oxygen + Why 2.32. |
![]() |
|||
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 |