0000913: Improve Db.Properties.Interp.loc_to_loc

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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

Platform

OS Version

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

related to

0000912

closed

yakobowski

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