GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
438 stars 63 forks source link

[Heapster] Fix arrays example #1421

Open m-yac opened 3 years ago

m-yac commented 3 years ago

There are at least two things broken with the arrays example in heapster-saw/examples.

m-yac commented 3 years ago

As of #1484, the proof of no_errors_sum_inc_ptr is broken as well.

eddywestbrook commented 3 years ago

I fixed the sum_2d example so that it now type-checks in the latest version of #1484. The issue was that sum_2d iterates over an array of arrays, and at the end of each iteration, a different sub-array is being borrowed from the overall array of arrays. So, when widening was being called, it would see two different permissions for sub-arrays that were unrelated. This was causing "undetermined variable" errors. So, instead, I fixed widening to drop any undetermined variables, and it looks like that fixed the type error. I haven't looked into the other issues with that function yet, though, but those should probably be the subject of this PR and not #1484.