Insufficient Permissions in Function Precondition Not Reported

[ArquintL]

The following program verifies with the option --enableMoreCompleteExhale but should not (and does not verify if this option is dropped).

Method client2_pkg_F only has half a permission to the predicate instance SomePredicate_pkg_F and calls function getter_pkg_F in its postcondition. However, this function requires write permissions to the predicate instance.

field val$_Int: Int

function getter_pkg_F(param_pkg_V0: Ref): Int
  requires acc(SomePredicate_pkg_F(param_pkg_V0), write)
{
  (unfolding acc(SomePredicate_pkg_F(param_pkg_V0), write) in param_pkg_V0.val$_Int)
}

predicate SomePredicate_pkg_F(param_pkg_V0: Ref) {
  true && acc(param_pkg_V0.val$_Int, write)
}

method client2_pkg_F(param_pkg_V0: Ref) returns (res_pkg_V0: Int)
  requires acc(SomePredicate_pkg_F(param_pkg_V0), 1 / 2)
  ensures acc(SomePredicate_pkg_F(param_pkg_V0), 1 / 2)
  ensures res_pkg_V0 == getter_pkg_F(param_pkg_V0)

[mschwerhoff]

Thanks for reporting this, I'll take a look. Please be aware that --enableMoreCompleteExhale is not considered "production-ready", so bugs are somewhat expected.

[marcoeilers]

This was fixed in #682.