View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0002235 | Frama-C | Kernel | public | 2016-06-21 22:35 | 2017-05-31 19:05 | ||||
Reporter | jrobbins | ||||||||
Assigned To | virgile | ||||||||
Priority | normal | Severity | crash | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Aluminium | ||||||||
Target Version | Fixed in Version | Frama-C 15-Phosphorus | |||||||
Summary | 0002235: Functions that claim to return a struct but don't cause a crash | ||||||||
Description | If a function returns a struct in its declaration, but it's method body does not return anything, Frama-C will warn about not finding a return value, and then crash. While the kernel does warn you this is an issue, no invalid operation on the user's part should cause a crash. Instead, it should cause a user error. | ||||||||
Steps To Reproduce | == File bug.c: struct s { int i; }; struct s foo() {} == Run command: frama-c bug.c == Output: [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing bug.c (with preprocessing) bug2.c:5:[kernel] warning: Body of function foo falls-through and cannot find an appropriate return value bug2.c:5:[kernel] failure: Found return without value in function foo [kernel] Current source was: bug.c:5 The full backtrace is: Raised at file "src/kernel_services/plugin_entry_points/log.ml", line 583, characters 30-31 Called from file "src/kernel_services/plugin_entry_points/log.ml", line 577, characters 9-16 Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 580, characters 15-16 Called from file "src/kernel_internals/typing/oneret.ml", line 246, characters 8-87 Called from file "src/kernel_internals/typing/oneret.ml", line 354, characters 22-54 Called from file "src/kernel_internals/typing/oneret.ml", line 361, characters 13-35 Called from file "src/kernel_services/ast_queries/file.ml", line 891, characters 6-26 Called from file "list.ml", line 73, characters 12-15 Called from file "src/kernel_services/ast_queries/file.ml", line 1143, characters 5-43 Called from file "src/kernel_services/ast_queries/file.ml", line 1579, characters 2-22 Called from file "src/kernel_services/ast_queries/file.ml", line 1666, characters 4-27 Called from file "src/kernel_services/ast_data/ast.ml", line 111, characters 2-28 Called from file "src/kernel_services/ast_data/ast.ml", line 123, characters 53-71 Called from file "src/kernel_internals/runtime/boot.ml", line 29, characters 6-20 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 787, characters 2-9 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 817, characters 18-64 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8 Frama-C aborted: internal error. Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Aluminium-20160501. 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 | ||||||||
Additional Information | Tested with Aluminum on Linux 64-bit. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
yakobowski (manager) 2016-12-08 10:23 |
Indeed. This is a limitation of Frama-C, that does not allow a function declared as non-void to *not* return something. We will turn the crash into a hard error. |
virgile (developer) 2016-12-12 10:02 |
Fixed by commit b6ab86c71f70542a73b705bb5d60f2492e87663e |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2016-06-21 22:35 | jrobbins | New Issue | |
2016-08-12 09:54 | signoles | Assigned To | => virgile |
2016-08-12 09:54 | signoles | Status | new => assigned |
2016-12-08 10:23 | yakobowski | Note Added: 0006310 | |
2016-12-12 10:02 | virgile | Note Added: 0006312 | |
2016-12-12 10:02 | virgile | Status | assigned => resolved |
2016-12-12 10:02 | virgile | Fixed in Version | => Frama-C GIT, precise the release id |
2016-12-12 10:02 | virgile | Resolution | open => fixed |
2017-05-31 19:04 | signoles | Fixed in Version | Frama-C GIT, precise the release id => |
2017-05-31 19:04 | signoles | Fixed in Version | => Frama-C 15-Phosphorus |
2017-05-31 19:05 | signoles | Status | resolved => closed |