Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002334Frama-CPlug-in > jessiepublic2017-12-06 10:052018-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 Filesc file icon jessie-crash.c [^] (875 bytes) 2017-12-06 10:05 [Show Content]

- Relationships

-  Notes
(0006477)
abustany (reporter)
2017-12-06 10:22

It seems that the string.h is the culprit, removing it allows jessie to parse the file correctly.
(0006478)
virgile (developer)
2017-12-06 11:22

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)
2018-01-09 15:19

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)
2018-07-11 15:34
edited on: 2018-07-11 15:41

Fixed in Frama-C Chlorine.


- 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker