list_loop_exec.c0 under the bugs folder is failing an assert at run time

[jennalwise]

While I was testing my Translator changes, I was testing the list_loop_exec.c0 file in the bugs folder and it is failing an assert likely injected for dynamic verification at run time. The program fails with the same error even when I revert my changes to the most recent commit in silicon-gv. The error message is as follows:

[error] c0rt: src/test/resources/bugs/list_loop_exec.verified.c0: 208.5-208.46: assert failed
[error] Nonzero exit code returned from runner: 134
[error] (Compile / run) Nonzero exit code returned from runner: 134
[error] Total time: 10 s, completed May 24, 2022, 5:50:09 PM

[jennalwise]

This is a file in my local repo only, so I will take a look at this when I have some time. Since it is in my local repo, there could be a problem with the file itself rather than the verifier.

[jennalwise]

Gradual C0 is operating correctly for this example. In list_loop_exec.c0 the loop invariant along the !(list == NULL || val <= list->val) path is completely precise and not well-formed: acc(curr->next->val) is not framed. Therefore, static verification fails down the !(list == NULL || val <= list->val) path and a run-time check for (list == NULL || val <= list->val) is optimistically added before the if that contains (list == NULL || val <= list->val) to force it down the true branch which succeeds static verification. Of course, at run-time the main program is designed to go down the statically failing branch, so dynamic verification/the inserted assert correctly fails.

[jennalwise]

Before closing this issue, I want to look into gradual_list.c0 which is also a local test file that is failing for me. I suspect it is failing for a similar reason to list_loop_exec.c0