search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.89k stars 256 forks source link

Dafny may report errors on code inside a doo file (bad) using malformed snippets (also bad) #4716

Open keyboardDrummer opened 11 months ago

keyboardDrummer commented 11 months ago

Running dafny test on a .doo file generated from a method {:test} Foo(x: int, y: int) {} gives the following error:

  |
5 | ͙ލ)�0
         '�����PHkB��X'�i�W,�ՄZv�h�W��_~1gC��o�mx�����D��kP#^ZWK;�8�    �)program�YkS�8�ί��
                                                                                           �R�/)dg��ng߅�퇶�q<M��pY�ϑ%Y��aagJI��syΣ�#��������ck����W����:M��p�����E2'���f��-��s:2�j�����2G�   ���p�[��8ۤ4#g�N����?����d�2�*�:��'�$h${��e�ܜ�Rf y
  |                ^^^^^^^^^^^^^^

build/stdlibexamples.doo(5,15): Error: Methods with the :test attribute may not have input arguments
keyboardDrummer commented 5 months ago

I'm not sure what the right solution is. For these particular errors we could move them to resolution phase to prevent this doo file from being generated, but that does not provide a generic mechanism for preventing this issue.

Another change we could make it in the snippet generation, to detect that the location is inside a doo file and either generate a good looking snippet or no snippet at all.