search

viperproject / carbon

Verification-condition-generation-based verifier for the Viper intermediate verification language.
Mozilla Public License 2.0
30 stars 21 forks source link

Carbon does not manage to prove some assertions in AVLTree that proved in Chalice #18

Open viper-admin opened 10 years ago

viper-admin commented 10 years ago

Created by bitbucket user juhaszu on 2014-05-28 09:12 Last updated on 2015-11-25 16:17

This occurs also in Silicon - issue 90 - so might actually be a chalice2sil issue, although no immediate translation problem is visible

Error messages:

[info] TestAdditionalOutputError([assert.failed:assertion.false] Assert might fail. Assertion (forall k: Int :: true && k in r.AVLTreeNodekeys$ ==> (m.AVLTreeNodekeys$[0] < k)) m ight not hold. (AVLTree.sil,913:5)) [info] TestAdditionalOutputError([call.precondition:assertion.false] The precondition of method AVLTreeNodeclose$ might not hold. Assertion (forall k: Int :: true && k in this$_1 2.AVLTreeNodeleft$.AVLTreeNodekeys$ ==> (k < this$_12.AVLTreeNodekey$)) might not hold. (AVLTree.sil,908:9)) [info] TestAdditionalOutputError([call.precondition:assertion.false] The precondition of method AVLTreeNoderebalanceRight$ might not hold. Assertion (forall k: Int :: true && k i n this$_12.AVLTreeNodeleft$.AVLTreeNodekeys$ ==> (k < this$_12.AVLTreeNodekey$)) might not hold. (AVLTree.sil,902:9)) [info] TestAdditionalOutputError([assert.failed:assertion.false] Assert might fail. Assertion (forall k: Int :: true && k in r.AVLTreeNodekeys$ ==> (k < m.AVLTreeNodekeys$[0])) m ight not hold. (AVLTree.sil,835:5)) [info] TestAdditionalOutputError([call.precondition:assertion.false] The precondition of method AVLTreeNodeclose$ might not hold. Assertion (forall k: Int :: true && k in this$_1 1.AVLTreeNoderight$.AVLTreeNodekeys$ ==> (this$_11.AVLTreeNodekey$ < k)) might not hold. (AVLTree.sil,831:9)) [info] TestAdditionalOutputError([call.precondition:assertion.false] The precondition of method AVLTreeNoderebalanceLeft$ might not hold. Assertion (forall k: Int :: true && k in this$_11.AVLTreeNoderight$.AVLTreeNodekeys$ ==> (this$_11.AVLTreeNodekey$ < k)) might not hold. (AVLTree.sil,826:9)) [info] TestAdditionalOutputError([postcondition.violated:assertion.false] Postcondition of AVLTreeNoderemove$ might not hold. Assertion !k in r.AVLTreeNodekeys$ might not hold. ( AVLTree.sil,635:11)) [info] TestAdditionalOutputError([call.precondition:assertion.false] The precondition of method AVLTreeNodeclose$ might not hold. Assertion (forall k: Int :: true && k in r.AVLTr eeNoderight$.AVLTreeNodekeys$ ==> (r.AVLTreeNodekey$ < k)) might not hold. (AVLTree.sil,700:9)) [info] TestAdditionalOutputError([call.precondition:assertion.false] The precondition of method AVLTreeNodeclose$ might not hold. Assertion (forall k: Int :: true && k in r.AVLTr eeNodeleft$.AVLTreeNodekeys$ ==> (k < r.AVLTreeNodekey$)) might not hold. (AVLTree.sil,700:9)) (AnnotationBasedTestSuite.scala:51) [info] + Verifier used: carbon 1.0. [info] + Time required: 901 msec (parse), 1.03 sec (typecheck), 0 msec (translate), 1105.40 sec (verify).

Attachments:

viper-admin commented 9 years ago

@alexanderjsummers on 2015-11-25 16:17:

  • changed attachment from (none) to AVLTree.sil