rems-project / cerberus

Cerberus C semantics
https://www.cl.cam.ac.uk/~pes20/cerberus/
Other
48 stars 25 forks source link

[CN] error message locations do not account for the preprocessor #393

Open peterohanley opened 1 month ago

peterohanley commented 1 month ago

This file has a const violation and CN prints an error message, but the error message is using the column information from after preprocessing with the source from before preprocessing.

#define LONGNAME 1
#define OTHER 2
void baz(unsigned char *dest, unsigned char *src, unsigned int n);
void foo(const unsigned char *bar, unsigned char *a)
{
    baz(&a[LONGNAME],bar,OTHER);
}
% cn errmsg_defines.c
errmsg_defines.c:6:15: error: constraint violation: passing 'const unsigned char*' to parameter of type 'unsigned char*' discards qualifiers
    baz(&a[LONGNAME],bar,OTHER);
              ^~~ 

If we inline LONGNAME we can see that the message is indeed for bar.

% cn errmsg_defines.c
errmsg_defines.c:6:15: error: constraint violation: passing 'const unsigned char*' to parameter of type 'unsigned char*' discards qualifiers
    baz(&a[1],bar,OTHER);
              ^~~ 

This one is probably pretty low priority, it's entirely an inconvenience.

yav commented 1 month ago

I've run into these kinds of issues before. My experience is that using a standard separate preprocessor one can get reliable line information, but not column information. I think popular C compilers just implement the preprocessing as part of their parsing infrastructure. We could consider implementing C's preprocessing algorithm. Not only we could potentially keep more precise location information, but that might make it possible to run the pre-processor on CN specification comments as well, which could be quite handy.

cp526 commented 1 month ago

More precise source locations and the ability to run the preprocessor on CN specifications would both be good.

But I assume implementing something that's fully compatible -- makes exactly the same decisions as the c compiler (if that's even consistent between clang and gcc) -- would be a big task. And if CN's custom preprocessor doesn't match their behaviour it becomes unusable for bigger projects.

yav commented 1 month ago

Writing a C preprocessing algorithm is something I've been meaning to do for a while, so I might have a go at it either on some project or in my free time. If anyone else is interested in this topic, here's a useful reference I've found:

https://www.spinellis.gr/blog/20060626/cpp.algo.pdf

PeterSewell commented 1 month ago

You should talk with Kayvan about this before embarking on it...

On Wed, 31 Jul 2024 at 17:38, Iavor S. Diatchki @.***> wrote:

Writing a C preprocessing algorithm is something I've been meaning to do for a while, so I might have a go at it either on some project or in my free time. If anyone else is interested in this topic, here's a useful reference I've found:

https://www.spinellis.gr/blog/20060626/cpp.algo.pdf

— Reply to this email directly, view it on GitHub https://github.com/rems-project/cerberus/issues/393#issuecomment-2260930079, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFMZZRLWAXBSZW3QATBK4TZPEHGXAVCNFSM6AAAAABK7PWRH6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDENRQHEZTAMBXHE . You are receiving this because you are subscribed to this thread.Message ID: @.***>

yav commented 1 month ago

Will do. I think there's likely more urgent things to fix, this is just something I've been looking into for a while, which is why I though I'd chime in :-)

peterohanley commented 1 week ago

This shift also happens with the source locations in state files.