Closed jennalwise closed 1 year ago
During my case-study, I discovered that silicon-gv is not producing a run time check for predicates that are being unfolded in an imprecise setting and are not in either heaps.
After looking at the code at https://github.com/gradual-verification/silicon-gv/blob/4445a12139cdbdeea75f94f35bbcd2b69478c8da/src/main/scala/rules/PredicateSupporter.scala#L183C37-L183C49 , we can see that there is a small bug where-in if (!chunkExisted && chunkExisted1) { should be if (!chunkExisted && !chunkExisted1) {. In its current form, run-time checks are only generated when the chunk isn't in the heap but is in the optimistic heap, when it really should generate checks only when it is in neither heap.
if (!chunkExisted && chunkExisted1) {
if (!chunkExisted && !chunkExisted1) {
Fixed here: https://github.com/gradual-verification/silicon-gv/commit/aaeb0dba4685786114710e7b3992a5a147a9ca95
jennalwise
commented
1 year ago
During my case-study, I discovered that silicon-gv is not producing a run time check for predicates that are being unfolded in an imprecise setting and are not in either heaps.
After looking at the code at https://github.com/gradual-verification/silicon-gv/blob/4445a12139cdbdeea75f94f35bbcd2b69478c8da/src/main/scala/rules/PredicateSupporter.scala#L183C37-L183C49 , we can see that there is a small bug where-in
if (!chunkExisted && chunkExisted1) {should beif (!chunkExisted && !chunkExisted1) {. In its current form, run-time checks are only generated when the chunk isn't in the heap but is in the optimistic heap, when it really should generate checks only when it is in neither heap.