0002235: Functions that claim to return a struct but don't cause a crash

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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

Platform

OS Version

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

Relationships

Notes
(0006310) 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.

(0006312) virgile (developer) 2016-12-12 10:02	Fixed by commit b6ab86c71f70542a73b705bb5d60f2492e87663e

Issue History
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