False negative for postconditions with this or #n in their expression

[mernst]

Commit d70dd74 introduces a false negative, in its use of CFAbstractStore.insertValuePermitNondeterministic(). Consider this test case:

import java.util.Optional;

class PureGetterTest2 {

  Optional<String> otherOptional() {
    if (Math.random() < 0.5) {
      return Optional.ofNullable(null);
    } else {
      return Optional.of("hello world");
    }
  }

  void foo() {
    if (otherOptional().isPresent()) {
      // BUG: no "method.invocation" error is issued here.
      otherOptional().get();
    }
  }
}

In a postcondition like @EnsuresPresent("field.method()"), it is correct to permit method() in the expression even if it is not @Deterministic. However, in a postcondition like @EnsuresPresent("#1.method()"), it should not be permitted to substitute in an argument that is not @Deterministic.