Use pprint for SMT encoding. #156
Annotations
10 warnings
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.TSet.fst#L28
(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.TSet.fst(28,4-28,7):
- Values of type `set` cannot be erased during extraction, but the
`must_erase_for_extraction` attribute claims that it can.
- Please remove the attribute.
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar/FStar/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
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fst(293,8-293,25):
- Pattern uses these theory symbols or terms that should not be in an SMT
pattern:
Prims.op_Subtraction
- See also /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fsti(435,8-435,51)
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/ulib/FStar.UInt.fsti#L435
(271) * Warning 271 at /home/runner/work/FStar/FStar/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
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
ulib/FStar.GhostSet.fst#L23
(318) * Warning 318 at ulib/FStar.GhostSet.fst(23,4-23,7):
- Values of type `set` cannot be erased during extraction, but the
`must_erase_for_extraction` attribute claims that it can.
- Please remove the attribute.
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
dummy#L1
(242) * Warning 242 at ulib/FStar.WellFounded.fst(122,0-131,33):
- Definitions of inner let-rec aux and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: ulib/FStar.WellFounded.fst(86,12-86,15)
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
dummy#L1
(242) * Warning 242 at ulib/FStar.WellFounded.fst(122,0-131,33):
- Definitions of inner let-rec aux and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: ulib/FStar.WellFounded.fst(126,12-126,15)
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
dummy#L1
(242) * Warning 242 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.LexicographicOrdering.fsti(187,0-194,59):
- Definitions of inner let-rec lex_t_wf_aux_y and its enclosing top-level
letbinding are not encoded to the solver, you will only be able to reason
with their types
- Also see: ulib/FStar.LexicographicOrdering.fst(75,14-75,28)
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
dummy#L1
(242) * Warning 242 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.LexicographicOrdering.fsti(187,0-194,59):
- Definitions of inner let-rec get_acc and its enclosing top-level letbinding
are not encoded to the solver, you will only be able to reason with their
types
- Also see: ulib/FStar.LexicographicOrdering.fst(124,10-124,17)
|
|
Run eval $(opam env) && make -kj$(nproc) ADMIT=1:
fstar/src/data/FStarC.RBSet.fst#L105
(337) * Warning 337 at /home/runner/work/FStar/FStar/fstar/src/data/FStarC.RBSet.fst(105,30-105,31):
- 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 '@'.
|
Loading