Frama-C Bug Tracking System - Frama-C
View Issue Details
0002334Frama-CPlug-in > jessiepublic2017-12-06 10:052018-07-11 15:41
abustany 
cmarche 
normalcrashalways
closedfixed 
x86_64Linux4.7.9
Frama-C 15-Phosphorus 
Frama-C 17-Chlorine 
0002334: Crash when trying to analyse a file with jessie
When 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
No tags attached.
c jessie-crash.c (875) 2017-12-06 10:05
https://bts.frama-c.com/file_download.php?file_id=1214&type=bug
Issue History
2017-12-06 10:05abustanyNew Issue
2017-12-06 10:05abustanyStatusnew => assigned
2017-12-06 10:05abustanyAssigned To => cmarche
2017-12-06 10:05abustanyFile Added: jessie-crash.c
2017-12-06 10:22abustanyNote Added: 0006477
2017-12-06 11:22virgileNote Added: 0006478
2018-01-09 15:19cmarcheNote Added: 0006504
2018-01-09 15:20cmarcheStatusassigned => resolved
2018-01-09 15:20cmarcheResolutionopen => fixed
2018-07-11 15:33signolesFixed in Version => Frama-C 16-Sulfur
2018-07-11 15:34signolesStatusresolved => closed
2018-07-11 15:34signolesNote Added: 0006581
2018-07-11 15:40signolesFixed in VersionFrama-C 16-Sulfur => Frama-C 17-Chlorine
2018-07-11 15:41signolesNote Edited: 0006581View Revisions

Notes
(0006477)
abustany   
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   
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   
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   
2018-07-11 15:34   
(edited on: 2018-07-11 15:41)
Fixed in Frama-C Chlorine.