@@ -0,0 +1,2613 @@
+# This file is part of BenchExec, a framework for reliable benchmarking:%0A# https://github.com/sosy-lab/benchexec%0A#%0A# SPDX-FileCopyrightText: 2007-2020 Dirk Beyer %3Chttps://www.sosy-lab.org%3E%0A#%0A# SPDX-License-Identifier: Apache-2.0%0A%0Aimport os%0Aimport benchexec.util as util%0Aimport benchexec.tools.template%0Aimport benchexec.result as result%0A%0A%0Aclass Tool(benchexec.tools.template.BaseTool):%0A    %22%22%22%0A    This class serves as tool adaptor for ESBMC (http://www.esbmc.org/)%0A    %22%22%22%0A%0A    REQUIRED_PATHS = %5B%22esbmc%22, %22esbmc-wrapper.py%22, %22my_instrument%22%5D%0A%0A    def executable(self):%0A        return util.find_executable(%22esbmc-wrapper.py%22)%0A%0A    def working_directory(self, executable):%0A        executableDir = os.path.dirname(executable)%0A        return executableDir%0A%0A    def version(self, executable):%0A        return self._version_from_tool(executable, %22-v%22)%0A%0A    def name(self):%0A        return %22FuSeBMC%22%0A%0A    def cmdline(self, executable, options, tasks, propertyfile, rlimits):%0A        assert len(tasks) == 1, %22only one inputfile supported%22%0A        inputfile = tasks%5B0%5D%0A        return %5Bexecutable%5D + %5B%22-p%22, propertyfile%5D + options + %5Binputfile%5D%0A%0A    def determine_result(self, returncode, returnsignal, output, isTimeout):%0A        output = %22%5Cn%22.join(output)%0A        status = result.RESULT_UNKNOWN%0A%0A        if self.allInText(%5B%22FALSE_DEREF%22%5D, output):%0A            status = result.RESULT_FALSE_DEREF%0A        elif self.allInText(%5B%22FALSE_FREE%22%5D, output):%0A            status = result.RESULT_FALSE_FREE%0A        elif self.allInText(%5B%22FALSE_MEMTRACK%22%5D, output):%0A            status = result.RESULT_FALSE_MEMTRACK%0A        elif self.allInText(%5B%22FALSE_OVERFLOW%22%5D, output):%0A            status = result.RESULT_FALSE_OVERFLOW%0A        elif self.allInText(%5B%22FALSE_TERMINATION%22%5D, output):%0A            status = result.RESULT_FALSE_TERMINATION%0A        elif self.allInText(%5B%22FALSE%22%5D, output):%0A            status = result.RESULT_FALSE_REACH%0A        elif %22TRUE%22 in output:%0A            status = result.RESULT_TRUE_PROP%0A        elif %22DONE%22 in output:%0A            status = result.RESULT_DONE%0A%0A        if status == result.RESULT_UNKNOWN:%0A            if isTimeout:%0A                status = %22TIMEOUT%22%0A            elif output.endswith((%22error%22, %22error%5Cn%22)):%0A                status = %22ERROR%22%0A%0A        return status%0A%0A    %22%22%22 helper method %22%22%22%0A%0A    def allInText(self, words, text):%0A        %22%22%22%0A        This function checks, if all the words appear in the given order in the text.%0A        %22%22%22%0A        index = 0%0A        for word in words:%0A            index = text%5Bindex:%5D.find(word)%0A            if index == -1:%0A                return False%0A        return True%0A

Create FuSeBMC.py