ID0001158: **This issue was created automatically from Mantis Issue 1158. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0001158 | Frama-C | Plug-in > jessie | public | 2012-04-16 | 2013-03-27 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | nmuller | **Assigned To** | cmarche | **Resolution** | fixed | | **Priority** | normal | **Severity** | feature | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 | ### 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 ## Attachments - [statement_behavior.c](/uploads/8cf47a660de8c39133748a7ac3e9607e/statement_behavior.c)