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:
-
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 :
-
//@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.