| 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
|
Relationships 
Relationships