speed of value analysis while use the "-lib-entry" and "main" and "-val-use-spec" option for value analysis
ID0001593: This issue was created automatically from Mantis Issue 1593. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001593 | Frama-C | Plug-in > Eva | public | 2014-01-12 | 2014-01-12 |
| Reporter | Yibiao | Assigned To | yakobowski | Resolution | no change required |
| Priority | low | Severity | trivial | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
With "-lib-entry", all global variables in the ast file will be initialized for a initial state in value analysis.
But I think it will largely impact on the speed of value analysis. Especially when I am using the "-val-use-spec" option for all the functions which called by the main function, there will be many global variables might not useful for value analysis. So in fact, I think we can only initialize all the global variables which only used in the main function for improving the speed of value analysis.