search

viperproject / carbon

Verification-condition-generation-based verifier for the Viper intermediate verification language.
Mozilla Public License 2.0
30 stars 20 forks source link

Examples without proper triggers don't verify #91

Open viper-admin opened 8 years ago

viper-admin commented 8 years ago

Created by @alexanderjsummers on 2016-01-13 17:09 Last updated on 2018-06-09 12:08

Because of a lack of appropriate triggers (at least for composite.sil), the examples composite.sil and bsearch.sil don't verify, and consume a lot of memory. We should consider whether to improve the specs or remove the examples. They might also serve as interesting cases for trigger-generation and matching-loop debugging.

See also: https://github.com/viperproject/silicon/issues/74 https://github.com/viperproject/silicon/issues/76

viper-admin commented 8 years ago

@alexanderjsummers on 2016-01-13 17:14:

  • edited the title
  • edited the description
  • changed priority from trivial to minor
viper-admin commented 6 years ago

@mschwerhoff commented on 2018-06-09 12:08

I just investigated quantifiedpermissions/sequences/bsearch.sil and found four genuine errors (two programming errors, two specification errors) that explain why the originally reported code doesn't verify. I kept the original code, but added triggers. Moreover, I added three fixed variants of the original example.

Both Carbon and Silicon now behave as expected for the updated test file. If you think that the original code without triggers would be worth keeping, e.g. for testing the axiom profiler, then you'll have to get the old code from Mercurial's history (and save it separately). I hope that's OK with you.

The other example (composite.sil) still needs investigation. Maybe Nils Becker could have a look at it.