search

goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
164 stars 72 forks source link

Refine function pointers by their type #39

Open vogler opened 8 years ago

vogler commented 8 years ago

Refine the abstract values of function pointers by checking which functions in the C source code are compatible with regards to their type.

Note: Calling an unknown function pointer is currently unsound, as not all functions are abstractly "executed".

In general, we might a first flow-insensitive analysis for providing global-variants per type. These abstractions could then be used to refine top-values in a subsequent analysis.

vogler commented 3 years ago

I think the idea behind the original issue of a 'top analysis' was that there are examples where you get more precise if you widen to a previously narrowed value. Haven't checked, but maybe it's something like the nested loops in https://github.com/goblint/analyzer/pull/217#issuecomment-836958276. I guess a top analysis would be similar to the restarting solver idea, just for any solver: start with top and narrow to get the values in a first phase and then run the analysis using those values for top in a second phase.