Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002315Frama-CPlug-in > value analysispublic2017-07-01 03:422017-07-03 23:39
Reportermaxime 
Assigned Toyakobowski 
PriorityhighSeverityblockReproducibilityalways
StatusclosedResolutionno change required 
PlatformOSOS Version
Product VersionFrama-C 15 Phosphorus 
Target VersionFixed in Version 
Summary0002315: unsoundness after external function call
DescriptionHi 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.
Steps To Reproduceframa-c -val unsound.c
TagsNo tags attached.
Attached Filesc file icon unsound.c [^] (273 bytes) 2017-07-01 03:42 [Show Content]

- Relationships

-  Notes
(0006418)
yakobowski (manager)
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 (reporter)
2017-07-03 19:30

Alright, that makes sense. Thank you.
(0006420)
yakobowski (manager)
2017-07-03 23:39

Feel free to comment further if you have suggestions for the manual.

- Issue History
Date Modified Username Field Change
2017-07-01 03:42 maxime New Issue
2017-07-01 03:42 maxime Status new => assigned
2017-07-01 03:42 maxime Assigned To => yakobowski
2017-07-01 03:42 maxime File Added: unsound.c
2017-07-02 11:16 yakobowski Note Added: 0006418
2017-07-02 11:16 yakobowski Status assigned => feedback
2017-07-03 19:30 maxime Note Added: 0006419
2017-07-03 19:30 maxime Status feedback => assigned
2017-07-03 23:39 yakobowski Note Added: 0006420
2017-07-03 23:39 yakobowski Status assigned => closed
2017-07-03 23:39 yakobowski Resolution open => no change required


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker