2021-01-27 12:31 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002334Frama-CPlug-in > jessiepublic2018-07-11 15:41
Reporterabustany 
Assigned Tocmarche 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
Platformx86_64OSLinuxOS Version4.7.9
Product VersionFrama-C 15-Phosphorus 
Target VersionFixed in VersionFrama-C 17-Chlorine 
Summary0002334: Crash when trying to analyse a file with jessie
DescriptionWhen running "frama-c -jessie jessie-crash.c" on the attached file, I get the following crash:

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing encoding.c (with preprocessing)
[jessie] Starting Jessie translation
[jessie] warning: \separated is not supported by Jessie. This predicate will be ignored
[kernel] Current source was: FRAMAC_SHARE/libc/__fc_string_axiomatic.h:35
         The full backtrace is:
         Raised at file "interp.ml", line 2383, characters 5-24
         Called from file "interp.ml", line 2644, characters 22-41
         Called from file "list.ml", line 70, characters 22-25
         Called from file "interp.ml", line 2731, characters 27-66
         Called from file "register.ml", line 175, characters 16-32
         Called from file "register.ml", line 278, characters 6-12
         Re-raised at file "register.ml", line 251, characters 29-103
         Called from file "queue.ml", line 105, characters 6-15
         Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
         Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
         Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
         Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
         
         Unexpected error (File "interp.ml", line 2383, characters 5-11: Assertion failed).
         Please report as 'crash' at http://bts.frama-c.com/.
         Your Frama-C version is Phosphorus-20170501.
         Note that a version and a backtrace alone often do not contain enough
         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

My packages are at the following version:

frama-c 20170501
why 2.39
why3 0.87.3
ocaml 4.03.0
TagsNo tags attached.
Attached Files
  • c file icon jessie-crash.c (875 bytes) 2017-12-06 10:05 -
    #include <stdbool.h>
    #include <stddef.h>
    #include <stdint.h>
    #include <string.h>
    
    #define OP_TYPE_DATA 0x01
    #define OP_TYPE_PING 0x02
    
    typedef struct {
    	uint8_t op_type;
    	uint8_t payload_size;
    	uint8_t payload[254];
    } message_t;
    
    bool decode_message(const uint8_t *buf, size_t buf_len, message_t *msg) {
      static const size_t MIN_MSG_SIZE = 0x02;
      static const size_t MAX_MSG_SIZE = 0x100;
    
      if (buf_len < MIN_MSG_SIZE || buf_len > MAX_MSG_SIZE)
        return false;
    
      uint8_t op_type = buf[0];
    
      if (op_type != OP_TYPE_DATA && op_type != OP_TYPE_PING)
        return false;
    
      memset(msg, 0, sizeof(message_t));
      msg->op_type = op_type;
    
      if (op_type == OP_TYPE_DATA) {
        uint8_t msg_size = buf[1];
    
        if (msg_size != buf_len)
          return false;
    
        msg->payload_size = msg_size - MIN_MSG_SIZE;
        memcpy(msg->payload, buf+2, msg->payload_size);
      }
    
      return true;
    }
    
    c file icon jessie-crash.c (875 bytes) 2017-12-06 10:05 +

-Relationships
+Relationships

-Notes

~0006477

abustany (reporter)

It seems that the string.h is the culprit, removing it allows jessie to parse the file correctly.

~0006478

virgile (developer)

The assertion in file "interp.ml", line 2383, characters 5-24 requires that there is no attribute attached to an ACSL axiomatic. This assumption is wrong: Frama-C's kernel use attributes to remember that a given global symbol (be it C or ACSL) is declared in Frama-C's standard library (and thus might deserve some special treatment). While it is safe to ignore such an attribute altogether, Jessie should not assume that no attribute will be present ever. Removing the assertion should thus solve the issue.

~0006504

cmarche (developer)

Fixed in master branch

That is, the presence of attributes does not trigger a crash anymore

Yet, it is unlikely that Jessie would support Frama-C' string.h

~0006581

signoles (manager)

Last edited: 2018-07-11 15:41

View 2 revisions

Fixed in Frama-C Chlorine.

+Notes

-Issue History
Date Modified Username Field Change
2017-12-06 10:05 abustany New Issue
2017-12-06 10:05 abustany Status new => assigned
2017-12-06 10:05 abustany Assigned To => cmarche
2017-12-06 10:05 abustany File Added: jessie-crash.c
2017-12-06 10:22 abustany Note Added: 0006477
2017-12-06 11:22 virgile Note Added: 0006478
2018-01-09 15:19 cmarche Note Added: 0006504
2018-01-09 15:20 cmarche Status assigned => resolved
2018-01-09 15:20 cmarche Resolution open => fixed
2018-07-11 15:33 signoles Fixed in Version => Frama-C 16-Sulfur
2018-07-11 15:34 signoles Status resolved => closed
2018-07-11 15:34 signoles Note Added: 0006581
2018-07-11 15:40 signoles Fixed in Version Frama-C 16-Sulfur => Frama-C 17-Chlorine
2018-07-11 15:41 signoles Note Edited: 0006581 View Revisions
+Issue History