Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Related Changesets ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001907Frama-CPlug-in > Evapublic2014-08-08 14:172015-03-17 22:18
ReporterAnne 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Sodium 
Summary0001907: Value abort because of Zero-sized location
DescriptionValue usually support structure types holding an array field with an undefined size, but in the attached case, it aborts with:

    user error: Zero-sized location S_buf[0].chunk (type 'int []').
                Probably empty struct.
                Aborting

* Notice that the size of `buf` is defined since it is only a pointer.
* If `buf` is defined instead of just declared `extern`, the problem disappear.
Steps To Reproduce$ frama-c -val struct.c
TagsNo tags attached.
Attached Filesc file icon struct.c [^] (155 bytes) 2014-08-08 14:17 [Show Content]

- Relationships

-  Notes
(0005401)
yakobowski (manager)
2014-08-08 14:25

 Thank. I was probably a bit over-zealous in fixing 1874, and will look into this. No guarantee, as this is a flexible member array, that are more or less unsupported by Value at the moment.
(0005402)
Anne (reporter)
2014-08-08 14:32

 I have many of those in the application I am analyzing, and it is usually working pretty well... except this external variable problem.
(0005403)
yakobowski (manager)
2014-08-08 14:35

 Because this is one is external, it is treated as if -lib-entry was enabled. In this mode, we fail when trying to feel the unknown size array.
(0005405)
yakobowski (manager)
2014-08-10 21:27

 Fix committed to master branch.

- Issue History
Date Modified Username Field Change
2014-08-08 14:17 Anne New Issue
2014-08-08 14:17 Anne Status new => assigned
2014-08-08 14:17 Anne Assigned To => yakobowski
2014-08-08 14:17 Anne File Added: struct.c
2014-08-08 14:22 yakobowski Relationship added related to 0001874
2014-08-08 14:25 yakobowski Note Added: 0005401
2014-08-08 14:32 Anne Note Added: 0005402
2014-08-08 14:35 yakobowski Note Added: 0005403
2014-08-10 21:27 yakobowski Note Added: 0005405
2014-08-10 21:27 yakobowski Status assigned => resolved
2014-08-10 21:27 yakobowski Resolution open => fixed
2015-01-28 18:08 Lau Tag Attached: struct
2015-01-28 18:08 Lau Tag Detached: struct
2015-03-17 22:17 signoles Fixed in Version => Frama-C Sodium
2015-03-17 22:18 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