|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0001477||Frama-C||Plug-in > Eva||public||2013-09-04 14:05||2014-03-13 15:57|
|Product Version||Frama-C Fluorine-20130601|
|Target Version||Fixed in Version||Frama-C Neon-20140301|
|Summary||0001477: Value analysis: bad type conversion plus unassigned fields in a struct leads to crash|
|Description||The attached code crashes value analysis for me (with frama-c -val testcase.c):|
[kernel] preprocessing with "gcc -C -E -I. testcase.c"
[value] Analyzing a complete application starting at main
[value] Computing initial state
testcase.c:3:[kernel] warning: overflow in conversion of - 1.0f (-1.) from floating-point to integer.
assert -1 < -1.0f < 256;
[kernel] Current source was: testcase.c:3
The full backtrace is:
Called from file "src/value/initial_state.ml", line 498, characters 14-70
Called from file "list.ml", line 74, characters 24-34
Called from file "src/value/initial_state.ml", line 461, characters 10-1023
Called from file "src/value/initial_state.ml", line 590, characters 20-70
Called from file "list.ml", line 69, characters 12-15
Called from file "src/value/initial_state.ml", line 565, characters 6-1023
Called from file "src/value/initial_state.ml", line 617, characters 13-23
Called from file "src/project/state_builder.ml", line 394, characters 17-21
Called from file "src/value/eval_funs.ml", line 313, characters 14-39
Called from file "src/value/eval_funs.ml", line 564, characters 11-40
Re-raised at file "src/value/eval_funs.ml", line 580, characters 47-50
Called from file "src/project/state_builder.ml", line 839, characters 9-13
Re-raised at file "src/project/state_builder.ml", line 847, characters 15-18
Called from file "src/value/register.ml", line 46, characters 4-24
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 732, characters 2-9
Called from file "src/kernel/cmdline.ml", line 212, characters 4-8
Unexpected error (File "src/memory_state/lmap.ml", line 289, characters 18-24: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Fluorine-20130601.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
|Tags||No tags attached.|
Thanks for the very concise bug report. As it happens, this bug is already corrected in the development version, and the fix will be part of the Neon release.
Since the conversion of -1f to an unsigned char is always undefined (the float is truncated towards 0, and the resulting integer is checked to fit within 0..225), Value fails at the very beginning of the analysis.
conv.c:3:[kernel] warning: overflow in conversion of - 1.0f (-1.) from floating-point to integer.
assert -1 < -1.0f < 256;
conv.c:3:[value] Evaluation of initializer '(unsigned char)(- 1.0f)' failed
[value] Initial state computed
[value] Values of globals at initialization
[value] Value analysis not started because globals initialization is not computable.
|Notice that the crash had nothing to do with the fact that the second field is unassigned: the standard specifies that b should be initialized to 0, and this is what Value does.|
|2013-09-04 14:05||djs52||New Issue|
|2013-09-04 14:05||djs52||Status||new => assigned|
|2013-09-04 14:05||djs52||Assigned To||=> yakobowski|
|2013-09-04 14:05||djs52||File Added: testcase.c|
|2013-09-04 14:29||yakobowski||Note Added: 0004055|
|2013-09-04 14:29||yakobowski||Status||assigned => resolved|
|2013-09-04 14:29||yakobowski||Resolution||open => fixed|
|2013-09-04 14:32||yakobowski||Note Added: 0004056|
|2014-03-13 15:56||signoles||Fixed in Version||=> Frama-C Neon-20140301|
|2014-03-13 15:57||signoles||Status||resolved => closed|
|2018-01-12 14:26||signoles||Category||Plug-in > value analysis => Plug-in > Eva|