Feature #6486
openGet rid of auxiliary functions if possible
0%
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.
Updated by Evgeny Novikov almost 5 years ago
- Blocked by deleted (Feature #6827: Merge weaving for different entities)
Updated by Evgeny Novikov almost 5 years ago
- Priority changed from High to Urgent
This is very important task since users suffer very much due to any auxiliary functions.
Updated by Evgeny Novikov over 4 years ago
- Priority changed from Urgent to High
Although this is a nice thing to do, it is too hard to implement. So, I suggest to do #9935 instead. That issue will solve almost all related problems expect for there still will be redundant auxiliary functions that just calls the model ones.
Updated by Evgeny Novikov over 4 years ago
- Related to Feature #9935: Get rid of auxilary function duplicates added