Record statement copies during loop unrolling

goblint / analyzer

Static analysis framework for C

https://goblint.in.tum.de

MIT License

160 stars 72 forks source link

Record statement copies during loop unrolling #1403

Closed sim642 closed 3 months ago

sim642 commented 3 months ago

This resurrects my old attempt at identifying syntactically unrolled loop iterations for #1372. The key yet subtle part to making it work was to only use skind and labels for stmt hashes for the hashtable.

This also adds a CFG cram test where statement copies are indicated by dotted edges.

TODO

[x] Test nested loops.

michael-schwarz commented 3 months ago

There seems to be some issues with the OS X cram tests:

cfgDot: command not found
graph-easy: command not found
goblint --set lib.activated '[]' --set exp.unrolling-factor 5 --enable ana.int.interval --enable witness.yaml.enabled 11-unrolled-loop-invariant.c seems to have radically different output than what was expected