Merge pull request #169 from mtzguido/make_nit #97
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.
|