Incremental analysis contradicts the from scratch analysis

[J2000A]

During the implementation for my bachelor thesis about generating test cases for the incremental analysis I encountered the problem, that the incremental analysis contradicts the from scratch analysis. @stilscher

Reproduction:

• cp tests/regression/15-deadlock/10-account_incorrect.c inital.c
• Replace in inital.c the init_account() function with:

init_account(bank_account *a) {
  return 0:
}

• Create Goblint Checks:
  Alternative Approach without the option --enable trans.goblint-check is described in this comment.
  ./goblint inital.c --enable trans.goblint-check --set trans.activated '["assert"]' && cp transformed.c inital.c
./goblint tests/regression/15-deadlock/10-account_incorrect.c --enable trans.goblint-check --set trans.activated '["assert"]'

• Run incremental analysis:
  ./goblint inital.c --enable incremental.save
./goblint transformed.c --enable incremental.load

Here the incremental analysis report:

[Error][Assert] Assertion "(unsigned long )f == (unsigned long )(& B)" will fail. (transformed.c:1467:5-1467:30)
[Error][Assert] Assertion "(unsigned long )t == (unsigned long )(& A)" will fail. (transformed.c:1468:5-1468:30)
[Error][Assert] Assertion "f->id == 1" will fail. (transformed.c:1469:5-1469:32)
[Error][Assert] Assertion "(unsigned long )f == (unsigned long )(& B)" will fail. (transformed.c:1473:5-1473:30)
[Error][Assert] Assertion "(unsigned long )t == (unsigned long )(& A)" will fail. (transformed.c:1474:5-1474:30)
[Error][Assert] Assertion "f->id == 1" will fail. (transformed.c:1475:5-1475:32)
...
[Success][Assert] Assertion "(unsigned long )f == (unsigned long )(& B)" will succeed (transformed.c:1467:5-1467:30)
[Success][Assert] Assertion "(unsigned long )t == (unsigned long )(& A)" will succeed (transformed.c:1468:5-1468:30)
[Warning][Assert] Assertion "f->id == 1" is unknown. (transformed.c:1469:5-1469:32)
[Success][Assert] Assertion "(unsigned long )f == (unsigned long )(& B)" will succeed (transformed.c:1473:5-1473:30)
[Success][Assert] Assertion "(unsigned long )t == (unsigned long )(& A)" will succeed (transformed.c:1474:5-1474:30)
[Success][Assert] Assertion "f->id == 1" will succeed (transformed.c:1475:5-1475:32)

=> The incremental analysis says that these six checks are successful/unknown and fail at the same time.

The from scratch analysis on the same file (./goblint transformed.c) just reports success:

[Success][Assert] Assertion "(unsigned long )f == (unsigned long )(& B)" will succeed (transformed.c:1467:5-1467:30)
[Success][Assert] Assertion "(unsigned long )t == (unsigned long )(& A)" will succeed (transformed.c:1468:5-1468:30)
[Success][Assert] Assertion "f->id == 1" will succeed (transformed.c:1469:5-1469:32)
[Success][Assert] Assertion "(unsigned long )f == (unsigned long )(& B)" will succeed (transformed.c:1473:5-1473:30)
[Success][Assert] Assertion "(unsigned long )t == (unsigned long )(& A)" will succeed (transformed.c:1474:5-1474:30)
[Success][Assert] Assertion "f->id == 1" will succeed (transformed.c:1475:5-1475:32)

The same can be reproduced with 15-deadlock/09-account_correct.c as input.

[J2000A]

Alternative way to generate Goblint Checks without the new option --enable trans.goblint-check intruduced in my pull request.

• Create Goblint Checks:
  ./goblint inital.c --set trans.activated '["assert"]' && sed -i 's/__VERIFIER_assert/__goblint_check/g' transformed.c && cp transformed.c inital.c
./goblint tests/regression/15-deadlock/10-account_incorrect.c --set trans.activated '["assert"]' && sed -i 's/__VERIFIER_assert/__goblint_check/g' transformed.c