Skip to content

AST and semantics of integer ranges #18

AST and semantics of integer ranges

AST and semantics of integer ranges #18

Triggered via push January 16, 2025 07:54
Status Failure
Total duration 1h 41m 8s
Artifacts

ci.yml

on: push
Fit to window
Zoom out
Zoom in

Annotations

8 errors and 11 warnings
ci: src/cddl/pulse/CDDL.Pulse.Base.fst#L15
(228) * Error 228 at src/cddl/pulse/CDDL.Pulse.Base.fst(15,9-15,9): - Could not check term: cbor_get_major_type: CBOR.Pulse.API.Base.get_major_type_t vmatch -> cbor_destr_string: CBOR.Pulse.API.Base.get_string_t vmatch -> ty: CBOR.Spec.Constants.major_type_byte_string_or_text_string -> sz: FStar.SizeT.t -> c: t -> Pulse.Lib.Core.stt Prims.bool (vmatch p c v ** Pulse.Lib.Core.pure (CDDL.Spec.Base.opt_precedes v FStar.Pervasives.Native.None)) (fun res -> vmatch p c v ** Pulse.Lib.Core.pure (CDDL.Spec.Base.opt_precedes v FStar.Pervasives.Native.None /\ res == CDDL.Spec.Misc.str_size ty (FStar.SizeT.v sz) v))
ci: src/cddl/pulse/CDDL.Pulse.Base.fst#L23
(12) * Error 12 at src/cddl/pulse/CDDL.Pulse.Base.fst(23,19-23,22): - Expected type Prims.bool but CDDL.Spec.Misc.str_size ty (FStar.SizeT.v sz) v has type CDDL.Spec.Base.typ - Raised within Tactics.refl_instantiate_implicits
ci: src/cddl/pulse/CDDL.Pulse.Base.fst#L16
(12) * Error 12 at src/cddl/pulse/CDDL.Pulse.Base.fst(23,21-23,22): - Expected type Prims.nat but v has type CBOR.Spec.API.Type.cbor - Raised within Tactics.refl_instantiate_implicits - See also src/cddl/pulse/CDDL.Pulse.Base.fst(16,6-16,7)
ci: out.fail.batch/FAILAllBytesCompose.fst#L81
(66) * Error 66 at out.fail.batch/FAILAllBytesCompose.fst(81,6-87,85): - Failed to resolve implicit argument ?57 of type Prims.bool introduced for Instantiating implicit argument
ci: out.fail.batch/FAILAllBytesCompose.fst#L83
(12) * Error 12 at out.fail.batch/FAILAllBytesCompose.fst(83,10-85,52): - Expected type EverParse3d.Interpreter.typ (*?u58*) _ (*?u59*) _ (*?u60*) _ (*?u61*) _ (*?u62*) _ (*?u63*) _ but EverParse3d.Interpreter.T_with_comment "should_not_be_here" (EverParse3d.Interpreter.T_denoted "should_not_be_here" dtyp__test1) "Validating field should_not_be_here" has type EverParse3d.Interpreter.typ kind__test1 EverParse3d.Interpreter.Trivial EverParse3d.Interpreter.Trivial EverParse3d.Interpreter.Trivial false false
ci: ulib/Prims.fst#L459
(19) * Error 19 at out.fail.batch/FAILAllBytesNotLast.fst(14,2-34,16): - Could not prove goal #1 - The SMT solver could not prove the query. Use --query_stats for more details. - See also ulib/Prims.fst(459,77-459,89)
ci: out.fail.batch/FAILAllBytesNotLast.fst#L43
(189) * Error 189 at out.fail.batch/FAILAllBytesNotLast.fst(43,53-43,67): - Expected expression of type EverParse3d.Kinds.parser_kind (*?u58*) _ EverParse3d.Kinds.WeakKindStrongPrefix got expression EverParse3d.Kinds.kind_all_bytes of type EverParse3d.Kinds.parser_kind false EverParse3d.Kinds.WeakKindConsumesAll
ci
Process completed with exit code 2.
ci
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
ci: dummy#L1
(274) * Warning 274: - Implicitly opening namespace 'cbor.pulse.api.det.' shadows module 'c' in file "/__w/everparse/everparse/karamel/krmllib/C.fst". - Rename "/__w/everparse/everparse/karamel/krmllib/C.fst" to avoid conflicts.
ci: dummy#L1
(361) * Warning 361 at Options.fst(594,0-597,15): - Some #push-options have not been popped. Current depth is 1.
ci: dummy#L1
(274) * Warning 274: - Implicitly opening namespace 'cbor.pulse.api.det.' shadows module 'c' in file "/__w/everparse/everparse/karamel/krmllib/C.fst". - Rename "/__w/everparse/everparse/karamel/krmllib/C.fst" to avoid conflicts.
ci: dummy#L1
(242) * Warning 242 at Ast.fst(395,0-429,18): - Definitions of inner let-rec seq and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: Ast.fst(397,12-397,15)
ci: dummy#L1
(242) * Warning 242 at Ast.fst(1251,0-1256,14): - Definitions of inner let-rec seq and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: Ast.fst(397,12-397,15)
ci: dummy#L1
(361) * Warning 361 at src/lowparse/LowParse.BitFields.fst(1276,0-1276,29): - Some #push-options have not been popped. Current depth is 1.
ci: Target.fst#L958
(337) * Warning 337 at Target.fst(958,28-958,29): - 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 '@'.
ci: Target.fst#L1051
(337) * Warning 337 at Target.fst(1051,69-1051,70): - 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 '@'.
ci: Target.fst#L1395
(337) * Warning 337 at Target.fst(1395,54-1395,55): - 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 '@'.
ci: dummy#L1
(361) * Warning 361 at Target.fst(1477,0-1501,9): - Some #push-options have not been popped. Current depth is 1.