Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001416Frama-CPlug-in > value analysispublic2013-05-07 23:582014-07-28 18:34
Reporterpascal 
Assigned Toyakobowski 
PrioritynormalSeveritycrashReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001416: 22446: unknown sizes of types and value initialization
DescriptionCommit 22446 transforms a crash when some types have unknown sizes into a clean exit, but there remains a problem with the test below:


Sending src/value/initial_state.ml
Transmitting file data .
Committed revision 22446.
~/ppc $ cat t.c
struct s;

struct larger {
  struct s t[2];
  int i;
} v;

int main(int c, char **v)
{
  return 0;
}
~/ppc $ bin/toplevel.opt -val t.c
[kernel] warning: cannot load 5 plug-ins (incompatible with Fluorine-20130401+dev).
                  Aorai; Obfuscator; Report; Security_slicing;
                  Wp
[kernel] preprocessing with "gcc -C -E -I. t.c"
[value] Analyzing a complete application starting at main
[value] Computing initial state
t.c:6:[value] warning: during initialization of variable 'v', size of type 'struct s' cannot be
                 computed (abstract type 'struct s')
[value] Initial state computed
[value] Values of globals at initialization
[kernel] Current source was: t.c:6
         The full backtrace is:
         Raised at file "cil/src/cil.ml", line 4250, characters 40-64
         Called from file "cil/src/cil.ml", line 4763, characters 17-35
         Called from file "src/project/state_builder.ml", line 556, characters 17-22
         Called from file "src/misc/bit_utils.ml", line 245, characters 37-66
         Called from file "list.ml", line 86, characters 24-34
         Called from file "src/misc/bit_utils.ml", line 242, characters 37-1023
         Called from file "src/misc/bit_utils.ml", line 432, characters 4-58
         Called from file "src/memory_state/offsetmap.ml", line 1726, characters 14-160
         Called from file "src/memory_state/offsetmap.ml", line 424, characters 10-34
         Called from file "format.ml", line 1166, characters 10-25
         Called from file "format.ml", line 1166, characters 10-25
         Called from file "src/lib/pretty_utils.ml", line 89, characters 2-121
         Called from file "format.ml", line 1166, characters 10-25
         Called from file "src/value/eval_funs.ml", line 317, characters 6-176
         Called from file "src/value/eval_funs.ml", line 567, characters 11-40
         Re-raised at file "src/value/eval_funs.ml", line 583, 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 82, characters 4-24
         Called from file "queue.ml", line 135, 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 (Cil.SizeOfError("abstract type 'struct s'", _)).
         Please report as 'crash' at http://bts.frama-c.com/. [^]
         Your Frama-C version is Fluorine-20130401+dev.
         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 [^]
~/ppc $
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2013-05-07 23:58 pascal New Issue
2013-05-07 23:58 pascal Status new => assigned
2013-05-07 23:58 pascal Assigned To => yakobowski
2013-05-23 18:20 svn Checkin
2013-05-23 18:20 svn Status assigned => resolved
2013-05-23 18:20 svn Resolution open => fixed
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed
2014-07-28 18:31 yakobowski Relationship added related to 0001874


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker