Module Goblint_lib.LoopfreeCallstring

Loopfree Callstring analysis loopfree_callstring that reduces the call string length of the classical Call String approach for recursions The idea is to improve the Call String analysis by representing all detected call cycle of the call string in a set In case no call cycles appears, the call string is identical to the call string of the Call String approach For example:

• call string main, a, b, c, a is represented as main, {a, b, c}
• call string main, a, a, b, b, b is represented as main, {a}, {b}

This approach is inspired by

• see https://arxiv.org/abs/2301.06439

  Schwarz, M., Saan, S., Seidl, H., Erhard, J., Vojdani, V. Clustered Relational Thread-Modular Abstract Interpretation with Local Traces. Appendix F.