View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0000913 | Frama-C | Plug-in > Eva | public | 2011-08-05 14:14 | 2011-10-10 14:14 | ||||
Reporter | yakobowski | ||||||||
Assigned To | yakobowski | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Carbon-20110201 | ||||||||
Target Version | Fixed in Version | Frama-C Nitrogen-20111001 | |||||||
Summary | 0000913: Improve Db.Properties.Interp.loc_to_loc | ||||||||
Description | A 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 :-) | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
||||||
|
![]() |
|
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. |
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. |
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. |
![]() |
|||
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 |