As a result around some discussion what it means for a tool to be a framework, I think it might be interesting to add the ability to use k-callstrings in Goblint. The implementation of it should be trivial, but it might be worth comparing:
- Does it help Goblint to be more precise when enabled together with our usual contexts on sv-comp?
- How does it compare to our normal approach to context-sensitive analysis, i.e., partial tabulation, w.r.t. precision and performance?
This might also be the basis for a Bachelor's thesis to do some larger scale measurements on all our different options for contexts.