def check_path_satisfiability(self, path, start_address, verbose=False):
        self._solver.reset()

        start_instr_found = False
        sat = False

        # Traverse basic blocks, translate its instructions to SMT
        # expressions and add them as assertions.
        for bb_curr, bb_next in zip(path[:-1], path[1:]):
            logger.info("BB @ {:#x}".format(bb_curr.address))

            # For each dual instruction...
            for dinstr in bb_curr:
                # If the start instruction have not been found, keep
                # looking...
                if not start_instr_found:
                    if dinstr.address == start_address:
                        start_instr_found = True
                    else:
                        continue

                logger.info("{:#x} {}".format(dinstr.address, dinstr.asm_instr))

                # For each REIL instruction...
                for reil_instr in dinstr.ir_instrs:
                    logger.info("{:#x} {:02d} {}".format(reil_instr.address >> 0x8, reil_instr.address & 0xff, reil_instr))

                    if reil_instr.mnemonic == ReilMnemonic.JCC:
                        # Check that the JCC is the last instruction of
                        # the basic block (skip CALL instructions.)
                        if dinstr.address + dinstr.asm_instr.size - 1 != bb_curr.end_address:
                            logger.error("Unexpected JCC instruction: {:#x} {} ({})".format(dinstr.address, dinstr.asm_instr, reil_instr))

                            # raise Exception()

                            continue

                        # Make sure branch target address from current
                        # basic block is the start address of the next.
                        assert(bb_curr.taken_branch == bb_next.address or
                            bb_curr.not_taken_branch == bb_next.address or
                            bb_curr.direct_branch == bb_next.address)

                        # Set branch condition accordingly.
                        if bb_curr.taken_branch == bb_next.address:
                            branch_var_goal = 0x1
                        elif bb_curr.not_taken_branch == bb_next.address:
                            branch_var_goal = 0x0
                        else:
                            continue

                        # Add branch condition goal contraint.
                        branch_var = self.get_operand_var(reil_instr.operands[0])

                        self.add_constraint(branch_var == branch_var_goal)

                        # The JCC instruction was the last within the
                        # current basic block. End this iteration and
                        # start next one.
                        break

                    # Translate and add SMT expressions to the solver.
                    for smt_expr in self._translator.translate(reil_instr):
                        logger.info("{}".format(smt_expr))

                        self._solver.add(smt_expr)

            sat = self._solver.check() == 'sat'

            logger.info("BB @ {:#x} sat? {}".format(bb_curr.address, sat))

            if not sat:
                break

        # Return satisfiability.
        return sat
Check satisfiability of a basic block path.
dataset/ETHPy150Open programa-stic/barf-project/barf/barf/analysis/codeanalyzer/codeanalyzer.py/CodeAnalyzer.check_path_satisfiability