CrossHair
CrossHair copied to clipboard
Allow for the possibility for aliased top-level parameter values
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.