Actions
Feature #6486
openGet rid of auxiliary functions if possible
Start date:
12/26/2015
Due date:
% Done:
0%
Estimated time:
Published in build:
Description
In the most of cases advices are used to replace original function calls with calls to model functions (just passed arguments may vary). This doesn't require auxiliary functions indeed since we can easily substitute model function calls directly to places where original functions were called.
This will help in several ways:- The resulting source code will have less size and verifiers will like this more.
- There will be no ugly ldv_.*\d+ functions in error traces.
- We will not have auxiliary files with ldv_.*\d+ functions (there is no such files at the moment but this is a bug) and there will be no reference to them from error traces.
Of course implementation of this feature requires parsing of advice bodies to understand whether we really can get rid of auxiliary functions.
Actions