search

viperproject / chalice2silver

Other
0 stars 0 forks source link

Test internal-bug-10.chalice fails only when executed on AST generated by Chalice2Silver #67

Open viper-admin opened 9 years ago

viper-admin commented 9 years ago

Created by @vakaras on 2015-06-30 12:10

Chalice2Silver test chaliceSuite/regressions/internal-bug-10.chalice fails when Silicon is used as a verifier. Silicon fails to show that the postcondition of the method add holds:

#!Chalice

  method add(x: int)
    requires valid;
    ensures valid;
    ensures size() == old(size())+1;
    ensures (forall y:int :: contains(y)==(old(contains(y)) || x==y));  // Silicon issue 113
  {
    unfold this.valid;
    if(next==null) {
      var n : Node;
      n := new Node;
      call n.init(x);
      next := n;
    } else {
      call next.add(x);
    }
    fold this.valid;
  }

Error:

[info] The following output occurred during testing, but should not have according to the test annotations:
[info]   [postcondition.violated:assertion.false] [postcondition.violated:assertion.false] Postcondition of Nodeadd$ might not hold. Assertion (forall y: Int :: true ==> (Nodecontains$(this$_2, y) == old(Nodecontains$(this$_2, y)) || (x == y))) might not hold. (internal-bug-10.chalice,22:14) (AnnotationBasedTestSuite.scala:59)

However, when Silicon is executed on Silver program directly (test all/chalice/internal-bug-14.sil), the program is verified successfully. Note that Carbon fails consistently.

Related issues:

Attachments: