EverParse+Pulse: Verified parsing and serialization with separation logic #36
Annotations
10 warnings
|
Build a package:
FStar.TSet.fst#L27
(318) * Warning 318 at C:\gh\2\_work\everparse\everparse\fstar\ulib\FStar.TSet.fst(27,4-27,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.
|
|
Build a package:
FStar.UInt.fsti#L435
(271) * Warning 271 at C:\gh\2\_work\everparse\everparse\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
|
|
Build a package:
FStar.UInt.fsti#L435
(271) * Warning 271 at C:\gh\2\_work\everparse\everparse\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 C:\gh\2\_work\everparse\everparse\fstar\ulib\FStar.UInt.fsti(435,8-435,51)
|
|
Build a package:
FStar.UInt.fsti#L435
(271) * Warning 271 at C:\gh\2\_work\everparse\everparse\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
|
|
Build a package:
dummy#L1
(242) * Warning 242 at c:\gh\2\_work\everparse\everparse\fstar\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: c:\gh\2\_work\everparse\everparse\fstar\ulib\FStar.WellFounded.fst(86,12-86,15)
|
|
Build a package:
dummy#L1
(242) * Warning 242 at c:\gh\2\_work\everparse\everparse\fstar\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: c:\gh\2\_work\everparse\everparse\fstar\ulib\FStar.WellFounded.fst(126,12-126,15)
|
|
Build a package:
FStar.GhostSet.fst#L23
(318) * Warning 318 at c:\gh\2\_work\everparse\everparse\fstar\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.
|
|
Build a package:
FStar.TSet.fst#L27
(318) * Warning 318 at c:\gh\2\_work\everparse\everparse\fstar\ulib\FStar.TSet.fst(27,4-27,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.
|
|
Build a package:
FStar.GSet.fst#L23
(318) * Warning 318 at c:\gh\2\_work\everparse\everparse\fstar\ulib\FStar.GSet.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.
|
|
Build a package:
FStar.MST.fst#L222
(330) * Warning 330 at c:\gh\2\_work\everparse\everparse\fstar\ulib\experimental\FStar.MST.fst(222,43-222,55):
- Polymonadic binds ((DIV, MSTATE) |> MSTATE) in this case) is an experimental
feature;it is subject to some redesign in the future. Please keep us
informed (on github etc.) about how you are using it
|
Loading