Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000913Frama-CPlug-in > Evapublic2011-08-05 14:142011-10-10 14:14
Reporteryakobowski 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000913: Improve Db.Properties.Interp.loc_to_loc
DescriptionA precise assigns clause for function memcpy is
/*@ assigns ((char*)dst)[0..n] \from ((char*)src)[0..n];
    assigns \result \from dst; */
void* Frama_C_memcpy(void* dst, const void* src, unsigned n);

This is currently not treated by the aforementioned Db function, probably because of the casts to char*. By using char* directly everywhere, the assigns clause is (imprecisely) translated to something equivalent to /*@ assigns dst[..] \from src[..];

Since the comment on the function is to complain if some unsupported cases are required, I'm complaining :-)
TagsNo tags attached.
Attached Files

- Relationships
related to 0000912closedyakobowski Functional dependencies are incorrect in presence of value analysis builtins 

-  Notes
(0002120)
yakobowski (manager)
2011-08-05 14:16

Related to bug 912: assigns clause can be used to mitigate the absence of support for dependencies in value analysis builtins.
(0002131)
yakobowski (manager)
2011-08-10 17:48

I've added the support for one level of casts in rev 14585. I reassign the bug to myself, since the need for this function will hopefully disappear once the translation from terms to locations_bytes/locations is completed.
(0002220)
yakobowski (manager)
2011-09-08 00:26

This should be much better, starting from revision 15040. If someone finds another non-treated construct, this bug can be reopened.

- Issue History
Date Modified Username Field Change
2011-08-05 14:14 yakobowski New Issue
2011-08-05 14:14 yakobowski Status new => assigned
2011-08-05 14:14 yakobowski Assigned To => pascal
2011-08-05 14:15 yakobowski Relationship added related to 0000912
2011-08-05 14:16 yakobowski Note Added: 0002120
2011-08-10 17:48 yakobowski Note Added: 0002131
2011-08-10 17:48 yakobowski Assigned To pascal => yakobowski
2011-09-08 00:26 yakobowski Note Added: 0002220
2011-09-08 00:26 yakobowski Status assigned => resolved
2011-09-08 00:26 yakobowski Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 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