View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0002322 | Frama-C | Kernel | public | 2017-07-31 13:14 | 2017-12-06 09:11 | ||||
Reporter | Jochen | ||||||||
Assigned To | virgile | ||||||||
Priority | normal | Severity | crash | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Platform | Phosphorus-20170501-beta1 | OS | xubuntu | OS Version | |||||
Product Version | Frama-C 15-Phosphorus | ||||||||
Target Version | Fixed in Version | Frama-C 16-Sulfur | |||||||
Summary | 0002322: repeated predicate definitions in separate file cause crash | ||||||||
Description | Running 'frama-c -wp part.c whole.c' on the attached files causes the follwoing crash: [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing part.c (with preprocessing) [kernel] Parsing whole.c (with preprocessing) [wp] warning: Missing RTE guards [kernel] Current source was: whole.c:12 The full backtrace is: Raised at file "map.ml", line 117, characters 16-25 Called from file "list.ml", line 55, characters 20-23 Called from file "src/plugins/wp/LogicCompiler.ml", line 772, characters 17-61 Called from file "src/plugins/wp/Warning.ml", line 139, characters 6-10 Called from file "src/plugins/wp/LogicSemantics.ml", line 853, characters 12-42 Called from file "src/plugins/wp/Context.ml", line 31, characters 12-17 Re-raised at file "src/plugins/wp/Context.ml", line 34, characters 41-46 Called from file "src/plugins/wp/Warning.ml", line 155, characters 14-18 Called from file "src/plugins/wp/cfgWP.ml", line 461, characters 23-135 Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48 Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48 Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48 Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48 Called from file "list.ml", line 84, characters 24-34 Called from file "src/plugins/wp/calculus.ml", line 339, characters 22-62 Called from file "src/plugins/wp/calculus.ml", line 343, characters 23-45 Called from file "src/plugins/wp/calculus.ml", line 647, characters 20-43 Called from file "src/plugins/wp/calculus.ml", line 606, characters 19-40 Called from file "src/plugins/wp/calculus.ml", line 757, characters 40-59 Called from file "set.ml", line 305, characters 38-41 Called from file "map.ml", line 168, characters 20-25 Called from file "map.ml", line 168, characters 10-18 Called from file "src/plugins/wp/calculus.ml", line 757, characters 4-64 Called from file "src/plugins/wp/calculus.ml", line 793, characters 19-51 Called from file "src/plugins/wp/cfgWP.ml", line 1468, characters 43-66 Called from file "src/plugins/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/plugins/wp/Context.ml", line 69, characters 43-48 Called from file "src/plugins/wp/cfgWP.ml", line 1456, characters 14-957 Called from file "src/plugins/wp/Model.ml", line 120, characters 17-20 Re-raised at file "src/plugins/wp/Model.ml", line 125, characters 25-28 Called from file "src/plugins/wp/Model.ml", line 126, characters 19-36 Called from file "src/plugins/wp/register.ml", line 654, characters 15-40 Called from file "src/libraries/stdlib/extlib.ml", line 299, characters 14-17 Re-raised at file "src/libraries/stdlib/extlib.ml", line 299, characters 47-48 Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12 Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12 Called from file "queue.ml", line 134, characters 6-20 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 (Not_found). Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Phosphorus-20170501-beta1. The problem disappears if: * the source file order is exchanged on the command line, * the overloaded predicate 'Bnd(integer n)' in while.c:5 is renamed e.g. to 'Bnd2', * the trivial 'ensures' clause is removed in whole.c:10, or * the 'requires' clause in whole.c:9 is changed to 'Bnd(1,(int)0)', i.e. 'Bnd' is inlined. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
||||||
|
![]() |
|
Jochen (reporter) 2017-07-31 13:18 |
Note that the contents of 'part.c' is a proper prefix of that of 'whole.c' (except for the closing '*/'). The crash problem also disappears when a definition disagrees between both files. |
jens (reporter) 2017-08-01 16:33 |
I looked at another example and it really looks like Frama-C has a problem with overloaded predicates when multiple files are processed. |
jens (reporter) 2017-08-02 09:55 |
This might be related to https://bts.frama-c.com/view.php?id=2151 |
virgile (developer) 2017-08-25 10:43 |
Fixed in MR 1457 (now merged) |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2017-07-31 13:14 | Jochen | New Issue | |
2017-07-31 13:14 | Jochen | File Added: part.c | |
2017-07-31 13:14 | Jochen | File Added: whole.c | |
2017-07-31 13:18 | Jochen | Note Added: 0006430 | |
2017-08-01 16:33 | jens | Note Added: 0006431 | |
2017-08-02 09:55 | jens | Note Added: 0006432 | |
2017-08-25 10:43 | virgile | Note Added: 0006448 | |
2017-08-25 10:43 | virgile | Status | new => resolved |
2017-08-25 10:43 | virgile | Fixed in Version | => Frama-C GIT, precise the release id |
2017-08-25 10:43 | virgile | Resolution | open => fixed |
2017-08-25 10:43 | virgile | Assigned To | => virgile |
2017-12-06 09:09 | signoles | Fixed in Version | Frama-C GIT, precise the release id => Frama-C 16-Sulfur |
2017-12-06 09:10 | signoles | Status | resolved => closed |
2017-12-06 09:11 | signoles | Relationship added | has duplicate 0002151 |