Empty Diagnostic Invariant List Crash [codex]

[mgordon]

Empty Diagnostic Invariant List Crash

Summary

CH-C can crash while saving secondary proof obligations if a diagnostic invs/arg element contains an empty invariant-list value, such as i="" or a trailing comma.

Reproducer

See repros/empty-diagnostic-invariant-list.xml.

<diagnostic>
  <invs>
    <arg a="1" i=""/>
    <arg a="2" i="17,"/>
  </invs>
</diagnostic>

Observed Failure

After SPEC CPU 2017 perlbench iteration 1, chkc c-project analyze failed while saving SPO diagnostics:

ValueError: invalid literal for int() with base 10: ''

The stack ended in CProofDiagnostic.py, parsing:

int(x) for x in xarginvs.split(",")

Cause

The XML reader assumes every comma-separated field in i is non-empty. Empty diagnostic invariant lists, or trailing commas, produce an empty string that cannot be converted with int.

Minimal Fix

Ignore empty fields while parsing the comma-separated invariant ids:

int(x) for x in xarginvs.split(",") if x != ""

empty-diagnostic-invariant-list.xml