Use a Pulse-specific _zero_for_deref instead of Low* KrmlLib
#592
Annotations
5 errors and 11 warnings
|
Pulse CI
Process completed with exit code 2.
|
|
Pulse CI:
ExtractPulse.fst#L121
(58) * Error 58 at /__w/pulse/pulse/pulse/src/extraction/ExtractPulse.fst(121,6-121,52):
- Expected a ghost expression.
- Because: arguments to short circuiting operators must be pure or ghost.
- Got an expression
let _ = FStarC.Extraction.ML.Syntax.string_of_mlpath p in
_ = "Pulse.Lib.ArrayPtr.null"
with effect 'FStarC.Effect.ALL'.
|
|
Pulse CI:
ExtractPulseC.fst#L89
(58) * Error 58 at /__w/pulse/pulse/pulse/src/extraction/ExtractPulseC.fst(89,4-89,79):
- Expected a ghost expression.
- Because: arguments to short circuiting operators must be pure or ghost.
- Got an expression
let _ = FStarC.Extraction.ML.Syntax.string_of_mlpath p in
FStarC.Util.starts_with _ "Pulse.C.Types.Struct.struct_t0"
with effect 'FStarC.Effect.ALL'.
|
|
Pulse CI:
PulseSyntaxExtension.Sugar.fst#L400
(58) * Error 58 at /__w/pulse/pulse/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(400,20-400,25):
- Expected a ghost expression.
- Because: arguments to short circuiting operators must be pure or ghost.
- Got an expression f x y with effect 'FStarC.Effect.ML'.
|
|
Pulse CI:
ExtractPulseOCaml.fst#L137
(58) * Error 58 at /__w/pulse/pulse/pulse/src/extraction/ExtractPulseOCaml.fst(137,11-137,71):
- Expected a ghost expression.
- Because: arguments to short circuiting operators must be pure or ghost.
- Got an expression
let _ = FStarC.Ident.lid_of_str "Pulse.Lib.Reference.read" in
FStarC.Syntax.Syntax.fv_eq_lid fv _
with effect 'FStarC.Effect.ML'.
|
|
Complete job
Node.js 20 actions are deprecated. The following actions are running on Node.js 20 and may not work as expected: actions/cache/restore@v4, zulip/github-actions-zulip/send-message@v1. Actions will be forced to run with Node.js 24 by default starting June 2nd, 2026. Please check if updated versions of these actions are available that support Node.js 24. To opt into Node.js 24 now, set the FORCE_JAVASCRIPT_ACTIONS_TO_NODE24=true environment variable on the runner or in your workflow file. Once Node.js 24 becomes the default, you can temporarily opt out by setting ACTIONS_ALLOW_USE_UNSECURE_NODE_VERSION=true. For more information see: https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/
|
|
Pulse CI:
Pulse.Syntax.Base.fst#L292
(290) * Warning 290 at /__w/pulse/pulse/pulse/src/checker/Pulse.Syntax.Base.fst(292,15-292,17):
- In the decreases clause for this function, the SMT solver may not be able to
prove that the types of
b1 (bound in Pulse.Syntax.Base.fst(292,15-292,17))
and t1 (bound in Pulse.Syntax.Base.fst(173,20-173,22))
are equal.
- The type of the first term is: Pulse.Syntax.Base.branch
- The type of the second term is: Pulse.Syntax.Base.st_term
- If the proof fails, try annotating these with the same type.
|
|
Pulse CI:
Pulse.Syntax.Base.fst#L297
(290) * Warning 290 at /__w/pulse/pulse/pulse/src/checker/Pulse.Syntax.Base.fst(297,14-297,16):
- In the decreases clause for this function, the SMT solver may not be able to
prove that the types of
q1 (bound in Pulse.Syntax.Base.fst(297,14-297,16))
and t1 (bound in Pulse.Syntax.Base.fst(173,20-173,22))
are equal.
- The type of the first term is: Pulse.Syntax.Base.qualifier
- The type of the second term is: Pulse.Syntax.Base.st_term
- If the proof fails, try annotating these with the same type.
|
|
Pulse CI:
Pulse.Syntax.Base.fst#L123
(290) * Warning 290 at /__w/pulse/pulse/pulse/src/checker/Pulse.Syntax.Base.fst(123,20-123,22):
- In the decreases clause for this function, the SMT solver may not be able to
prove that the types of
p1 (bound in Pulse.Syntax.Base.fst(123,20-123,22))
and pb1 (bound in Pulse.Syntax.Base.fst(139,16-139,19))
are equal.
- The type of the first term is: Pulse.Syntax.Base.pattern
- The type of the second term is: Pulse.Syntax.Base.pattern & Prims.bool
- If the proof fails, try annotating these with the same type.
|
|
Pulse CI:
Pulse.Syntax.Base.fst#L139
(290) * Warning 290 at /__w/pulse/pulse/pulse/src/checker/Pulse.Syntax.Base.fst(139,16-139,19):
- In the decreases clause for this function, the SMT solver may not be able to
prove that the types of
pb1 (bound in Pulse.Syntax.Base.fst(139,16-139,19))
and p1 (bound in Pulse.Syntax.Base.fst(123,20-123,22))
are equal.
- The type of the first term is: Pulse.Syntax.Base.pattern & Prims.bool
- The type of the second term is: Pulse.Syntax.Base.pattern
- If the proof fails, try annotating these with the same type.
|
|
Pulse CI:
Pulse.Lib.Raise.fst#L21
(318) * Warning 318 at /__w/pulse/pulse/pulse/lib/common/Pulse.Lib.Raise.fst(21,4-21,12):
- Values of type `raisable` will be erased during extraction, but its
interface hides this fact.
- Add the `must_erase_for_extraction` attribute to the `val raisable`
declaration for this symbol in the interface
|
|
Pulse CI:
Pulse.Common.fst#L84
(337) * Warning 337 at /__w/pulse/pulse/pulse/src/checker/Pulse.Common.fst(84,11-84,12):
- The operator '@' has been resolved to FStar.List.Tot.append even though
FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop
relying on this deprecated, special treatment of '@'.
|
|
Pulse CI:
PulseSyntaxExtension.SyntaxWrapper.fsti#L90
(239) * Warning 239 at /__w/pulse/pulse/pulse/src/syntax_extension/PulseSyntaxExtension.SyntaxWrapper.fsti(90,5-90,11):
- Adding an implicit 'assume new' qualifier on PulseSyntaxExtension.SyntaxWrapper.branch
|
|
Pulse CI:
ExtractPulse.fst#L66
(272) * Warning 272 at /__w/pulse/pulse/pulse/src/extraction/ExtractPulse.fst(66,0-66,41):
- Top-level let-bindings must be total; this term may have effects
|
|
Pulse CI:
ExtractPulse.fst#L32
(272) * Warning 272 at /__w/pulse/pulse/pulse/src/extraction/ExtractPulse.fst(32,0-32,39):
- Top-level let-bindings must be total; this term may have effects
|
|
Pulse CI:
ExtractPulseOCaml.fst#L33
(272) * Warning 272 at /__w/pulse/pulse/pulse/src/extraction/ExtractPulseOCaml.fst(33,0-33,39):
- Top-level let-bindings must be total; this term may have effects
|
Loading