More annotations for precondition errors for builtin functions

src/nagini_translation/resources/bool.sil

@@ -130,7 +130,7 @@ function int___mul__(self: Int, other: Int): Int
 
 function int___floordiv__(self: Int, other: Int): Int
     decreases _
-    requires other != 0
+    requires @error("Divisor may be zero.")(other != 0)
 {
     self \ other
 }

src/nagini_translation/resources/float.sil

@@ -101,7 +101,7 @@ function float___truediv__(self: Ref, other: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
-    requires issubtype(typeof(other), int()) ==> int___unbox__(other) != 0
+    requires @error("Divisor may be zero.")(issubtype(typeof(other), int()) ==> @error("Divisor may be zero.")(int___unbox__(other) != 0))
     requires issubtype(typeof(other), int())  // cannot express non-zero at the moment
     ensures issubtype(typeof(result), float())
     ensures (issubtype(typeof(self), int()) && issubtype(typeof(other), int())) ==>
@@ -123,7 +123,7 @@ function float___rtruediv__(self: Ref, other: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
-    requires issubtype(typeof(self), int()) ==> int___unbox__(self) != 0
+    requires @error("Divisor may be zero.")(issubtype(typeof(self), int()) ==> @error("Divisor may be zero.")(int___unbox__(self) != 0))
     requires issubtype(typeof(self), int())  // cannot express non-zero at the moment
     ensures issubtype(typeof(result), float())
     ensures (issubtype(typeof(self), int()) && issubtype(typeof(other), int())) ==>

src/nagini_translation/resources/float_ieee32.sil

@@ -99,7 +99,7 @@ function float___truediv__(self: Ref, other: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
-    requires float___unbox__(other) != ___float32_zero()
+    requires @error("Divisor may be zero.")(float___unbox__(other) != ___float32_zero())
     ensures issubtype(typeof(result), float())
     ensures result == __prim__perm___box__(___float32_div(float___unbox__(self), float___unbox__(other)))
 
@@ -119,7 +119,7 @@ function float___rtruediv__(self: Ref, other: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
-    requires float___unbox__(self) != ___float32_zero()
+    requires @error("Divisor may be zero.")(float___unbox__(self) != ___float32_zero())
     ensures issubtype(typeof(result), float())
     ensures result == __prim__perm___box__(___float32_div(float___unbox__(other), float___unbox__(self)))
 

src/nagini_translation/resources/float_real.sil

@@ -330,8 +330,8 @@ function float___truediv__(self: Ref, other: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
-    requires float___is_nan__(other) == false && float___is_inf__(other, false) == false && float___is_inf__(other, true) == false ==>
-        float___unbox__(other) != 0 / 1
+    requires @error("Divisor may be zero.")(float___is_nan__(other) == false && float___is_inf__(other, false) == false && float___is_inf__(other, true) == false ==>
+        @error("Divisor may be zero.")(float___unbox__(other) != 0 / 1))
     ensures issubtype(typeof(result), float())
     ensures float___is_nan__(self) == true || float___is_nan__(other) == true ==>
         result == float___box_nan()
@@ -366,8 +366,8 @@ function float___rtruediv__(self: Ref, other: Ref): Ref
     decreases _
     requires issubtype(typeof(self), float())
     requires issubtype(typeof(other), float())
-    requires float___is_nan__(self) == false && float___is_inf__(self, false) == false && float___is_inf__(self, true) == false ==>
-        float___unbox__(self) != 0 / 1
+    requires @error("Divisor may be zero.")(float___is_nan__(self) == false && float___is_inf__(self, false) == false && float___is_inf__(self, true) == false ==>
+        @error("Divisor may be zero.")(float___unbox__(self) != 0 / 1))
     ensures issubtype(typeof(result), float())
     ensures float___is_nan__(self) == true || float___is_nan__(other) == true ==>
         result == float___box_nan()

src/nagini_translation/resources/list.sil

@@ -75,8 +75,8 @@ method list___getitem_slice__(self: Ref, key: Ref) returns (_res: Ref)
 method list___setitem__(self: Ref, key: Int, item: Ref) returns ()
     requires issubtype(typeof(self), list(list_arg(typeof(self), 0)))
     requires acc(self.list_acc)
-    requires key >= 0
-    requires key < list___len__(self)
+    requires @error("List index may be negative.")(key >= 0)
+    requires @error("List index may be out of bounds.")(key < list___len__(self))
     requires issubtype(typeof(item), list_arg(typeof(self), 0))
     ensures acc(self.list_acc)
     ensures self.list_acc == old(self.list_acc)[key := item]

src/nagini_translation/resources/seq.sil

@@ -24,8 +24,8 @@ function PSeq___getitem__(self: Ref, index: Ref): Ref
     decreases _
     requires issubtype(typeof(self), PSeq(PSeq_arg(typeof(self), 0)))
     requires issubtype(typeof(index), int())
-    requires let ln == (PSeq___len__(self)) in
-                ((int___unbox__(index) < 0 ==> int___unbox__(index) >= -ln) && (int___unbox__(index) >= 0 ==> int___unbox__(index) < ln))
+    requires @error("Index may be out of bounds.")(let ln == (PSeq___len__(self)) in
+                @error("Index may be out of bounds.")((int___unbox__(index) < 0 ==> int___unbox__(index) >= -ln) && (int___unbox__(index) >= 0 ==> int___unbox__(index) < ln)))
     ensures result == (int___unbox__(index) >= 0 ? PSeq___sil_seq__(self)[int___unbox__(index)] : PSeq___sil_seq__(self)[PSeq___len__(self) + int___unbox__(index)])
     ensures issubtype(typeof(result), PSeq_arg(typeof(self), 0))
 

src/nagini_translation/resources/tuple.sil

@@ -105,7 +105,8 @@ function tuple___len__(self: Ref): Int
 
 function tuple___getitem__(self: Ref, key: Int): Ref
     decreases _
-    requires let ln == (tuple___len__(self)) in ((key >= 0 ==> key < ln) && (key < 0 ==> key >= -ln))
+    requires @error("Tuple index may be out of bounds.")(let ln == (tuple___len__(self)) in
+        @error("Tuple index may be out of bounds.")((key >= 0 ==> key < ln) && (key < 0 ==> key >= -ln)))
     ensures key >= 0 ==> issubtype(typeof(result), tuple_arg(typeof(self), key))
     ensures key < 0 ==> issubtype(typeof(result), tuple_arg(typeof(self), tuple___len__(self) + key))
     ensures key >= 0 ==> result == tuple___val__(self)[key]
@@ -114,8 +115,8 @@ function tuple___getitem__(self: Ref, key: Int): Ref
 function tuple___getitem_slice__(self: Ref, key: Ref): Ref
     decreases _
     requires issubtype(typeof(key), slice())
-    requires (slice___start__(key, tuple___len__(self)) >= 0 && slice___start__(key, tuple___len__(self)) <= tuple___len__(self))
-    requires (slice___stop__(key, tuple___len__(self)) >= 0 && slice___stop__(key, tuple___len__(self)) <= tuple___len__(self))
+    requires @error("Slice start may be out of bounds.")(slice___start__(key, tuple___len__(self)) >= 0 && slice___start__(key, tuple___len__(self)) <= tuple___len__(self))
+    requires @error("Slice end index may be out of bounds.")(slice___stop__(key, tuple___len__(self)) >= 0 && slice___stop__(key, tuple___len__(self)) <= tuple___len__(self))
     ensures typeof(result) == tuple(tuple_args(typeof(self))[slice___start__(key, tuple___len__(self))..slice___stop__(key, tuple___len__(self))])
     ensures forall i: Int :: {tuple_arg(typeof(result), i)} (i >= 0 && i < (slice___stop__(key, tuple___len__(self)) - slice___start__(key, tuple___len__(self)))) ==> tuple_arg(typeof(result), i) == tuple_arg(typeof(self), i + slice___start__(key, tuple___len__(self)))
     ensures tuple___len__(result) == (slice___stop__(key, tuple___len__(self)) - slice___start__(key, tuple___len__(self)))