Tests for old issues and some small fixes

src/nagini_translation/main.py

@@ -97,7 +97,10 @@ def translate(path: str, jvm: JVM, selected: Set[str] = set(), base_dir: str = N
     path = os.path.abspath(path)
     error_manager.clear()
     current_path = os.path.dirname(inspect.stack()[0][1])
-    resources_path = os.path.join(current_path, 'resources')
+    if sif:
+        preamble_path = os.path.join(current_path, 'sif', 'resources')
+    else:
+        preamble_path = os.path.join(current_path, 'resources')
 
     if sif:
         viper_ast = ViperASTExtended(jvm, jvm.java, jvm.scala, jvm.viper, path)
@@ -114,7 +117,7 @@ def translate(path: str, jvm: JVM, selected: Set[str] = set(), base_dir: str = N
 
     analyzer = Analyzer(types, path, selected)
     main_module = analyzer.module
-    with open(os.path.join(resources_path, 'preamble.index'), 'r') as file:
+    with open(os.path.join(preamble_path, 'preamble.index'), 'r') as file:
         analyzer.add_native_silver_builtins(json.loads(file.read()))
 
     analyzer.initialize_io_analyzer()

src/nagini_translation/resources/all.sil

@@ -12,10 +12,15 @@ domain SIFDomain[T] {
     axiom low_true {
         forall x: T :: {Low(x)} Low(x)
     }
+    axiom lowevent_true {
+        LowEvent()
+    }
+    function LowEvent(): Bool
 }
 
 
 import "bool.sil"
+import "references.sil"
 import "bytes.sil"
 import "iterator.sil"
 import "list.sil"

src/nagini_translation/resources/bool.sil

@@ -18,10 +18,6 @@ function NoneType___bool__(self: Ref) : Bool
     decreases _
     ensures self == null ==> !result
 
-function object___str__(self: Ref) : Ref
-    decreases _
-    ensures issubtype(typeof(result), str())
-
 function bool___bool__(self: Ref) : Bool
     decreases _
     requires self != null ==> issubtype(typeof(self), bool())
@@ -258,4 +254,6 @@ function abs(a: Int): Int
     decreases _
     ensures result == (a >= 0 ? a : -a)
 
-method print(r: Ref)
+method print(r: Ref)
+    requires Low(r)
+    requires LowEvent()

src/nagini_translation/resources/preamble.index

@@ -542,7 +542,8 @@
         },
         "__len__": {
             "args": ["tuple"],
-            "type": "__prim__int"
+            "type": "__prim__int",
+            "requires": ["__val__", "args"]
         },
         "__val__": {
             "args": ["tuple"],

src/nagini_translation/resources/references.sil

@@ -0,0 +1,11 @@
+/*
+ * Copyright (c) 2019 ETH Zurich
+ * This Source Code Form is subject to the terms of the Mozilla Public
+ * License, v. 2.0. If a copy of the MPL was not distributed with this
+ * file, You can obtain one at http://mozilla.org/MPL/2.0/.
+ */
+
+
+ function object___str__(self: Ref) : Ref
+    decreases _
+    ensures issubtype(typeof(result), str())

src/nagini_translation/sif/resources/all.sil

@@ -5,11 +5,15 @@
  * file, You can obtain one at http://mozilla.org/MPL/2.0/.
  */
 
+import <decreases/int.vpr>
+
 domain SIFDomain[T] {
     function Low(x: T): Bool
+    function LowEvent(): Bool
 }
 
 import "../../resources/bool.sil"
+import "references.sil"
 import "../../resources/bytes.sil"
 import "../../resources/iterator.sil"
 import "../../resources/list.sil"