def make_reachable()

in cbmc_viewer/reachablet.py [0:0]


def make_reachable(viewer_reachable, cbmc_reachable, srcdir, goto):
    """The implementation of make-reachable."""

    if viewer_reachable:
        if filet.all_json_files(viewer_reachable):
            return ReachableFromJson(viewer_reachable)
        fail("Expected json files: {}".format(viewer_reachable))

    if cbmc_reachable and srcdir:
        if filet.all_json_files(cbmc_reachable):
            return ReachableFromCbmcJson(cbmc_reachable, srcdir)
        if filet.all_xml_files(cbmc_reachable):
            return ReachableFromCbmcXml(cbmc_reachable, srcdir)
        fail("Expected json files or xml files, not both: {}"
             .format(cbmc_reachable))

    if goto and srcdir:
        return ReachableFromGoto(goto, srcdir)

    logging.info("make-reachable: nothing to do: need "
                 "--srcdir and --goto, or "
                 "cbmc reachable functions results (goto-analyzer --reachable-functions)"
                 " and --srcdir, or "
                 "--viewer-reachable")
    return Reachable()