Format with black; change script to nitwit.sh; remove unnecessary code
@@ -31,31 +31,38 @@ import benchexec.util as util
class Tool(benchexec.tools.template.BaseTool):
"""
- Tool info for the Nitwit Validator, an interpreter-based violation witness validator.
+ Tool info for the NITWIT Validator, an interpreter-based violation witness validator.
URL: https://github.com/moves-rwth/nitwit-validator
"""
+
REQUIRED_PATHS = []
- BIN_DIR = 'bin'
+ BIN_DIR = "bin"
def executable(self):
- executable = util.find_executable('validate.sh')
+ executable = util.find_executable("nitwit.sh")
bin_path = os.path.join(os.path.dirname(executable), self.BIN_DIR)
- if not os.path.isdir(bin_path) or \
- not os.path.isfile(os.path.join(bin_path, "nitwit32")) or \
- not os.path.isfile(os.path.join(bin_path, "nitwit64")):
- logging.warning("Required binary files for Nitwit not found in {0}.".format(bin_path))
+ if (
+ not os.path.isdir(bin_path)
+ or not os.path.isfile(os.path.join(bin_path, "nitwit32"))
+ or not os.path.isfile(os.path.join(bin_path, "nitwit64"))
+ ):
+ logging.warning(
+ "Required binary files for Nitwit not found in {0}.".format(bin_path)
+ )
return executable
def program_files(self, executable):
- return [executable, os.path.join(self.BIN_DIR, 'nitwit32'),
- os.path.join(self.BIN_DIR, 'nitwit64')]
+ return [
+ executable,
+ os.path.join(self.BIN_DIR, "nitwit32"),
+ os.path.join(self.BIN_DIR, "nitwit64"),
+ ]
def version(self, executable):
- stdout = self._version_from_tool(executable, '--version')
- return stdout.strip()
+ return self._version_from_tool(executable, "--version")
def name(self):
- return 'Nitwit'
+ return "Nitwit"
def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}):
if propertyfile:
@@ -64,6 +71,8 @@ class Tool(benchexec.tools.template.BaseTool):
def determine_result(self, returncode, returnsignal, output, isTimeout):
"""
+ See README.md at https://github.com/moves-rwth/nitwit-validator for information
+ about result codes.
@param returncode: code returned
@param returnsignal: signal, which terminated validator
@param output: the std output
@@ -71,19 +80,17 @@ class Tool(benchexec.tools.template.BaseTool):
"""
if returnsignal == 0 and (returncode == 0 or returncode == 245):
status = result.RESULT_FALSE_REACH
- elif returncode is None or returncode == -9:
- status = 'TIMEOUT'
- elif returncode in [4, 5, 240, 241, 242, 243, 250]:
+ elif returncode is None or returncode in [-9, 9]:
+ status = "TIMEOUT"
+ elif returncode in [4, 5, 241, 242, 243, 250]:
status = result.RESULT_UNKNOWN
else:
status = result.RESULT_ERROR
- if 'Out of memory' in output or returncode == 251:
- status = 'OUT OF MEMORY'
+ if "Out of memory" in output or returncode == 251:
+ status = "OUT OF MEMORY"
if not status:
status = result.RESULT_ERROR
- if isTimeout:
- status = 'TIMEOUT'
return status
