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
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))
The text was updated successfully, but these errors were encountered:
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.The text was updated successfully, but these errors were encountered: