Do not turn trivially diverging loops into assume(false)

[tautschnig]

CBMC's symbolic execution by default turns while(true) {} loops into assume(false) to counter trivial non-termination of symbolic execution. When unwinding assertions are enabled, however, we should report the non-termination of such loops.

Resolves: #2909

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[zhassan-aws]

Thanks @tautschnig for the quick fix! Should we consider this a soundness issue in CBMC and fix it on the CBMC side instead? i.e., when unwinding assertions are enabled, self loops should not be replaced with assume(false)?

[tautschnig]

Thanks @tautschnig for the quick fix! Should we consider this a soundness issue in CBMC and fix it on the CBMC side instead? i.e., when unwinding assertions are enabled, self loops should not be replaced with assume(false)?

I think we should indeed seek to make this consistent on the CBMC side for version 6. I'll come up with a PR.

[qinheping]

Yes, when applying loop contracts, lack of decreases may lead to vacuous verification, which is the case of Zyad's comment. Now the synthesizer for Kani doesn't synthesize decrease clauses, and should does before it became stable.

[feliperodri]

Thanks @tautschnig for the quick fix! Should we consider this a soundness issue in CBMC and fix it on the CBMC side instead? i.e., when unwinding assertions are enabled, self loops should not be replaced with assume(false)?

I think we should indeed seek to make this consistent on the CBMC side for version 6. I'll come up with a PR.

@tautschnig if we fix this on version 6, we do not need to merge this PR, correct? Shall we close it in favor of the new update?

[tautschnig]

Thanks @tautschnig for the quick fix! Should we consider this a soundness issue in CBMC and fix it on the CBMC side instead? i.e., when unwinding assertions are enabled, self loops should not be replaced with assume(false)?

I think we should indeed seek to make this consistent on the CBMC side for version 6. I'll come up with a PR.

@tautschnig if we fix this on version 6, we do not need to merge this PR, correct? Shall we close it in favor of the new update?

Merging this PR would help disentangle a Kani issue from the CBMC release. Once CBMC v6 is released and Kani starts using it we can then remove this, but then we will anyway end up removing several options from the command line being used to invoke CBMC.