Emit a result-determining postcondition as rewrites_to - #240
Draft
nikswamy wants to merge 8 commits into
Draft
Annotations
21 warnings
|
Complete job
Node.js 20 is deprecated. The following actions target Node.js 20 but are being forced to run on Node.js 24: actions/checkout@v3. For more information see: https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/
|
|
Test pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/pulse.checked/Pulse.fst.checked
instead of _cache/Pulse.fst.checked
|
|
Test pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse.Main to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/common.checked/Pulse.Main.fsti.checked
instead of _cache/Pulse.Main.fsti.checked
|
|
Test pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/pulse.checked/Pulse.fst.checked
instead of _cache/Pulse.fst.checked
|
|
Test pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse.Main to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/common.checked/Pulse.Main.fsti.checked
instead of _cache/Pulse.Main.fsti.checked
|
|
Test pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/pulse.checked/Pulse.fst.checked
instead of _cache/Pulse.fst.checked
|
|
Test pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse.Main to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/common.checked/Pulse.Main.fsti.checked
instead of _cache/Pulse.Main.fsti.checked
|
|
Test pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/pulse.checked/Pulse.fst.checked
instead of _cache/Pulse.fst.checked
|
|
Test pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse.Main to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/common.checked/Pulse.Main.fsti.checked
instead of _cache/Pulse.Main.fsti.checked
|
|
Test pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/pulse.checked/Pulse.fst.checked
instead of _cache/Pulse.fst.checked
|
|
Test pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse.Main to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/common.checked/Pulse.Main.fsti.checked
instead of _cache/Pulse.Main.fsti.checked
|
|
Build pal:
Pulse.Lib.C.Array.fst#L220
(288) * Warning 288 at Pulse.Lib.C.Array.fst(220,4-220,13):
- Pulse.Lib.Array.Core.mask_free is deprecated
- Array.mask_free is unsound; only use for model implementations
- See also Pulse.Lib.C.Array.fst(220,2-220,15)
|
|
Build pal:
Pulse.Lib.C.Array.fst#L220
(288) * Warning 288 at Pulse.Lib.C.Array.fst(220,4-220,13):
- Pulse.Lib.Array.Core.mask_free is deprecated
- Array.mask_free is unsound; only use for model implementations
- See also Pulse.Lib.C.Array.fst(220,2-220,15)
|
|
Build pal:
Pulse.Lib.C.Array.fst#L202
(288) * Warning 288 at Pulse.Lib.C.Array.fst(203,12-203,22):
- Pulse.Lib.Array.Core.mask_alloc is deprecated
- Array.mask_alloc is unsound; only use for model implementations
- See also Pulse.Lib.C.Array.fst(202,1-210,3)
|
|
Build pal:
Pulse.Lib.C.Array.fst#L202
(288) * Warning 288 at Pulse.Lib.C.Array.fst(203,12-203,22):
- Pulse.Lib.Array.Core.mask_alloc is deprecated
- Array.mask_alloc is unsound; only use for model implementations
- See also Pulse.Lib.C.Array.fst(202,1-210,3)
|
|
Build pal:
FStar.Int.Cast.fst#L170
(288) * Warning 288 at Pulse.Lib.C.Casts.fst(25,4-25,19):
- FStar.Int.Cast.uint64_to_int64 is deprecated
- with care; in C the result is implementation-defined when not representable
- See also /home/runner/.local/fstar/lib/fstar/ulib/FStar.Int.Cast.fst(170,4-170,19)
|
|
Build pal:
FStar.Int.Cast.fst#L170
(288) * Warning 288 at Pulse.Lib.C.Casts.fst(25,4-25,19):
- FStar.Int.Cast.uint64_to_int64 is deprecated
- with care; in C the result is implementation-defined when not representable
- See also /home/runner/.local/fstar/lib/fstar/ulib/FStar.Int.Cast.fst(170,4-170,19)
|
|
Build pal:
FStar.Int.Cast.fst#L155
(288) * Warning 288 at Pulse.Lib.C.Casts.fst(21,4-21,19):
- FStar.Int.Cast.uint32_to_int32 is deprecated
- with care; in C the result is implementation-defined when not representable
- See also /home/runner/.local/fstar/lib/fstar/ulib/FStar.Int.Cast.fst(155,4-155,19)
|
|
Build pal:
FStar.Int.Cast.fst#L155
(288) * Warning 288 at Pulse.Lib.C.Casts.fst(21,4-21,19):
- FStar.Int.Cast.uint32_to_int32 is deprecated
- with care; in C the result is implementation-defined when not representable
- See also /home/runner/.local/fstar/lib/fstar/ulib/FStar.Int.Cast.fst(155,4-155,19)
|
|
Build pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/pulse.checked/Pulse.fst.checked
instead of _cache/Pulse.fst.checked
|
|
Build pal:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse.Main to be already checked.
- Found it in an unexpected location:
/home/runner/.local/fstar/lib/fstar/pulse/common.checked/Pulse.Main.fsti.checked
instead of _cache/Pulse.Main.fsti.checked
|
background
wait
wait-all
cancel
parallel
Loading