make the plugin work #31
Annotations
4 errors and 11 warnings
|
Everparse CI:
out.fail.batch/FAILAllBytesCompose.fst#L81
(66) * Error 66 at out.fail.batch/FAILAllBytesCompose.fst(81,6-87,85):
- Failed to resolve implicit argument ?57
of type Prims.bool
introduced for Instantiating implicit argument
|
|
Everparse CI:
out.fail.batch/FAILAllBytesCompose.fst#L83
(12) * Error 12 at out.fail.batch/FAILAllBytesCompose.fst(83,10-85,52):
- Expected type
EverParse3d.Interpreter.typ (*?u58*)
_
(*?u59*)
_
(*?u60*)
_
(*?u61*)
_
(*?u62*)
_
(*?u63*)
_
but
EverParse3d.Interpreter.T_with_comment "should_not_be_here"
(EverParse3d.Interpreter.T_denoted "should_not_be_here" dtyp__test1)
"Validating field should_not_be_here"
has type
EverParse3d.Interpreter.typ kind__test1
EverParse3d.Interpreter.Trivial
EverParse3d.Interpreter.Trivial
EverParse3d.Interpreter.Trivial
false
false
|
|
Everparse CI:
ulib/Prims.fst#L459
(19) * Error 19 at out.fail.batch/FAILAllBytesNotLast.fst(14,2-34,16):
- Could not prove goal #1
- The SMT solver could not prove the query. Use --query_stats for more
details.
- See also ulib/Prims.fst(459,77-459,89)
|
|
Everparse CI:
out.fail.batch/FAILAllBytesNotLast.fst#L43
(189) * Error 189 at out.fail.batch/FAILAllBytesNotLast.fst(43,53-43,67):
- Expected expression of type
EverParse3d.Kinds.parser_kind (*?u58*)
_
EverParse3d.Kinds.WeakKindStrongPrefix
got expression EverParse3d.Kinds.kind_all_bytes
of type
EverParse3d.Kinds.parser_kind false
EverParse3d.Kinds.WeakKindConsumesAll
|
|
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
Everparse CI:
dummy#L1
(274) * Warning 274:
- Implicitly opening namespace 'cbor.pulse.api.det.' shadows module 'c'
in file "/__w/everparse/everparse/karamel/krmllib/C.fst".
- Rename "/__w/everparse/everparse/karamel/krmllib/C.fst" to avoid conflicts.
|
|
Everparse CI:
dummy#L1
(361) * Warning 361 at Options.fst(594,0-597,15):
- Some #push-options have not been popped. Current depth is 1.
|
|
Everparse CI:
dummy#L1
(274) * Warning 274:
- Implicitly opening namespace 'cbor.pulse.api.det.' shadows module 'c'
in file "/__w/everparse/everparse/karamel/krmllib/C.fst".
- Rename "/__w/everparse/everparse/karamel/krmllib/C.fst" to avoid conflicts.
|
|
Everparse CI:
dummy#L1
(242) * Warning 242 at Ast.fst(395,0-429,18):
- Definitions of inner let-rec seq and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: Ast.fst(397,12-397,15)
|
|
Everparse CI:
dummy#L1
(242) * Warning 242 at Ast.fst(1251,0-1256,14):
- Definitions of inner let-rec seq and its enclosing top-level letbinding are
not encoded to the solver, you will only be able to reason with their types
- Also see: Ast.fst(397,12-397,15)
|
|
Everparse CI:
dummy#L1
(361) * Warning 361 at src/lowparse/LowParse.BitFields.fst(1276,0-1276,29):
- Some #push-options have not been popped. Current depth is 1.
|
|
Everparse CI:
Target.fst#L958
(337) * Warning 337 at Target.fst(958,28-958,29):
- 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 '@'.
|
|
Everparse CI:
Target.fst#L1051
(337) * Warning 337 at Target.fst(1051,69-1051,70):
- 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 '@'.
|
|
Everparse CI:
Target.fst#L1395
(337) * Warning 337 at Target.fst(1395,54-1395,55):
- 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 '@'.
|
|
Everparse CI:
dummy#L1
(361) * Warning 361 at Target.fst(1477,0-1501,9):
- Some #push-options have not been popped. Current depth is 1.
|
Loading