Skip to content

Merge pull request #169 from mtzguido/make_nit #97

Merge pull request #169 from mtzguido/make_nit

Merge pull request #169 from mtzguido/make_nit #97

Triggered via push February 19, 2025 19:54
Status Success
Total duration 48m 55s
Artifacts

ci.yml

on: push
Fit to window
Zoom out
Zoom in

Annotations

30 warnings
ci: FStar/stage0/out/bin/../lib/fstar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /__w/everparse/everparse/FStar/stage0/out/bin/../lib/fstar/ulib/FStar.UInt.fsti(435,8-435,51): - Pattern uses these theory symbols or terms that should not be in an SMT pattern: Prims.op_Subtraction
ci: FStar/src/basic/FStarC.Plugins.fst#L85
(337) * Warning 337 at /__w/everparse/everparse/FStar/src/basic/FStarC.Plugins.fst(85,16-85,17): - 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: FStar/src/basic/FStarC.Plugins.fst#L86
(337) * Warning 337 at /__w/everparse/everparse/FStar/src/basic/FStarC.Plugins.fst(86,16-86,17): - 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: FStar/src/basic/FStarC.Plugins.fst#L87
(337) * Warning 337 at /__w/everparse/everparse/FStar/src/basic/FStarC.Plugins.fst(87,16-87,17): - 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: FStar/src/basic/FStarC.Plugins.fst#L88
(337) * Warning 337 at /__w/everparse/everparse/FStar/src/basic/FStarC.Plugins.fst(88,16-88,17): - 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: FStar/src/parser/FStarC.Parser.AST.fst#L772
(328) * Warning 328 at /__w/everparse/everparse/FStar/src/parser/FStarC.Parser.AST.fst(772,8-772,22): - Global binding 'FStarC.Parser.AST.decl_to_string' is recursive but not used in its body
ci: FStar/src/parser/FStarC.Parser.ToDocument.fst#L733
(328) * Warning 328 at /__w/everparse/everparse/FStar/src/parser/FStarC.Parser.ToDocument.fst(733,8-733,14): - Global binding 'FStarC.Parser.ToDocument.p_decl' is recursive but not used in its body
ci: FStar/src/parser/FStarC.Parser.ToDocument.fst#L754
(328) * Warning 328 at /__w/everparse/everparse/FStar/src/parser/FStarC.Parser.ToDocument.fst(754,4-754,13): - Global binding 'FStarC.Parser.ToDocument.p_justSig' is recursive but not used in its body
ci: FStar/src/parser/FStarC.Parser.ToDocument.fst#L1093
(328) * Warning 328 at /__w/everparse/everparse/FStar/src/parser/FStarC.Parser.ToDocument.fst(1093,4-1093,24): - Global binding 'FStarC.Parser.ToDocument.p_disjunctivePattern' is recursive but not used in its body
ci: FStar/src/parser/FStarC.Parser.ToDocument.fst#L1731
(328) * Warning 328 at /__w/everparse/everparse/FStar/src/parser/FStarC.Parser.ToDocument.fst(1731,4-1731,21): - Global binding 'FStarC.Parser.ToDocument.p_maybeFocusArrow' is recursive but not used in its body
ci: Spec.Loops.fst#L47
(328) * Warning 328 at Spec.Loops.fst(47,8-47,19): - Global binding 'Spec.Loops.repeat_base' is recursive but not used in its body
ci: dummy#L1
(250) * Warning 250: - Error while extracting LowStar.Monotonic.Buffer.mgcmalloc_of_list_partial to KaRaMeL. - Failure("Argument of FStar.Buffer.createL is not a list literal!")
ci: dummy#L1
(250) * Warning 250: - Error while extracting FStar.List.filter_map to KaRaMeL. - Failure("Internal error: name not found filter_map_acc\n")
ci: dummy#L1
(250) * Warning 250: - Error while extracting FStar.List.index to KaRaMeL. - Failure("Internal error: name not found index\n")
ci: FStar.Krml.Endianness.fst#L21
(288) * Warning 288 at FStar.Krml.Endianness.fst(45,13-45,20): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)
ci: FStar.Krml.Endianness.fst#L21
(288) * Warning 288 at FStar.Krml.Endianness.fst(47,8-47,32): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)
ci: FStar.Krml.Endianness.fst#L21
(288) * Warning 288 at FStar.Krml.Endianness.fst(55,11-55,18): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)
ci: FStar.Krml.Endianness.fst#L21
(288) * Warning 288 at FStar.Krml.Endianness.fst(56,11-56,18): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)
ci: FStar.Krml.Endianness.fst#L36
(288) * Warning 288 at FStar.Krml.Endianness.fst(57,4-57,28): - FStar.Krml.Endianness.lemma_euclidean_division is deprecated - FStar.Endianness.lemma_euclidean_division - See also FStar.Krml.Endianness.fst(36,4-36,28)
ci: FStar.Krml.Endianness.fst#L21
(288) * Warning 288 at FStar.Krml.Endianness.fst(57,56-57,63): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)
ci: dummy#L1
(361) * Warning 361 at LowParse.Spec.BoundedInt.fsti(232,0-235,62): - Some #push-options have not been popped. Current depth is 1.
ci: LowParse.Spec.Base.fsti#L544
(271) * Warning 271 at LowParse.Spec.Base.fsti(544,13-546,17): - Pattern misses at least one bound variable: t
ci: LowParse.Spec.Base.fsti#L546
(271) * Warning 271 at LowParse.Spec.Base.fsti(546,14-546,16): - SMT pattern misses at least one bound variable: t
ci: LowParse.Spec.Enum.fst#L107
(328) * Warning 328 at LowParse.Spec.Enum.fst(107,8-107,24): - Global binding 'LowParse.Spec.Enum.assoc_flip_intro' is recursive but not used in its body
ci: dummy#L1
(361) * Warning 361 at LowParse.BitFields.fst(1276,0-1276,29): - Some #push-options have not been popped. Current depth is 1.
ci: LowParse.Spec.BitSum.fst#L1421
(331) * Warning 331 at LowParse.Spec.BitSum.fst(1421,7-1421,8): - This name is being ignored
ci: dummy#L1
(361) * Warning 361 at LowParse.Spec.BitSum.fst(2116,0-2141,57): - Some #push-options have not been popped. Current depth is 2.
ci: LowParse.Low.Base.Spec.fst#L487
(337) * Warning 337 at LowParse.Low.Base.Spec.fst(487,8-487,18): - This definitions has multiple decreases clauses. - The decreases clause on the declaration is ignored, please remove it.
ci: LowParse.Low.Base.Spec.fst#L511
(328) * Warning 328 at LowParse.Low.Base.Spec.fst(511,8-511,24): - Global binding 'LowParse.Low.Base.Spec.valid_list_equiv' is recursive but not used in its body
ci: LowParse.Low.Base.Spec.fst#L548
(337) * Warning 337 at LowParse.Low.Base.Spec.fst(548,8-548,21): - This definitions has multiple decreases clauses. - The decreases clause on the declaration is ignored, please remove it.