Check world (test F* + all subprojects) #443
Annotations
10 errors and 10 warnings
|
Meta.Interface.fst#L237
(72) * Error 72 at /__w/FStar/FStar/hacl-star/code/meta/Meta.Interface.fst(237,18-237,32):
- Identifier not found: lookup_lb_view
|
|
Meta.Interface.fst#L237
(72) * Error 72 at /__w/FStar/FStar/hacl-star/code/meta/Meta.Interface.fst(237,18-237,32):
- Identifier not found: lookup_lb_view
|
|
Vale.AES.GCM_helpers.fst#L245
(19) * Error 19 at /__w/FStar/FStar/hacl-star/vale/code/crypto/aes/Vale.AES.GCM_helpers.fst(245,2-257,4):
- Could not prove post-condition
- The SMT solver could not prove the query. Use --query_stats for more
details.
- This query was retried due to the --proof_recovery option, yet it still
failed on all attempts.
- Also see: /__w/FStar/FStar/hacl-star/vale/code/crypto/aes/Vale.AES.GCM_helpers.fst(245,2-257,4)
- Other related locations: /__w/FStar/FStar/hacl-star/vale/code/crypto/aes/Vale.AES.GCM_helpers.fst(243,11-243,96)
|
|
Vale.AES.GCM_helpers.fst#L245
(19) * Error 19 at /__w/FStar/FStar/hacl-star/vale/code/crypto/aes/Vale.AES.GCM_helpers.fst(245,2-257,4):
- Could not prove post-condition
- The SMT solver could not prove the query. Use --query_stats for more
details.
- This query was retried due to the --proof_recovery option, yet it still
failed on all attempts.
- Also see: /__w/FStar/FStar/hacl-star/vale/code/crypto/aes/Vale.AES.GCM_helpers.fst(245,2-257,4)
- Other related locations: /__w/FStar/FStar/hacl-star/vale/code/crypto/aes/Vale.AES.GCM_helpers.fst(243,11-243,96)
|
|
Vale.Lib.Tactics.fst#L34
(72) * Error 72 at /__w/FStar/FStar/hacl-star/vale/code/lib/util/Vale.Lib.Tactics.fst(34,32-34,44):
- Identifier not found: bv_of_binder
|
|
Vale.Lib.Tactics.fst#L34
(72) * Error 72 at /__w/FStar/FStar/hacl-star/vale/code/lib/util/Vale.Lib.Tactics.fst(34,32-34,44):
- Identifier not found: bv_of_binder
|
|
Vale.Interop.Base.fst#L161
(19) * Error 19 at /__w/FStar/FStar/hacl-star/vale/specs/interop/Vale.Interop.Base.fst(161,2-163,64):
- Subtyping check failed
- Expected type Type got type n_arrow dom Type
- The SMT solver could not prove the query. Use --query_stats for more
details.
- This query was retried due to the --proof_recovery option, yet it still
failed on all attempts.
- Also see: /__w/FStar/FStar/hacl-star/vale/specs/interop/Vale.Interop.Base.fst(162,10-162,15)
- Other related locations: /__w/FStar/FStar/hacl-star/vale/specs/interop/Vale.Interop.Base.fst(160,35-160,40)
|
|
Vale.Interop.Base.fst#L161
(19) * Error 19 at /__w/FStar/FStar/hacl-star/vale/specs/interop/Vale.Interop.Base.fst(161,2-163,64):
- Subtyping check failed
- Expected type Type got type n_arrow dom Type
- The SMT solver could not prove the query. Use --query_stats for more
details.
- This query was retried due to the --proof_recovery option, yet it still
failed on all attempts.
- Also see: /__w/FStar/FStar/hacl-star/vale/specs/interop/Vale.Interop.Base.fst(162,10-162,15)
- Other related locations: /__w/FStar/FStar/hacl-star/vale/specs/interop/Vale.Interop.Base.fst(160,35-160,40)
|
|
Lib.Sequence.fst#L263
(19) * Error 19 at /__w/FStar/FStar/hacl-star/lib/Lib.Sequence.fst(263,52-279,5):
- Subtyping check failed
- Expected type map_blocks_a 0
got type s: FStar.Seq.Base.seq a {FStar.Seq.Base.length s = 0}
- Try with --query_stats to get more details
- This query was retried due to the --proof_recovery option, yet it still
failed on all attempts.
- Also see: /__w/FStar/FStar/hacl-star/lib/Lib.Sequence.fst(267,50-267,54)
- Other related locations: /__w/FStar/FStar/hacl-star/lib/Lib.Sequence.fst(266,6-266,10)
|
|
Lib.Sequence.fst#L263
(19) * Error 19 at /__w/FStar/FStar/hacl-star/lib/Lib.Sequence.fst(263,52-279,5):
- Subtyping check failed
- Expected type map_blocks_a 0
got type s: FStar.Seq.Base.seq a {FStar.Seq.Base.length s = 0}
- Try with --query_stats to get more details
- This query was retried due to the --proof_recovery option, yet it still
failed on all attempts.
- Also see: /__w/FStar/FStar/hacl-star/lib/Lib.Sequence.fst(267,50-267,54)
- Other related locations: /__w/FStar/FStar/hacl-star/lib/Lib.Sequence.fst(266,6-266,10)
|
|
dummy#L0
(250) * Warning 250:
- Error while extracting (["LowStar", "ImmutableBuffer"], "igcmalloc_of_list")
to KaRaMeL.
- Got an exception:Failure("Argument of FStar.Buffer.createL is not a list literal!")
|
|
dummy#L0
(250) * Warning 250:
- Error while extracting (["LowStar", "ImmutableBuffer"], "ialloca_of_list")
to KaRaMeL.
- Got an exception:Failure("Argument of FStar.Buffer.createL is not a list literal!")
|
|
dummy#L0
(250) * Warning 250:
- Error while extracting (["LowStar", "Monotonic", "Buffer"],
"mgcmalloc_of_list_partial") to KaRaMeL.
- Got an exception:Failure("Argument of FStar.Buffer.createL is not a list literal!")
|
|
dummy#L0
(250) * Warning 250:
- Error while extracting (["FStar", "List"], "index") to KaRaMeL.
- Got an exception:Failure("Internal error: name not found index\n")
|
|
dummy#L0
(250) * Warning 250:
- Error while extracting (["FStar", "List"], "filter_map") to KaRaMeL.
- Got an exception:Failure("Internal error: name not found filter_map_acc\n")
|
|
EverCrypt.Hash.fst#L288
(285) * Warning 285 at /__w/FStar/FStar/hacl-star/providers/evercrypt/fst/EverCrypt.Hash.fst(288,6-288,7):
- Module not found: M
|
|
EverCrypt.Hash.fst#L288
(285) * Warning 285 at /__w/FStar/FStar/hacl-star/providers/evercrypt/fst/EverCrypt.Hash.fst(288,6-288,7):
- Module not found: M
|
|
Hacl.Streaming.Blake2.Params.fst#L50
(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(50,11-50,15):
- Module not found: Core
|
|
Hacl.Streaming.Blake2.Params.fst#L50
(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(50,11-50,15):
- Module not found: Core
|
|
Lib.IntTypes.fsti#L988
(361) * Warning 361 at /__w/FStar/FStar/hacl-star/lib/Lib.IntTypes.fsti(988,0-988,21):
- Some #push-options have not been popped. Current depth is 1.
|
The logs for this run have expired and are no longer available.
Loading