Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001700Frama-CPlug-in > E-ACSLpublic2014-03-14 23:402014-09-15 17:35
Reporterploc 
Assigned Toguillaume-petiot 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in Version 
Summary0001700: A valid pointer to an empty struct generate a failure
DescriptionIn memory_model/e_acsl_mmodel.c, line 328, you had assert(size > 0); However if the struct is empty: struct toto {}; A valid pointer to toto will have size 0 but still be a valid use. You should have assert(size >= 0);
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0005008)
guillaume-petiot (developer)
2014-03-25 14:17

Fix committed to master branch.
(0005466)
signoles (manager)
2014-09-15 17:35

Fixed in E-ACSL 0.4.1.

- Issue History
Date Modified Username Field Change
2014-03-14 23:40 ploc New Issue
2014-03-14 23:40 ploc Status new => assigned
2014-03-14 23:40 ploc Assigned To => signoles
2014-03-15 09:24 signoles Assigned To signoles => guillaume-petiot
2014-03-17 09:20 guillaume-petiot Status assigned => resolved
2014-03-25 13:23 signoles Resolution open => fixed
2014-03-25 14:17 guillaume-petiot Note Added: 0005008
2014-09-15 17:35 signoles Note Added: 0005466
2014-09-15 17:35 signoles Status resolved => closed
2014-09-15 17:35 signoles Product Version => Frama-C Neon-20140301


Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker