Skip to content

Track block-comment state across lines when computing brace depth #154

Description

@Fancyyyf

Summary

_compute_brace_depth_per_line scans each line independently. It skips a block
comment only until the end of the current line and does not preserve an
in_block_comment state for the following line.

The implementation comment says:

# If block comment spans lines, we ignore braces inside it (simplified)

but braces on subsequent comment lines are processed as real syntax.

Affected locations

  • src/reasoner.py:25-79 (_compute_brace_depth_per_line)
  • src/reasoner.py:82-147 (_split_into_blocks_braced, which consumes the
    incorrect depths)

Reproduction

This valid C/C++ input contains a closing brace inside a block comment:

int f() {
    /* comment starts
       }
    */
    return 0;
}

Equivalent test:

lines = [
    "int f() {",
    "    /* comment starts",
    "       }",
    "    */",
    "    return 0;",
    "}",
]

assert _compute_brace_depth_per_line(lines) == [1, 1, 1, 1, 1, 0]

Current result:

[1, 1, 0, 0, 0, -1]

The brace in the comment closes the function early, and the real final brace
then drives the depth negative.

Impact

_split_into_blocks_braced treats the computed depth as a safe syntactic
boundary:

if depths[j] == entry_depth:
    split_point = j

Incorrect depths can therefore split a function at a comment or nested-block
boundary. The reasoner then chains postconditions across blocks that do not
represent valid syntactic units, increasing both false-positive and
false-negative verification results.

The issue affects languages routed through this shared brace scanner, including
C, C++, Java, JavaScript/TypeScript, Rust, and similar brace-delimited
languages.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions