Formatting. #537
Annotations
6 warnings
|
main:
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/work/c2pulse/c2pulse/opt/fstar/stage2/out/lib/fstar/ulib/FStar.Int.Cast.fst(170,4-170,19)
|
|
main:
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/work/c2pulse/c2pulse/opt/fstar/stage2/out/lib/fstar/ulib/FStar.Int.Cast.fst(170,4-170,19)
|
|
main:
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/work/c2pulse/c2pulse/opt/fstar/stage2/out/lib/fstar/ulib/FStar.Int.Cast.fst(155,4-155,19)
|
|
main:
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/work/c2pulse/c2pulse/opt/fstar/stage2/out/lib/fstar/ulib/FStar.Int.Cast.fst(155,4-155,19)
|
|
main:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse.Main to be already checked.
- Found it in an unexpected location:
/home/runner/work/c2pulse/c2pulse/opt/pulse/out/lib/pulse/lib/Pulse.Main.fsti.checked
instead of _cache/Pulse.Main.fsti.checked
|
|
main:
dummy#L0
(321) * Warning 321:
- Did not expect module Pulse to be already checked.
- Found it in an unexpected location:
/home/runner/work/c2pulse/c2pulse/opt/pulse/out/lib/pulse/lib/Pulse.fst.checked
instead of _cache/Pulse.fst.checked
|