CrossHair icon indicating copy to clipboard operation
CrossHair copied to clipboard

Allow for the possibility for aliased top-level parameter values

Open pschanely opened this issue 4 years ago • 0 comments

One of CrossHair's strengths is that it models the heap and can detect a variety of "aliasing" problems - bugs caused by having the same object accessible through different paths of references. In this example, we can detect that two sub-lists might be the same list, which breaks the expected postcondition.

But CrossHair only does this for container contents, not for top-level parameters. For instance, it does not understand that the two parameters of this function could be the same list.

pschanely avatar Jan 27 '21 02:01 pschanely