Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001477Frama-CPlug-in > Evapublic2013-09-04 14:052014-03-13 15:57
Reporterdjs52 
Assigned Toyakobowski 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001477: Value analysis: bad type conversion plus unassigned fields in a struct leads to crash
DescriptionThe 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:
         http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines [^]

TagsNo tags attached.
Attached Filesc file icon testcase.c [^] (107 bytes) 2013-09-04 14:05 [Show Content]

- Relationships

-  Notes
(0004055)
yakobowski (manager)
2013-09-04 14:29

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
  NOT ACCESSIBLE
[value] Value analysis not started because globals initialization is not computable.
(0004056)
yakobowski (manager)
2013-09-04 14:32

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.

- Issue History
Date Modified Username Field Change
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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker