Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 168
    • Issues 168
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #996

22446: unknown sizes of types and value initialization

ID0001416: This issue was created automatically from Mantis Issue 1416. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0001416 Frama-C Plug-in > Eva public 2013-05-07 2014-07-28
Reporter pascal Assigned To yakobowski Resolution fixed
Priority normal Severity crash Reproducibility have not tried
Platform - OS - OS Version -
Product Version Frama-C GIT, precise the release id Target Version - Fixed in Version Frama-C Neon-20140301

Description :

Commit 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 $

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking