The attached file avl-bug1.c0.txt is a version of a correctly running c0 program with "//@requires ?;" added to functions that should need it. Running with -x yields the error:
sbt:gvc0> run -x avl.c0
[info] running (fork) gvc.Main -x avl.c0
[error] Error: Field access runtime check failed for struct Node.key
[error] Nonzero exit code returned from runner: 1
[error] (Compile / run) Nonzero exit code returned from runner: 1
[error] Total time: 4 s, completed May 20, 2022, 10:26:55 PM
It appears that the ? at the top of the function is not generating the required permission everywhere it needs to.
I tried to isolate the issue by commenting out accesses to the key field, but I ran into another bug (filing separately)
The attached file avl-bug1.c0.txt is a version of a correctly running c0 program with "//@requires ?;" added to functions that should need it. Running with -x yields the error:
It appears that the ? at the top of the function is not generating the required permission everywhere it needs to.
I tried to isolate the issue by commenting out accesses to the key field, but I ran into another bug (filing separately)