search

ggrov / tacny

Tactics for the Dafny program verifier
3 stars 2 forks source link

Extension Crashing when running DARe #45

Open LonMcGregor opened 8 years ago

LonMcGregor commented 8 years ago
LonMcGregor commented 8 years ago

(extension) Regarding assert not tagged - This is due to a comment being on the end of the line - detection of this doesn't exist yet

dc950 commented 7 years ago

The cause of the first issue regarding Dijkstra.dfy is due to an exception occurring in the boogie translator meaning the methods containing errors are not flag. Possible solution is to identify when this occurs, reinsert everything that was removed iteration and to try and remove each item individually.

ggrov commented 7 years ago

Are these exceptions a result of changes made to the AST (i.a. are result of what we are doing in the DARe tool)? Is this the reason why so many of the programs in the Dafny test suite/library fails?

dc950 commented 7 years ago

Most of the DARe bugs are fixed now. I will run the logger again tomorrow to get new data and see if any new bugs have cropped up. I also came across another bug that I've added at the bottom and will look into.

LonMcGregor commented 7 years ago

On the latest commit i've pushed to refactoring, bd91f59, there seems to be a problem where DARe is saying programs are not valid even though they are.

Looking into this, it's throwing a FileNotFoundException @ Removers.cs:28. Even though the files do exist.

ggrov commented 7 years ago

Duncan, could you have a look at it? (May also be the source that so many programs are considered invalid in the data set?)

ggrov commented 7 years ago

I get the same problem (or at least it fails) when I use the simple demo I've used at the Dafny course.

dc950 commented 7 years ago

I've been unable to replicate the issue Leon is referring to. If there is FileNotFoundException there its probably to do with the files that dafny needs to run. I tried completely re-cloning the repository, building boogie, building dafny then running the extension and it still would run fine. I'm also fairly certain this has nothing to do with the failing programs in the data set.

I did, however, come across another reason it was crashing in the extension: line 434 in DeadAnnotationTagger.cs will throw an InvalidOperationException when the results list is empty as it is trying to access the first result.

LonMcGregor commented 7 years ago

I think the invalid programs are more due to dafny itself than the DARe extension.

I'll have another try later today with re-cloning the repo, and seeing if it was some missing files.

ggrov commented 7 years ago

I very much doubt this for my case (see email). It verifies as normal but dare fails. It also used to workfor previous versions.

ggrov commented 7 years ago

Yuhui, could this have anything to do with your changes to the resolver?

LonMcGregor commented 7 years ago

I've just re-clones the repo, and built it. The extension now works as expected. So i'm not sure whats causing the problem.

ggrov commented 7 years ago

Me too - and the example program works fine for me too.

lyhlbyl commented 7 years ago

It is not quite likely, as there is no tactic call in those examples. Tacny won't be triggered.