2021-03-02 03:15 CET

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

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



yakobowski (manager)

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


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.


yakobowski (manager)

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