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()