2021-02-27 09:54 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001158Frama-CPlug-in > jessiepublic2013-03-27 09:44
Reporternmuller 
Assigned Tocmarche 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
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 Files
  • c file icon statement_behavior.c (435 bytes) 2012-04-16 11:42 -
    /* run.config
       OPT: -val -inout -journal-disable
    */
    /*@ ensures \result == (int)(5 * x);
    */
    int pfsqopfc(int x) {
    int five_times;
    
    /*@
      assigns five_times;
      ensures five_times == (int)(5 * x);
    */
    asm ("leal (%1,%1,4), %0"
                 : "=r" (five_times)
                 : "r" (x)
                 );
    /*@ assert five_times == (int) (5 * x);*/ // valid
    return five_times;
    }
    
    int main () {
      int x = 1;
      int y = pfsqopfc(x);
      return 0;
    }
    
    c file icon statement_behavior.c (435 bytes) 2012-04-16 11:42 +

-Relationships
+Relationships

-Notes

~0002900

nmuller (reporter)

Under Nitrogen :
frama-c -jessie file.c -> KO
frama-c -jessie -jessie-atp file.c -> KO

~0002910

virgile (developer)

Jessie does not support inline assembly.

~0002918

nmuller (reporter)

it seems to work with wp on the gui

~0003494

cmarche (developer)

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)

Fixed in Frama-C Oxygen + Why 2.32.
+Notes

-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
+Issue History