search

static-analysis-engineering / CodeHawk-C

CodeHawk C Analyzer: sound static analysis of memory safety (undefined behavior)
MIT License
27 stars 6 forks source link

Add more program context to json output #49

Open waskyo opened 1 month ago

waskyo commented 1 month ago

This is known to be an issue with the json output, but perhaps it applies more widely.

Currently proofs only include a line number, which is not enough to disambiguate and pinpoint when multiple proofs are present in a single source line.

It is not clear to me if we need to do something special in the presence of macros?

sipma commented 4 weeks ago

Thank you for suggesting this addition to the json output!

Program contexts have now been added, with commit https://github.com/static-analysis-engineering/CodeHawk-C/pull/50/commits/9c7b66642432446cad978d492089a0e46ad40ae8 .

A description and example are given here: https://github.com/static-analysis-engineering/CodeHawk-C/pull/50#issue-2634579910

waskyo commented 3 weeks ago

Leaving this issue open to also cover the investigation of adding column numbers to the program context.