Merge pull request #561 from fabianboesiger/master

Rename range function in Viper code generated by Nagini frontend

Author: mschwerhoff

src/test/resources/frontends/nagini/testsarpverificationtest_rd_quantified.py.vpr

@@ -84,7 +84,7 @@ domain PyType {
 
   unique function slice(): PyType
 
-  unique function range(): PyType
+  unique function py_range(): PyType
 
   unique function Iterator_basic(): PyType
 
@@ -274,8 +274,8 @@ domain PyType {
     extends_(slice(), object()) && get_basic(slice()) == slice()
   }
 
-  axiom subtype_range {
-    extends_(range(), object()) && get_basic(range()) == range()
+  axiom subtype_py_range {
+    extends_(py_range(), object()) && get_basic(py_range()) == py_range()
   }
 
   axiom subtype_Iterator {

src/test/resources/frontends/nagini/testsfunctionalverificationexamplescav_example.py.vpr

@@ -84,7 +84,7 @@ domain PyType {
 
   unique function slice(): PyType
 
-  unique function range(): PyType
+  unique function py_range(): PyType
 
   unique function Iterator_basic(): PyType
 
@@ -278,8 +278,8 @@ domain PyType {
     extends_(slice(), object()) && get_basic(slice()) == slice()
   }
 
-  axiom subtype_range {
-    extends_(range(), object()) && get_basic(range()) == range()
+  axiom subtype_py_range {
+    extends_(py_range(), object()) && get_basic(py_range()) == py_range()
   }
 
   axiom subtype_Iterator {

src/test/resources/frontends/nagini/testsfunctionalverificationexamplesiap_bst.py.vpr

@@ -84,7 +84,7 @@ domain PyType {
 
   unique function slice(): PyType
 
-  unique function range(): PyType
+  unique function py_range(): PyType
 
   unique function Iterator_basic(): PyType
 
@@ -278,8 +278,8 @@ domain PyType {
     extends_(slice(), object()) && get_basic(slice()) == slice()
   }
 
-  axiom subtype_range {
-    extends_(range(), object()) && get_basic(range()) == range()
+  axiom subtype_py_range {
+    extends_(py_range(), object()) && get_basic(py_range()) == py_range()
   }
 
   axiom subtype_Iterator {

src/test/resources/frontends/nagini/testsfunctionalverificationexamplesparkinson_recell.py.vpr

@@ -84,7 +84,7 @@ domain PyType {
 
   unique function slice(): PyType
 
-  unique function range(): PyType
+  unique function py_range(): PyType
 
   unique function Iterator_basic(): PyType
 
@@ -278,8 +278,8 @@ domain PyType {
     extends_(slice(), object()) && get_basic(slice()) == slice()
   }
 
-  axiom subtype_range {
-    extends_(range(), object()) && get_basic(range()) == range()
+  axiom subtype_py_range {
+    extends_(py_range(), object()) && get_basic(py_range()) == py_range()
   }
 
   axiom subtype_Iterator {

src/test/resources/frontends/nagini/testsfunctionalverificationexamplesrosetta_qsort.py.vpr

@@ -84,7 +84,7 @@ domain PyType {
 
   unique function slice(): PyType
 
-  unique function range(): PyType
+  unique function py_range(): PyType
 
   unique function Iterator_basic(): PyType
 
@@ -274,8 +274,8 @@ domain PyType {
     extends_(slice(), object()) && get_basic(slice()) == slice()
   }
 
-  axiom subtype_range {
-    extends_(range(), object()) && get_basic(range()) == range()
+  axiom subtype_py_range {
+    extends_(py_range(), object()) && get_basic(py_range()) == py_range()
   }
 
   axiom subtype_Iterator {

src/test/resources/frontends/nagini/testsfunctionalverificationexamplestest_student_enroll_preds.py.vpr

@@ -84,7 +84,7 @@ domain PyType {
 
   unique function slice(): PyType
 
-  unique function range(): PyType
+  unique function py_range(): PyType
 
   unique function Iterator_basic(): PyType
 
@@ -278,8 +278,8 @@ domain PyType {
     extends_(slice(), object()) && get_basic(slice()) == slice()
   }
 
-  axiom subtype_range {
-    extends_(range(), object()) && get_basic(range()) == range()
+  axiom subtype_py_range {
+    extends_(py_range(), object()) && get_basic(py_range()) == py_range()
   }
 
   axiom subtype_Iterator {

src/test/resources/frontends/nagini/testsfunctionalverificationissues00017.py.vpr

@@ -84,7 +84,7 @@ domain PyType {
 
   unique function slice(): PyType
 
-  unique function range(): PyType
+  unique function py_range(): PyType
 
   unique function Iterator_basic(): PyType
 
@@ -274,8 +274,8 @@ domain PyType {
     extends_(slice(), object()) && get_basic(slice()) == slice()
   }
 
-  axiom subtype_range {
-    extends_(range(), object()) && get_basic(range()) == range()
+  axiom subtype_py_range {
+    extends_(py_range(), object()) && get_basic(py_range()) == py_range()
   }
 
   axiom subtype_Iterator {
@@ -489,33 +489,33 @@ function Measure$check(map: Seq[Measure$], key: Ref, value: Int): Bool
   (forall m: Measure$ :: { (m in map) } (m in map) ==> Measure$guard(m) && Measure$key(m) == key ==> Measure$value(m) > value)
 }
 
-function range___create__(start: Int, stop: Int, ctr: Int): Ref
+function py_range___create__(start: Int, stop: Int, ctr: Int): Ref
   requires stop >= start
-  ensures range___val__(result) == [start..stop)
-  ensures range___start__(result) == start
-  ensures range___stop__(result) == stop
-  ensures typeof(result) == range()
+  ensures py_range___val__(result) == [start..stop)
+  ensures py_range___start__(result) == start
+  ensures py_range___stop__(result) == stop
+  ensures typeof(result) == py_range()
 
 
-function range___val__(self: Ref): Seq[Int]
+function py_range___val__(self: Ref): Seq[Int]
 
 
-function range___start__(self: Ref): Int
+function py_range___start__(self: Ref): Int
 
 
-function range___stop__(self: Ref): Int
+function py_range___stop__(self: Ref): Int
 
 
-function range___len__(self: Ref): Int
-  requires issubtype(typeof(self), range())
-  ensures result == |range___val__(self)|
+function py_range___len__(self: Ref): Int
+  requires issubtype(typeof(self), py_range())
+  ensures result == |py_range___val__(self)|
 
 
-function range___sil_seq__(self: Ref): Seq[Ref]
-  requires issubtype(typeof(self), range())
-  ensures |result| == range___len__(self)
-  ensures (forall i: Int :: { result[i] } i >= 0 && i < |range___val__(self)| ==> result[i] == __prim__int___box__(range___val__(self)[i]))
-  ensures (forall i: Ref :: { (i in result) } (i in result) == (typeof(i) == int() && (int___unbox__(i) in range___val__(self))))
+function py_range___sil_seq__(self: Ref): Seq[Ref]
+  requires issubtype(typeof(self), py_range())
+  ensures |result| == py_range___len__(self)
+  ensures (forall i: Int :: { result[i] } i >= 0 && i < |py_range___val__(self)| ==> result[i] == __prim__int___box__(py_range___val__(self)[i]))
+  ensures (forall i: Ref :: { (i in result) } (i in result) == (typeof(i) == int() && (int___unbox__(i) in py_range___val__(self))))
 
 
 function str___len__(self: Ref): Int
@@ -594,13 +594,13 @@ method test_nested_forall(_cthread_157: Ref, _caller_measures_157: Seq[Measure$]
   var _method_measures_157: Seq[Measure$]
   _method_measures_157 := Seq[Measure$]()
   _err := null
-  a_1 := range___create__(1, 3, 0)
+  a_1 := py_range___create__(1, 3, 0)
   inhale _isDefined(3235681)
-  b_0 := range___create__(1, 6, 1)
+  b_0 := py_range___create__(1, 6, 1)
   inhale _isDefined(3170146)
-  c := range___create__(4, 7, 2)
+  c := py_range___create__(4, 7, 2)
   inhale _isDefined(99)
-  assert (forall lambda17_21$x: Ref :: { (lambda17_21$x in range___sil_seq__(_checkDefined(a_1, 3235681))) } issubtype(typeof(lambda17_21$x), int()) ==> (lambda17_21$x in range___sil_seq__(_checkDefined(a_1, 3235681))) ==> (forall lambda17_42$y: Ref :: { (lambda17_42$y in range___sil_seq__(_checkDefined(b_0, 3170146))) } issubtype(typeof(lambda17_42$y), int()) ==> (lambda17_42$y in range___sil_seq__(_checkDefined(b_0, 3170146))) ==> int___eq__(lambda17_21$x, lambda17_42$y) ==> (forall lambda17_79$x: Ref :: { (lambda17_79$x in range___sil_seq__(_checkDefined(c, 99))) } issubtype(typeof(lambda17_79$x), int()) ==> (lambda17_79$x in range___sil_seq__(_checkDefined(c, 99))) ==> int___gt__(int___unbox__(lambda17_79$x), int___unbox__(lambda17_42$y)))))
+  assert (forall lambda17_21$x: Ref :: { (lambda17_21$x in py_range___sil_seq__(_checkDefined(a_1, 3235681))) } issubtype(typeof(lambda17_21$x), int()) ==> (lambda17_21$x in py_range___sil_seq__(_checkDefined(a_1, 3235681))) ==> (forall lambda17_42$y: Ref :: { (lambda17_42$y in py_range___sil_seq__(_checkDefined(b_0, 3170146))) } issubtype(typeof(lambda17_42$y), int()) ==> (lambda17_42$y in py_range___sil_seq__(_checkDefined(b_0, 3170146))) ==> int___eq__(lambda17_21$x, lambda17_42$y) ==> (forall lambda17_79$x: Ref :: { (lambda17_79$x in py_range___sil_seq__(_checkDefined(c, 99))) } issubtype(typeof(lambda17_79$x), int()) ==> (lambda17_79$x in py_range___sil_seq__(_checkDefined(c, 99))) ==> int___gt__(int___unbox__(lambda17_79$x), int___unbox__(lambda17_42$y)))))
   goto __end
   label __end
 }
@@ -620,13 +620,13 @@ method test_nested_forall_2(_cthread_158: Ref, _caller_measures_158: Seq[Measure
   var _method_measures_158: Seq[Measure$]
   _method_measures_158 := Seq[Measure$]()
   _err := null
-  a_2 := range___create__(1, 5, 3)
+  a_2 := py_range___create__(1, 5, 3)
   inhale _isDefined(3301217)
-  b_1 := range___create__(1, 6, 4)
+  b_1 := py_range___create__(1, 6, 4)
   inhale _isDefined(3235682)
-  c_0 := range___create__(4, 7, 5)
+  c_0 := py_range___create__(4, 7, 5)
   inhale _isDefined(3170147)
-  assert (forall lambda25_21$x: Ref :: { (lambda25_21$x in range___sil_seq__(_checkDefined(a_2, 3301217))) } issubtype(typeof(lambda25_21$x), int()) ==> (lambda25_21$x in range___sil_seq__(_checkDefined(a_2, 3301217))) ==> (forall lambda25_42$y: Ref :: { (lambda25_42$y in range___sil_seq__(_checkDefined(b_1, 3235682))) } issubtype(typeof(lambda25_42$y), int()) ==> (lambda25_42$y in range___sil_seq__(_checkDefined(b_1, 3235682))) ==> int___eq__(lambda25_21$x, lambda25_42$y) ==> (forall lambda25_79$x: Ref :: { (lambda25_79$x in range___sil_seq__(_checkDefined(c_0, 3170147))) } issubtype(typeof(lambda25_79$x), int()) ==> (lambda25_79$x in range___sil_seq__(_checkDefined(c_0, 3170147))) ==> int___gt__(int___unbox__(lambda25_79$x), int___unbox__(lambda25_42$y)))))
+  assert (forall lambda25_21$x: Ref :: { (lambda25_21$x in py_range___sil_seq__(_checkDefined(a_2, 3301217))) } issubtype(typeof(lambda25_21$x), int()) ==> (lambda25_21$x in py_range___sil_seq__(_checkDefined(a_2, 3301217))) ==> (forall lambda25_42$y: Ref :: { (lambda25_42$y in py_range___sil_seq__(_checkDefined(b_1, 3235682))) } issubtype(typeof(lambda25_42$y), int()) ==> (lambda25_42$y in py_range___sil_seq__(_checkDefined(b_1, 3235682))) ==> int___eq__(lambda25_21$x, lambda25_42$y) ==> (forall lambda25_79$x: Ref :: { (lambda25_79$x in py_range___sil_seq__(_checkDefined(c_0, 3170147))) } issubtype(typeof(lambda25_79$x), int()) ==> (lambda25_79$x in py_range___sil_seq__(_checkDefined(c_0, 3170147))) ==> int___gt__(int___unbox__(lambda25_79$x), int___unbox__(lambda25_42$y)))))
   goto __end
   label __end
 }

src/test/resources/frontends/nagini/testsfunctionalverificationissues00031.py.vpr

@@ -84,7 +84,7 @@ domain PyType {
 
   unique function slice(): PyType
 
-  unique function range(): PyType
+  unique function py_range(): PyType
 
   unique function Iterator_basic(): PyType
 
@@ -292,8 +292,8 @@ domain PyType {
     extends_(slice(), object()) && get_basic(slice()) == slice()
   }
 
-  axiom subtype_range {
-    extends_(range(), object()) && get_basic(range()) == range()
+  axiom subtype_py_range {
+    extends_(py_range(), object()) && get_basic(py_range()) == py_range()
   }
 
   axiom subtype_Iterator {

src/test/resources/frontends/nagini/testsfunctionalverificationissues00057.py.vpr

@@ -84,7 +84,7 @@ domain PyType {
 
   unique function slice(): PyType
 
-  unique function range(): PyType
+  unique function py_range(): PyType
 
   unique function Iterator_basic(): PyType
 
@@ -278,8 +278,8 @@ domain PyType {
     extends_(slice(), object()) && get_basic(slice()) == slice()
   }
 
-  axiom subtype_range {
-    extends_(range(), object()) && get_basic(range()) == range()
+  axiom subtype_py_range {
+    extends_(py_range(), object()) && get_basic(py_range()) == py_range()
   }
 
   axiom subtype_Iterator {

src/test/resources/frontends/nagini/testsfunctionalverificationtest_behavioural_subtyping_classmethod.py.vpr

@@ -84,7 +84,7 @@ domain PyType {
 
   unique function slice(): PyType
 
-  unique function range(): PyType
+  unique function py_range(): PyType
 
   unique function Iterator_basic(): PyType
 
@@ -286,8 +286,8 @@ domain PyType {
     extends_(slice(), object()) && get_basic(slice()) == slice()
   }
 
-  axiom subtype_range {
-    extends_(range(), object()) && get_basic(range()) == range()
+  axiom subtype_py_range {
+    extends_(py_range(), object()) && get_basic(py_range()) == py_range()
   }
 
   axiom subtype_Iterator {