Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002341Frama-CPlug-in > frompublic2018-01-11 12:232018-01-11 21:54
Assigned Toyakobowski 
StatusclosedResolutionno change required 
PlatformLinuxOSUbuntuOS Version 16.04.3 LTS (GN
Product VersionFrama-C 14 Silicon 
Target VersionFixed in Version 
Summary0002341: Incorrect dependency assignment using arraay inside for loop
DescriptionIn 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 ReproduceCall the -deps Option in frama-c from command line using the attached file.
TagsNo tags attached.
Attached Filesc file icon arrayInLoop.c [^] (477 bytes) 2018-01-11 12:23 [Show Content]

- Relationships

-  Notes
jaimeabe (reporter)
2018-01-11 17:32

Using Option -ulevel 100 this "error" is solved and the dependencies correctly resolved. So there was no error.
yakobowski (manager)
2018-01-11 21:54

The dependency analysis computes only an over-approximation, so the result is actually correct (and is the one intended). Loops are indeed a source of imprecisions. Option -ulevel, which we do not advise in general, is indeed a solution. In the future, option -slevel should be suficient to get the same precision, but this is not the case yet.

- Issue History
Date Modified Username Field Change
2018-01-11 12:23 jaimeabe New Issue
2018-01-11 12:23 jaimeabe Status new => assigned
2018-01-11 12:23 jaimeabe Assigned To => yakobowski
2018-01-11 12:23 jaimeabe File Added: arrayInLoop.c
2018-01-11 17:32 jaimeabe Note Added: 0006505
2018-01-11 21:54 yakobowski Note Added: 0006506
2018-01-11 21:54 yakobowski Status assigned => closed
2018-01-11 21:54 yakobowski Resolution open => no change required

Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker