Input computations imprecise when calling unknown function

ID0000644: This issue was created automatically from Mantis Issue 644. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000644	Frama-C	Plug-in > inout	public	2010-12-20	2010-12-20

Reporter	vmoyalam	Assigned To	pascal	Resolution	no change required
Priority	normal	Severity	feature	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Carbon-20101201-beta1	Target Version	-	Fixed in Version	Frama-C Carbon-20101201-beta1

Description :

If a local variable is modified two times consecutively:

1. local = CONSTANT1; local = CONSTANT2;

   CONSTANT1 and CONSTANT2 are both considered as in operands (-inout and-input options), but if the variable is modified in another way :

2. //@assigns i; extern void f(/ out */ int * const i) ;

   local = CONSTANT1; local = CONSTANT2; f(&local);

   CONSTANT1 and CONSTANT2 are no longer present in the Inout analysis.

Additional Information :

See the complete example in the attached file.

Attachments

• test_II.c