Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Better "See also" targeting #36

Open
parno opened this issue Mar 8, 2019 · 0 comments
Open

Better "See also" targeting #36

parno opened this issue Mar 8, 2019 · 0 comments

Comments

@parno
Copy link
Member

parno commented Mar 8, 2019

Currently, Vale/F* reports most verification errors in terms of the original Vale source code. However, the treatment of the "See also" reporting is current rather odd. In the example below, the "Also see" parenthetical reported with the error message points to line 0 column 0. However, the "see also" for the corresponding warning contains useful line and column information. Unfortunately, that information points to the generated F* file X64.AESGCM.fst instead of the precondition on the original Vale procedure. Fixing either one or both of these limitations would help improve the Vale debug cycle.

(0,0-0,0): (Warning 252) ***** PRECONDITION NOT MET AT line 3168 column 16 of file ./code/thirdPartyPorts/OpenSSL/aes/X64.AESGCM.vaf ***** (see also obj/code/thirdPartyPorts/OpenSSL/aes/X64.AESGCM.fst(310,28-310,68))
obj/code/thirdPartyPorts/OpenSSL/aes/X64.AESGCM.fst(886,2-909,16): (Error 19) ***** PRECONDITION NOT MET AT line 3168 column 16 of file ./code/thirdPartyPorts/OpenSSL/aes/X64.AESGCM.vaf ***** (Also see: (0,0-0,0))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant