diff --git a/benchexec/tools/abc.py b/benchexec/tools/abc.py index 2af3f974f..c00c013a4 100644 --- a/benchexec/tools/abc.py +++ b/benchexec/tools/abc.py @@ -18,12 +18,24 @@ class Tool(benchexec.tools.template.BaseTool2): URL: https://people.eecs.berkeley.edu/~alanmi/abc/ """ + REQUIRED_PATHS = ["bin/", "abc.rc"] + def executable(self, tool_locator): return tool_locator.find_executable("abc", subdir="bin") def name(self): return "ABC" + def version(self, executable): + return self._version_from_tool( + executable, arg="-q version", line_prefix="UC Berkeley, ABC" + ) + + def program_files(self, executable): + return self._program_files_from_executable( + executable, self.REQUIRED_PATHS, parent_dir=True + ) + def cmdline(self, executable, options, task, rlimits): # The default read method in ABC cannot process uninitialized registers properly. # Therefore, a new read method `&r` (`&read`) is invoked here. @@ -39,7 +51,7 @@ def determine_result(self, run): """ if run.was_timeout: return result.RESULT_TIMEOUT - for line in run.output: + for line in run.output[::-1]: if line.startswith("Property proved") or line.startswith( "Networks are equivalent" ): diff --git a/benchexec/tools/avr.py b/benchexec/tools/avr.py index b5aeaaed2..01c5bd35a 100644 --- a/benchexec/tools/avr.py +++ b/benchexec/tools/avr.py @@ -7,6 +7,7 @@ import benchexec.result as result import benchexec.tools.template +from math import ceil class Tool(benchexec.tools.template.BaseTool2): @@ -15,6 +16,8 @@ class Tool(benchexec.tools.template.BaseTool2): URL: https://github.com/aman-goel/avr """ + REQUIRED_PATHS = ["build/"] + def executable(self, tool_locator): return tool_locator.find_executable("avr.py") @@ -22,6 +25,10 @@ def name(self): return "AVR" def cmdline(self, executable, options, task, rlimits): + if rlimits.cputime and "--timeout" not in options: + options += ["--timeout", str(rlimits.cputime)] + if rlimits.memory and "--memout" not in options: + options += ["--memout", str(ceil(rlimits.memory / 1000000.0))] return [executable] + options + [task.single_input_file] def determine_result(self, run): @@ -30,7 +37,7 @@ def determine_result(self, run): """ if run.was_timeout: return result.RESULT_TIMEOUT - for line in run.output: + for line in run.output[::-1]: # skip the lines that do not contain verification result if not line.startswith("Verification result:"): continue