Better error messages for built-in functions (using Viper annotations)

src/nagini_translation/lib/errors/wrappers.py

@@ -84,7 +84,10 @@ def string(self, show_viper_reason: bool) -> str:
         """
         reason = self._reason_string or self._node
         if reason is None and self.identifier in VAGUE_REASONS:
-            if not show_viper_reason:
+            if (self.offending_node.info().getClass().getSimpleName() == "AnnotationInfo" and
+                    self.offending_node.info().values().contains("error")):
+                return self.offending_node.info().values().get("error").get().head()
+            elif not show_viper_reason:
                 return VAGUE_REASONS[self.identifier]
             else:
                 return self._reason.readableMessage()

src/nagini_translation/resources/bool.sil

@@ -119,7 +119,7 @@ function int___floordiv__(self: Int, other: Int): Int
 
 function int___div__(self: Int, other: Int): Ref
     decreases _
-    requires other != 0
+    requires @error("Divisor may be zero.")(other != 0)
     ensures (self % other == 0) ==> (typeof(result) == int() && int___unbox__(result) == self \ other)
     ensures (self % other != 0) ==> typeof(result) == float()
 
@@ -161,7 +161,7 @@ function Place___eq__(self: Ref, other: Ref): Bool
 
 function object___cast__(typ: PyType, obj: Ref): Ref
     decreases _
-    requires issubtype(typeof(obj), typ)
+    requires @error("Cast may not succeed.")issubtype(typeof(obj), typ)
     ensures result == obj
     ensures issubtype(typeof(obj), typ)
 

src/nagini_translation/resources/list.sil

@@ -55,7 +55,8 @@ function list___getitem__(self: Ref, key: Ref): Ref
     requires issubtype(typeof(self), list(list_arg(typeof(self), 0)))
     requires issubtype(typeof(key), int())
     requires acc(self.list_acc, wildcard)
-    requires let ln == (list___len__(self)) in ((int___unbox__(key) < 0 ==> int___unbox__(key) >= -ln) && (int___unbox__(key) >= 0 ==> int___unbox__(key) < ln))
+    requires @error("List index may be out of bounds.")(let ln == (list___len__(self)) in (int___unbox__(key) < 0 ==> int___unbox__(key) >= -ln))
+    requires @error("List index may be out of bounds.")(let ln == (list___len__(self)) in (int___unbox__(key) >= 0 ==> int___unbox__(key) < ln))
     ensures result == (int___unbox__(key) >= 0 ? self.list_acc[int___unbox__(key)] : self.list_acc[list___len__(self) + int___unbox__(key)])
     ensures issubtype(typeof(result), list_arg(typeof(self), 0))
 

src/nagini_translation/resources/preamble.index

@@ -47,7 +47,7 @@
             "args": ["list", "__prim__int", "object"],
             "type": null,
             "MustTerminate": true,
-            "requires": ["__len__"]
+            "requires": ["__len__", "__getitem__"]
         },
         "__iter__": {
             "args": ["list"],
@@ -76,7 +76,7 @@
         "__getitem__": {
             "args": ["list", "int"],
             "type": "object",
-            "requires": ["__len__"]
+            "requires": ["__len__", "int___unbox__"]
         },
         "__contains__": {
             "args": ["list", "object"],

src/nagini_translation/resources/set_dict.sil

@@ -134,7 +134,7 @@ function dict___getitem__(self: Ref, key: Ref) : Ref
     decreases _
     requires issubtype(typeof(self), dict(dict_arg(typeof(self), 0), dict_arg(typeof(self), 1)))
     requires acc(self.dict_acc, wildcard)
-    requires dict___contains__(self, key)
+    requires @error("Key might not be present in dictionary.")dict___contains__(self, key)
     ensures issubtype(typeof(result), dict_arg(typeof(self), 1))
     ensures result == self.dict_acc[key]