You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
rightfully fails because [:consume-all] removes the strong prefix property of its parser. But right now, EverParse fails with F* Error 19, i.e. a Z3 failure to prove that field a above with [:consume-all] has the strong prefix property. While expected, this is not palatable to the user.
In fact, as designed in #116, [:consume-all] is meant to be used only as the last field of a struct. Thus, I believe this should be checked syntactically (or, at worst, at the level of the 3D AST) and EverParse should reject uses of [:consume-all] for struct fields other than the last one, with a suitable error message.
The text was updated successfully, but these errors were encountered:
Reported by @Smfakhoury
The following 3D specification:
rightfully fails because
[:consume-all]
removes the strong prefix property of its parser. But right now, EverParse fails with F* Error 19, i.e. a Z3 failure to prove that fielda
above with[:consume-all]
has the strong prefix property. While expected, this is not palatable to the user.In fact, as designed in #116,
[:consume-all]
is meant to be used only as the last field of a struct. Thus, I believe this should be checked syntactically (or, at worst, at the level of the 3D AST) and EverParse should reject uses of[:consume-all]
for struct fields other than the last one, with a suitable error message.The text was updated successfully, but these errors were encountered: