Merge pull request #178 from PascalDevenoge/master

Terminate with error code according to verification result

src/nagini_translation/main.py

@@ -11,6 +11,7 @@
 import json
 import logging
 import os
+import sys
 import re
 import time
 import traceback
@@ -45,6 +46,7 @@
     VerificationResult,
     ViperVerifier
 )
+from nagini_translation import verifier
 from typing import List, Set, Tuple
 
 
@@ -370,10 +372,16 @@ def add_response(part):
             translate_and_verify(file, jvm, args, add_response, arp=args.arp, base_dir=args.base_dir)
             socket.send_string(response[0])
     else:
-        translate_and_verify(args.python_file, jvm, args, arp=args.arp, base_dir=args.base_dir)
+        success = translate_and_verify(args.python_file, jvm, args, arp=args.arp, base_dir=args.base_dir)
+        sys.exit(0 if success else 1)
 
 
-def translate_and_verify(python_file, jvm, args, print=print, arp=False, base_dir=None):
+def translate_and_verify(python_file, jvm, args, print=print, arp=False, base_dir=None) -> bool:
+    """
+    Translates input file to viper code and dispatches result to backend for verification
+
+    :returns: Whether translation and verification was successful
+    """
     try:
         start = time.time()
         selected = set(args.select.split(',')) if args.select else set()
@@ -412,6 +420,7 @@ def translate_and_verify(python_file, jvm, args, print=print, arp=False, base_di
         print(vresult.to_string(args.ide_mode, args.show_viper_errors))
         duration = '{:.2f}'.format(time.time() - start)
         print('Verification took ' + duration + ' seconds.')
+        return isinstance(vresult, verifier.Success)
     except (TypeException, InvalidProgramException, UnsupportedException) as e:
         print("Translation failed")
         if isinstance(e, (InvalidProgramException, UnsupportedException)):
@@ -443,8 +452,10 @@ def translate_and_verify(python_file, jvm, args, print=print, arp=False, base_di
                     print('Type error: ' + msg + ' (' + file + '@' + line + '.0)')
                 else:
                     print(msg)
+        return False
     except ConsistencyException as e:
         print(e.message + ': Translated AST contains inconsistencies.')
+        return False
 
     except JException as e:
         print(e.stacktrace())