Mismatch between line numbers and sourcelines content in JSON when using preprocessed code

[waskyo]

Sorry for the long title, but the issue is hard to explain succinctly.

If I pass a preprocessed file to chkc, the proof obligation line numbers reference the line numbers in the source before the preprocessor was run, and not the lines in the preprocessed file.

However, filesource -> sourcelines in the json file contains the preprocessed output.

This means that the line numbers between the proof obligations and the source inside of the json don't match.

See attached json file for an example of the issue. Also attached are the original C file and preprocessed C file (renamed to .txt to appease GitHub) that I used to generate the json output.

The commands I ran were:

gcc -E hello.c > hello_preproc.c
chkc c-file run hello_preproc.c --json -o hello_preproc.c

hello_preproc.c.json
hello_preproc.c.txt
hello.c.txt

[sipma]

The reason is that the line numbers for the proof obligations are based on the line numbers that the parser receives from CIL, which are the line numbers (with file) provided by the preprocessor as # xxx in the file. When the input file is run on a preprocessed file as source those line numbers will be used for the proof obligations, but the preprocessed source file (which is the only source file available) will be used as is as the backing source, hence the mismatch.

An easy remedy is to either comment out or remove (depending on your preference) the lines that start with # ,
e.g., like so:
hello_preproc_converted.c.txt
which will give the right line numbers, relative to the source.

[waskyo]

As we talked in person, it seems like the best we can do is document this behavior and let users choose what to do.