Scalar evolutions analysis

[Anton Vasilyev]

Dear CPAchecker Developers,

Is there something like scalar evolutions analysis in CPAchecker for induction variables?

https://gcc.gnu.org/onlinedocs/gccint/Scalar-evolutions.html

If there is no such analysis, please point me which level (CFA or separate CPA) is preferable for implementation.

Best regards,

Anton Vasilyev

[Philipp Wendler]

Hi Anton,

Am 14.08.23 um 17:04 schrieb Anton Vasilyev:

> Is there something like scalar evolutions analysis in CPAchecker for
> induction variables?
> https://gcc.gnu.org/onlinedocs/gccint/Scalar-evolutions.html

Hm, this page seems to be mostly internal details of GCC and I don't
really understand what analysis you are referring to.

If you are talking about replacing loops with closed forms, this is
commonly called loop abstraction in verification.
We don't have that in CPAchecker right now.

If you mean something else, please describe the analysis that you want
to perform.

> If there is no such analysis, please point me which level (CFA or separate
> CPA) is preferable for implementation.

If you want to find out whether a loop can be abstracted, a CPA should
be fine (and one should always use a CPA as long as it can do what one
needs).

If you want to rewrite loops into closed forms in order to make some
other analysis easier, a CFA post-processing would be needed, I guess.

Greetings
Philipp

--
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181