rems-project / cerberus

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

[CN] Potentially incorrect typing #272

Open dc-mak opened 1 month ago

dc-mak commented 1 month ago

It's not clear why this fails type checking (note this is the same example as https://github.com/rems-project/cerberus/issues/270 but the issue here is not the bad location info, but why it fails in the first place). Minimised and adapted from: https://github.com/rems-project/cerberus/blob/master/tests/pnvi_testsuite/pointer_copy_user_ctrlflow_bitwise.c

16:58 ➜  cerberus git:(master) cat illtyped_multiply.error.c && cn illtyped_multiply.error.c 2>tmp.out
#include<inttypes.h>
#include<limits.h>
#include<stddef.h>
size_t f(int x) {
    return sizeof(uintptr_t) * CHAR_BIT;
}
[1/1]: f
tests/cn/illtyped_multiply.error.c:5:12: error: Type error
    return sizeof(uintptr_t) * CHAR_BIT;
           ~~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~
Expected value of type 'u64' but found value of type 'u32'
dc-mak commented 1 month ago

Possibly related to https://github.com/rems-project/cerberus/issues/236 and also https://github.com/rems-project/cerberus/issues/257