$ tis-interpreter.sh test.c
test.c:3:[kernel] warning: Body of function foo falls-through and cannot find an appropriate return value
test.c:3:[kernel] failure: Found return without value in function foo
[kernel] Current source was: test.c:3
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml", line 586, characters 30-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 580, characters 9-16
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 583, characters 15-16
Called from file "src/kernel_internals/typing/oneret.ml", line 248, characters 8-87
Called from file "src/kernel_internals/typing/oneret.ml", line 356, characters 22-54
Called from file "src/kernel_internals/typing/oneret.ml", line 363, characters 13-35
Called from file "src/kernel_services/ast_queries/file.ml", line 884, characters 6-26
Called from file "list.ml", line 73, characters 12-15
Called from file "src/kernel_services/ast_queries/file.ml", line 1135, characters 5-43
Called from file "src/kernel_services/ast_queries/file.ml", line 1572, characters 2-22
Called from file "src/kernel_services/ast_queries/file.ml", line 1659, characters 4-27
Called from file "src/kernel_services/ast_data/ast.ml", line 113, characters 2-28
Called from file "src/kernel_services/ast_data/ast.ml", line 125, characters 53-71
Called from file "src/kernel_internals/runtime/boot.ml", line 31, characters 6-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 783, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 813, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 224, characters 4-8
Frama-C aborted: internal error.
Please report at https://github.com/TrustInSoft/tis-interpreter/issues
$
$ cat test.c
struct S { int x; };
struct S foo () {}
int main ()
{
return 0;
}
$