SMG consistency checks
This is an 'overview' of points we may want to change regarding any checks on SMGs. See also upstream #712.
General things
-
Use assertions / google's Verify exception instead of SMGInconsistentException
so it is treated as a CPAchecker bug and not swallowed. -
Add message directly to the exception. Fail immediately when an inconsistency is found, instead of waiting for all checks to pass. I can't see the use of it. -
Use assert
in top-level calls so the checks are disabled by-benchmark
option. -
Maybe reconsider where it is enabled by default (currently a HALF
setting is default). Separate option for more frequent/thorough checks asFULL
is too expensive?
SMG-specific things
-
Check against FIT-TR-2012-04 p.8? -
add nesting consistency
-
-
join.SMGJoinSubSMGs#performChecks
is set tofalse
and never changes. Are these checks needed? They are ignored even in tests, e.g.SMGRegionsWithRegionsTest#testAbstractionOfLinkedRegionsWithSubregions()
fails if I turn them on. -
Check for PTE with wrong target specifiers. Note, algorithm 11, line 7 explicitly overrides target specifiers that are wrongly written in Algorithm 7, line 3 for two regions abstracted into a list 2+. -
Should such checks be moved into constructors / add/remove methods? That is, assert that a new edge is consistent with all present edges when we are constructing and adding it, instead of checking this after at some checkpoint.
Edited by Петров Олег Максимович