silicon
silicon copied to clipboard
viperproject
New objects and non-aliasing information
Created by @mschwerhoff on 2013-05-24 15:38 Last updated on 2019-03-02 22:27
When an object is created as v := new(), Silicon should be able to assert that every object that was reachable before calling new must be different from v. Silicon is currently only able to prove this non-equality between v and objects that were directly accessible, i.e., that were not "hidden" in a predicate. This is, because Silicon collects all reference-typed constants that are directly found in the store or in heap chunks.
In order to make Silicon (more) complete one could introduce "timestamps" that order references according to when they came into scope. The timestamp of a predicate would then be passed on to references that are unfolded from it. Another approach would be to adapt the approach of Spec#.
An example can be found in the test case Sil:basic/new.sil.
@mschwerhoff commented on 2015-03-03 11:53
https://github.com/viperproject/silicon/issues/105 was marked as a duplicate of this issue.
@mschwerhoff commented on 2015-10-26 18:53
https://github.com/viperproject/silicon/issues/173 was marked as a duplicate of this issue.
@mschwerhoff commented on 2016-03-30 14:22
Examples:
#!text
method test05(c1: Ref)
requires acc(pred_val(c1))
{
var c2: Ref; c2 := new(val)
unfold acc(pred_val(c1))
assert c2 != c1.val // FAILS
}
predicate abs(c: Ref)
function fun(c: Ref): Ref
requires acc(abs(c))
method test06(c1: Ref)
requires acc(abs(c1))
{
var c2: Ref; c2 := new(val)
assert c2 != fun(c1) // FAILS
}
@mschwerhoff commented on 2019-03-02 22:27
Directly related: https://github.com/viperproject/silicon/issues/344