| 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 |
| ||||||||
 Relationships |
||||||
|
||||||
 Relationships |
| Notes |
|
|
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. |
| 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 |