Skip to content

Incorrect dependency assignment using arraay inside for loop

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


Id Project Category View Due Date Updated
ID0002341 Frama-C Plug-in > from public 2018-01-11 2018-01-11
Reporter jaimeabe Assigned To yakobowski Resolution no change required
Priority urgent Severity major Reproducibility always
Platform Linux OS Ubuntu OS Version 16.04.3 LTS (GN
Product Version Frama-C 14-Silicon Target Version - Fixed in Version -

Description :

In the attached file, the dependencies Analysis result should be GlobalVector[3] FROM Schalter dependent. However, the reality is that it assigns the dependenciy of Schalter to the whole vector (GlobalVector[0..4]).

Steps To Reproduce :

Call the -deps Option in frama-c from command line using the attached file.

Attachments

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information