search

dafny-lang / dafny

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

Fix: Dafny server API for counterexamples #5847

Open Dargones opened 1 month ago

Dargones commented 1 month ago

Description

Fixes https://github.com/dafny-lang/ide-vscode/issues/492

The language sever currently crushes when asking to display counterexamples. This is because #5013 changed the way counterexamples are represented but the IDE still expects the old representation. This PR fixes this. The IDE will now display any constraints that equate some literal to a variable/field/function application, etc. Here are some examples:

Screenshot 2024-10-21 at 4 39 26 PM

How has this been tested?

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

keyboardDrummer commented 3 weeks ago

I brought back the old tests, the ones that test .Variables, but they are failing. It seems the fix does not work.

MikaelMayer commented 3 weeks ago

@keyboardDrummer would you know how to fix the tests?

Dargones commented 3 weeks ago

@keyboardDrummer @MikaelMayer The old tests use an entirely different interface, so they won't help at all. The way to go is to edit existing tests manually one by one. I can do this but it might take me a few days.