Merge pull request #213 from mtzguido/fix #278
Annotations
30 warnings
|
Steel CI:
Steel.ST.Effect.AtomicAndGhost.fsti#L185
(352) * Warning 352 at /__w/steel/steel/steel/lib/steel/Steel.ST.Effect.AtomicAndGhost.fsti(185,16-185,20):
- Combinator (Steel.ST.Effect.AtomicAndGhost.STAGCommon ,
Steel.ST.Effect.AtomicAndGhost.STAGCommon) |>
Steel.ST.Effect.AtomicAndGhost.STAGCommon is not a substitutive indexed
effect combinator, it is better to make it one if possible for better
performance and ease of use
|
|
Steel CI:
Steel.ST.Effect.fsti#L169
(352) * Warning 352 at /__w/steel/steel/steel/lib/steel/Steel.ST.Effect.fsti(169,24-169,36):
- Combinator ite_Steel.ST.Effect.STBase is not a substitutive indexed effect
combinator, it is better to make it one if possible for better performance
and ease of use
|
|
Steel CI:
Steel.ST.Effect.fsti#L168
(352) * Warning 352 at /__w/steel/steel/steel/lib/steel/Steel.ST.Effect.fsti(168,19-168,26):
- Combinator Steel.ST.Effect.STBase <: Steel.ST.Effect.STBase is not a
substitutive indexed effect combinator, it is better to make it one if
possible for better performance and ease of use
|
|
Steel CI:
Steel.ST.Effect.fsti#L167
(352) * Warning 352 at /__w/steel/steel/steel/lib/steel/Steel.ST.Effect.fsti(167,16-167,20):
- Combinator (Steel.ST.Effect.STBase , Steel.ST.Effect.STBase) |>
Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it
is better to make it one if possible for better performance and ease of use
|
|
Steel CI:
Steel.ST.Effect.fsti#L169
(352) * Warning 352 at /__w/steel/steel/steel/lib/steel/Steel.ST.Effect.fsti(169,24-169,36):
- Combinator ite_Steel.ST.Effect.STBase is not a substitutive indexed effect
combinator, it is better to make it one if possible for better performance
and ease of use
|
|
Steel CI:
Steel.ST.Effect.fsti#L168
(352) * Warning 352 at /__w/steel/steel/steel/lib/steel/Steel.ST.Effect.fsti(168,19-168,26):
- Combinator Steel.ST.Effect.STBase <: Steel.ST.Effect.STBase is not a
substitutive indexed effect combinator, it is better to make it one if
possible for better performance and ease of use
|
|
Steel CI:
Steel.ST.Effect.fsti#L167
(352) * Warning 352 at /__w/steel/steel/steel/lib/steel/Steel.ST.Effect.fsti(167,16-167,20):
- Combinator (Steel.ST.Effect.STBase , Steel.ST.Effect.STBase) |>
Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it
is better to make it one if possible for better performance and ease of use
|
|
Steel CI:
Steel.Effect.Common.fsti#L415
(340) * Warning 340 at /__w/steel/steel/steel/lib/steel/Steel.Effect.Common.fsti(461,24-461,37):
- Unfolding name which is marked as a plugin: frame_vc_norm
- See also /__w/steel/steel/steel/lib/steel/Steel.Effect.Common.fsti(415,4-415,17)
|
|
Steel CI:
Steel.Effect.Common.fsti#L2066
(337) * Warning 337 at /__w/steel/steel/steel/lib/steel/Steel.Effect.Common.fsti(2066,65-2066,66):
- 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 '@'.
|
|
Steel CI:
ExtractSteel.Krml.fst#L33
(337) * Warning 337 at /__w/steel/steel/steel/src/extraction/ExtractSteel.Krml.fst(33,41-33,42):
- 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 '@'.
|
|
Build karamel (if not cached):
FStar.Krml.Endianness.fst#L21
(288) * Warning 288 at FStar.Krml.Endianness.fst(58,34-58,41):
- FStar.Krml.Endianness.le_to_n is deprecated
- FStar.Endianness.le_to_n
- See also FStar.Krml.Endianness.fst(21,8-21,15)
|
|
Build karamel (if not cached):
FStar.Krml.Endianness.fst#L21
(288) * Warning 288 at FStar.Krml.Endianness.fst(58,11-58,18):
- FStar.Krml.Endianness.le_to_n is deprecated
- FStar.Endianness.le_to_n
- See also FStar.Krml.Endianness.fst(21,8-21,15)
|
|
Build karamel (if not cached):
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)
|
|
Build karamel (if not cached):
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)
|
|
Build karamel (if not cached):
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)
|
|
Build karamel (if not cached):
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)
|
|
Build karamel (if not cached):
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)
|
|
Build karamel (if not cached):
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)
|
|
Build karamel (if not cached):
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)
|
|
Build karamel (if not cached):
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
|
|
Build F*:
FStarC.Parser.ToDocument.fst#L1989
(328) * Warning 328 at /__w/steel/steel/FStar/src/parser/FStarC.Parser.ToDocument.fst(1989,4-1989,12):
- Global binding
'FStarC.Parser.ToDocument.p_tmNoEq'
is recursive but not used in its body
|
|
Build F*:
FStarC.Parser.ToDocument.fst#L1725
(328) * Warning 328 at /__w/steel/steel/FStar/src/parser/FStarC.Parser.ToDocument.fst(1725,4-1725,21):
- Global binding
'FStarC.Parser.ToDocument.p_maybeFocusArrow'
is recursive but not used in its body
|
|
Build F*:
FStarC.Parser.ToDocument.fst#L1093
(328) * Warning 328 at /__w/steel/steel/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
|
|
Build F*:
FStarC.Parser.ToDocument.fst#L754
(328) * Warning 328 at /__w/steel/steel/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
|
|
Build F*:
FStarC.Parser.ToDocument.fst#L733
(328) * Warning 328 at /__w/steel/steel/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
|
|
Build F*:
FStarC.Plugins.fst#L88
(337) * Warning 337 at /__w/steel/steel/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 '@'.
|
|
Build F*:
FStarC.Plugins.fst#L87
(337) * Warning 337 at /__w/steel/steel/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 '@'.
|
|
Build F*:
FStarC.Plugins.fst#L86
(337) * Warning 337 at /__w/steel/steel/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 '@'.
|
|
Build F*:
FStarC.Plugins.fst#L85
(337) * Warning 337 at /__w/steel/steel/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 '@'.
|
|
Build F*:
FStar.UInt.fsti#L436
(271) * Warning 271 at /__w/steel/steel/FStar/stage0/out/lib/fstar/ulib/FStar.UInt.fsti(436,8-436,51):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
|
Loading