Postconditions are checked without assuming that contracts are wellformed

[viper-admin]

Created by @vakaras on 2015-07-29 13:01 Last updated on 2015-11-18 09:24

In the following Silver example, Silicon checks if postcondition is established without checking that tje contract is well formed and reports a different error than Carbon.

#!Silver

field x: Int

function postFunction(this: Ref): Int
  requires this != null
  //:: ExpectedOutput(postcondition.violated:assertion.false)
  //:: MissingOutput(postcondition.violated:assertion.false, /Silicon/issue/162/)
  //:: UnexpectedOutput(postcondition.violated:insufficient.permission, /Silicon/issue/162/)
  ensures this.x == 0
{
  1
}

[viper-admin]

@alexanderjsummers on 2015-10-02 10:05:

• edited the description

[viper-admin]

@mschwerhoff commented on 2015-11-18 09:24

Since Silicon represents permissions as heap chunks, it is difficult for Silicon to avoid reporting insufficient permissions when checking the postcondition:

1. Silicon checks the function contract for well-definedness, which will fail due to insufficient permission to this.x
2. Silicon inhales the precondition, which does not provide permissions to this.x; consequently, no heap chunk for this.x is produced
3. Silicon consumes the postcondition, which fails because permissions to this.x are not available

If Carbon reported insufficient permissions, it can simply continue the verification under the additional assumption that sufficient permissions were available, i.e. H[this, x] > none. For Silicon, this is in general not (so easily) possible (without causing spurious errors afterwards) because it would have to add a heap chunk, sum up all potential permissions in the heap (which requires accounting for aliasing and permissions inside predicates), and assume that the sum is non-none.

[viper-admin]

@mschwerhoff commented on 2015-11-18 09:24

Duplicate of https://github.com/viperproject/silicon/issues/34.

[viper-admin]

@mschwerhoff on 2015-11-18 09:24:

• changed state from new to duplicate

[viper-admin]

@mschwerhoff commented on 2015-11-18 12:31

https://github.com/viperproject/silicon/issues/144 was marked as a duplicate of this issue.

[viper-admin]

@mschwerhoff commented on 2015-11-18 12:48

https://github.com/viperproject/silicon/issues/152 was marked as a duplicate of this issue.