Merge branch 'master' into builtin_function_errors

src/nagini_translation/lib/viper_ast.py

@@ -142,11 +142,10 @@ def Method(self, name, args, returns, pres, posts, locals, body, position,
             body_with_locals = self.none
         else:
             body_with_locals = self.scala.Some(self.Seqn([body], position, info, locals))
-        method = getobject(self.ast, "MethodWithLabelsInScope")
-        return method.apply(name, self.to_seq(args), self.to_seq(returns),
-                            self.to_seq(pres), self.to_seq(posts),
-                            body_with_locals, position, info,
-                            self.NoTrafos)
+        return self.ast.Method(name, self.to_seq(args), self.to_seq(returns),
+                               self.to_seq(pres), self.to_seq(posts),
+                               body_with_locals, position, info,
+                               self.NoTrafos)
 
     def Field(self, name, type, position, info):
         return self.ast.Field(name, type, position, info, self.NoTrafos)
@@ -293,7 +292,7 @@ def DecreasesWildcard(self, condition, position, info):
 
     def PredicateInstance(self, args, pred_name, position, info):
         args_seq = self.to_seq(args)
-        return self.jvm.viper.silver.plugin.standard.predicateinstance.PredicateInstance(args_seq, pred_name, position, info, self.NoTrafos)
+        return self.jvm.viper.silver.plugin.standard.predicateinstance.PredicateInstance(pred_name, args_seq, position, info, self.NoTrafos)
 
     def FullPerm(self, position, info):
         return self.ast.FullPerm(position, info, self.NoTrafos)

src/nagini_translation/main.py

@@ -65,7 +65,8 @@ def parse_sil_file(sil_path: str, jvm, float_option: str = None):
     path = jvm.java.nio.file.Paths.get(sil_path, [])
     none = getattr(getattr(jvm.scala, 'None$'), 'MODULE$')
     tp.beforeParse(text, False)
-    parsed = parser.parse(text, path, none)
+    diskloader = getattr(getattr(jvm.viper.silver.ast.utility, "DiskLoader$"), "MODULE$")
+    parsed = parser.parse(text, path, none, diskloader)
 
     parse_result = parsed
     parse_result.initProperties()