2021-03-02 03:15 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000913Frama-CPlug-in > Evapublic2011-10-10 14:14
Reporteryakobowski 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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 
+Relationships

-Notes

~0002120

yakobowski (manager)

Related to bug 912: assigns clause can be used to mitigate the absence of support for dependencies in value analysis builtins.

~0002131

yakobowski (manager)

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)

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

-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
+Issue History