def viewer()

in cbmc_viewer/viewer.py [0:0]

• 57 lines of code
• 5 McCabe index (conditional complexity)

def viewer():
    """Construct the cbmc report."""

    parser = create_parser()
    args = parser.parse_args()
    args = optionst.defaults(args)

    if not (args.result or args.viewer_result or args.coverage or args.viewer_coverage):
        parser.error("Need property checking results or coverage checking results.")

    global_progress("CBMC viewer")

    htmldir = os.path.join(args.reportdir, "html")
    jsondir = os.path.join(args.reportdir, "json")
    os.makedirs(htmldir, exist_ok=True)
    os.makedirs(jsondir, exist_ok=True)

    def dump(obj, name):
        with open(os.path.join(jsondir, name), 'w') as output:
            output.write(str(obj))

    progress("Scanning property checking results")
    results = resultt.make_result(args.viewer_result, args.result)
    dump(results, 'viewer-result.json')
    progress("Scanning property checking results", True)

    progress("Scanning error traces")
    traces = tracet.make_trace(args.viewer_trace, args.result, args.srcdir, args.wkdir)
    dump(traces, 'viewer-trace.json')
    progress("Scanning error traces", True)

    progress("Scanning coverage data")
    coverage = coveraget.make_coverage(args.viewer_coverage, args.srcdir, args.coverage)
    dump(coverage, 'viewer-coverage.json')
    progress("Scanning coverage data", True)

    progress("Scanning loop definitions")
    loops = loopt.make_loop(args.viewer_loop, None, args.srcdir, args.goto)
    dump(loops, 'viewer-loop.json')
    progress("Scanning loop definitions", True)

    progress("Scanning properties")
    properties = propertyt.make_property(args.viewer_property, args.property, args.srcdir)
    dump(properties, 'viewer-property.json')
    progress("Scanning properties", True)

    progress("Computing reachable functions")
    reachable = reachablet.make_reachable(args.viewer_reachable, None, args.srcdir, args.goto)
    dump(reachable, 'viewer-reachable.json')
    progress("Computing reachable functions", True)

    # Make sources last, it may delete the goto binary
    progress("Scanning source tree")
    sources = sourcet.make_source(args.viewer_source,
                                  args.goto,
                                  args.source_method,
                                  args.srcdir, args.wkdir,
                                  args.exclude, args.extensions)
    dump(sources, 'viewer-source.json')
    progress("Scanning source tree", True)

    progress("Preparing symbol table")
    symbols = symbolt.make_symbol(args.viewer_symbol, args.viewer_source,
                                  args.goto, args.wkdir,
                                  args.srcdir, None)
    dump(symbols, 'viewer-symbol.json')
    progress("Preparing symbol table", True)

    config = configt.Config(args.config)
    report.report(config, sources, symbols, results, coverage, traces,
                  properties, loops, htmldir, progress)

    global_progress("CBMC viewer", True)
    return 0 # exit with normal return code