diffblue / 2ls

Static Analyzer and Verifier
http://www.cprover.org/2LS
Other
44 stars 24 forks source link

Enable and improve GOTO instrumentation #146

Closed FrNecas closed 3 years ago

FrNecas commented 3 years ago

In order to make the feature fully work, some minor refactoring was necessary.

I've tested the feature manually on the following examples and all of them seem to work as expected:

void main() { Data x1 = {0,}; Data x2 = {&x1,}; Data x3 = {&x2,}; Data *curr = &x3; while (curr) { assert(curr->content == 0); curr = curr->next; } }

FrNecas commented 3 years ago

Thanks for the reviews. Braces fixed and basic test coverage added.

peterschrammel commented 3 years ago

I think you can merge @viktormalik

viktormalik commented 3 years ago

Indeed, thanks. Merged.