Silicon and Carbon fail on AVLTree example translated by Chalice2Sil

[viper-admin]

Created by bitbucket user juhaszu on 2014-05-26 13:47
Last updated on 2019-08-28 09:42

All failures are for calling a method wihtin a constraining block, where the precondition quantifies on integers

Fails with the following error code:

The precondition of method AVLTreeNoderebalanceRight$ might not hold. Assertion (this$_20.AVLTreeNodeleft$ != null) ==> (forall k: Int :: true && k in this$_20.AVLTreeNodeleft$.AVLTreeNodekeys$ ==> (k < this$_20.AVLTreeNodekey$)) might not hold. (AVLTree.sil,899:9))

The precondition of method AVLTreeNoderebalanceLeft$ might not hold. Assertion (this$_17.AVLTreeNoderight$ != null) ==> (forall k: Int :: true && k in this$_17.AVLTreeNoderight$.AVLTreeNodekeys$ ==> (this$_17.AVLTreeNodekey$ < k)) might not hold. (AVLTree.sil,824:9))

The precondition of method AVLTreeNodeclose$ might not hold. Assertion (this$_16.AVLTreeNoderight$ != null) ==> (forall k: Int :: true && k in this$_16.AVLTreeNoderight$.AVLTreeNodekeys$ ==> (this$_16.AVLTreeNodekey$ < k)) might not hold. (AVLTree.sil,699:9))

Seems to be quantification related

---

Attachments:

• AVLTree.sil

[viper-admin]

@alexanderjsummers commented on 2019-08-28 09:42

The current example code doesn't parse; it also relies on constraining/fresh syntax which we agreed to remove. I suggest migrating this to a work-in-progress example

[viper-admin]

@alexanderjsummers on 2019-08-28 09:42:

• changed state from new to on hold
• edited the description