def close_function_stack_frames()

in cbmc_viewer/tracet.py [0:0]

• 39 lines of code
• 6 McCabe index (conditional complexity)

def close_function_stack_frames(trace):
    """Append function-return steps missing from end of a trace.

    The json and xml traces from cbmc include function-call
    and function-return steps, but each error trace ends with
    a failure and omits the function returns for the function
    calls remaining on the call stack.  This appends these
    missing function returns to the end of the trace so that
    all function calls are properly nested and bracketed with
    call/return steps."""

    stack = []

    def push_stack(stack, elt):
        stack.append(elt)
        return stack

    def pop_stack(stack):
        assert stack
        return stack[-1], stack[:-1]

    location = None
    for step in trace:
        kind = step['kind']
        location = step['location']
        callee_name = step.get('detail', {}).get('name')
        callee_name_path = step.get('detail', {}).get('name-path')
        callee_location = step.get('detail', {}).get('location')

        if kind == 'function-call':
            stack = push_stack(stack, (callee_name, callee_name_path, callee_location))
            continue

        if kind == 'function-return':
            pair, stack = pop_stack(stack)
            callee_name_, _, _ = pair
            if callee_name != callee_name_:
                raise UserWarning('Function call-return mismatch: {} {}'
                                  .format(callee_name, callee_name_))
            continue

    stack.reverse()
    for callee_name, callee_name_path, callee_location in stack:
        function_return = {
            "detail": {
                "location": callee_location,
                "name": callee_name,
                "name-path": callee_name_path
            },
            "kind": "function-return",
            "location": location,
            "hidden": True # TODO: should match corresponding call
        }
        trace.append(function_return)

    return trace