Improve the tool-info modules of ABC and AVR

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"
             ):

benchexec/tools/avr.py

@@ -15,13 +15,21 @@ 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")
 
     def name(self):
         return "AVR"
 
     def cmdline(self, executable, options, task, rlimits):
+        from math import ceil
+
+        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 +38,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