Skip to content

Try to carefully set up merkle Put loopInv to unravel nicely when fix… #551

Try to carefully set up merkle Put loopInv to unravel nicely when fix…

Try to carefully set up merkle Put loopInv to unravel nicely when fix… #551

Triggered via push December 9, 2024 06:34
Status Failure
Total duration 1h 7m 15s
Artifacts

ci.yml

on: push
Matrix: build-vos
Matrix: build
Fit to window
Zoom out
Zoom in

Annotations

9 errors and 5 warnings
build-vos (dev): src/program_proof/tulip/invariance/linearize.v#L260
UNDEFINED EVARS:?X319==[Σ tulip_ghostG0 γ p ts tid future rds form Q m |- Union dbmap] (parameter Union of union) {?Union}
build-vos (dev): src/program_proof/tulip/invariance/learn.v#L7
UNDEFINED EVARS:?X24==[Σ tulip_ghostG0 γ p gid cpool cmds log |- heapGS ?Σ] (parameter heapGS0 of txnsys_inv) {?heapGS0}
build (dev): src/program_proof/tulip/invariance/linearize.v#L260
UNDEFINED EVARS:?X47690==[Σ tulip_ghostG0 γ p ts tid future rds form Q m |- Union dbmap] (parameter Union of union) {?Union}
build (dev): src/program_proof/tulip/invariance/learn.v#L7
UNDEFINED EVARS:?X24==[Σ tulip_ghostG0 γ p gid cpool cmds log |- heapGS ?Σ] (parameter heapGS0 of txnsys_inv) {?heapGS0}
build (8.20): src/program_proof/tulip/invariance/linearize.v#L260
UNDEFINED EVARS:?X47769==[Σ tulip_ghostG0 γ p ts tid future rds form Q m |- Union dbmap] (parameter Union of union) {?Union}
build (8.20): src/program_proof/tulip/invariance/learn.v#L7
UNDEFINED EVARS:?X24==[Σ tulip_ghostG0 γ p gid cpool cmds log |- heapGS ?Σ@{γ:=γ; p:=p; gid:=gid; cpool:=cpool; cmds:=cmds}] (parameter heapGS0 of txnsys_inv) {?heapGS0}
python
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
check-goose
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
build-vos (dev)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
build (dev)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
build (8.20)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636