package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install

Dune Dependency

Authors

Maintainers

Sources

goblint-2.5.0.tbz
sha256=452d8491527aea21f2cbb11defcc14ba0daf9fdb6bdb9fc0af73e56eac57b916
sha512=1993cd45c4c7fe124ca6e157f07d17ec50fab5611b270a434ed1b7fb2910aa85a8e6eaaa77dad770430710aafb2f6d676c774dd33942d921f23e2f9854486551

doc/goblint.lib/Goblint_lib/LoopfreeCallstring/index.html

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.

OCaml

Innovation. Community. Security.