You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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 text was updated successfully, but these errors were encountered:
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)
The text was updated successfully, but these errors were encountered: