search

boogie-org / boogie-friends

Tools for interacting with Boogie
45 stars 13 forks source link

When using `include`, helpful "this is the precondition that might not hold" information is missing from flycheck errors #5

Open wilcoxjay opened 8 years ago

wilcoxjay commented 8 years ago

Consider a that has two files A.dfy and B.dfy. A contains library declarations, which B uses via the include directive. 

// A.dfy
method foo(x: int)
  requires x > 0
  requires x % 2 == 0
{
} 
// B.dfy
include "A.dfy"

method bar()
{
  foo(0);
}

Then flycheck will report that a precondition of foo is violated, but it won't tell you which one. This gets annoying when there are many preconditions, and I am reduced to copy-pasting the contents of A into B or to running dafny on the command line.

Would it be possible to get this information into flycheck, preferably including the ability to jump to the precondition, just like when the caller and callee are in the same file?

cpitclaudel commented 8 years ago

Thanks for that report! That's indeed annoying :/ C-c C-c is probably a half-decent workaround, as long as your files are quick to process.

The issue is within the Dafny server implementation (not within the Emacs mode), and I need to debug that. That could take a while; I may have time next week-end though.