Frama-C Bug Tracking System - Frama-C
View Issue Details
0002315Frama-CPlug-in > Evapublic2017-07-01 03:422017-07-03 23:39
maxime 
yakobowski 
highblockalways
closedno change required 
Frama-C 15-Phosphorus 
 
0002315: unsoundness after external function call
Hi everyone, Frama-C is unsound after an external function call. See the attached file. Running frama-c -val unsound.c gives me: [value] Called Frama_C_show_each_r({1}) This is wrong. The call to the external function f can update **x, and so *y can be anything. At the call to f(x), I think you should grab all the base addresses that are reachable by the arguments and set them to TOP.
frama-c -val unsound.c
No tags attached.
c unsound.c (273) 2017-07-01 03:42
https://bts.frama-c.com/file_download.php?file_id=1194&type=bug
Issue History
2017-07-01 03:42maximeNew Issue
2017-07-01 03:42maximeStatusnew => assigned
2017-07-01 03:42maximeAssigned To => yakobowski
2017-07-01 03:42maximeFile Added: unsound.c
2017-07-02 11:16yakobowskiNote Added: 0006418
2017-07-02 11:16yakobowskiStatusassigned => feedback
2017-07-03 19:30maximeNote Added: 0006419
2017-07-03 19:30maximeStatusfeedback => assigned
2017-07-03 23:39yakobowskiNote Added: 0006420
2017-07-03 23:39yakobowskiStatusassigned => closed
2017-07-03 23:39yakobowskiResolutionopen => no change required
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0006418)
yakobowski   
2017-07-02 11:16   
The observed behavior is the intended one, and is not (in our opinion) unsound. We sacrifice generality for precision and ease of use. More precisely, we make assumptions on what the functions without a body do, so that the analysis does not degenerate too early. It is up the user to check that those assumptions hold, or to stub the functions without a body appropriately. ## How to see that the analysis is unfinished: First, notice that a warning is emitted to signal that the the analysis of 'f' may be/is probably incorrect: unsound.c:12:[kernel] warning: Neither code nor specification for function f, generating default assigns from the prototype If you inspect the statuses of those 'assigns' clauses afterwards, either in the GUI or with the Report plugin, you will see that they have 'Unknown' status. For the program to be deemed correct, they would need to have 'Valid' or 'Considered Valid' status. ## How to model the call to 'f'? The two possibilities are either to write a C body, or to write assigns/from clauses. In this particular case, a proper clause is //@ assigns **p \from \nothing; void f(int **p); ## Where is this documented? Section 5.2.8 of the manual is the most explicit (but should probably be made even clearer). Functions without body are also mentioned in Section 4.4.3. Detailed explanations on how to write proper assigns/from clauses are given in Section 7.2. I am interested in feedback on what could be improved regarding this topic. > At the call to f(x), I think you should grab all the base addresses that are > reachable by the arguments and set them to TOP. Indeed, this would be sound. But: 1) this would include all global variables, resulting later on in an almost completely imprecise analysis 2) this cannot be expressed in ACSL for the global variables, and only with difficulty for the local ones.
(0006419)
maxime   
2017-07-03 19:30   
Alright, that makes sense. Thank you.
(0006420)
yakobowski   
2017-07-03 23:39   
Feel free to comment further if you have suggestions for the manual.