rems-project / cerberus

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

[CN] `ptr_eq` typing (confusingly) not strict enough #380

Open dc-mak opened 4 months ago

dc-mak commented 4 months ago

Specifically, x and y should have type u64 not pointer

12:56 ➜  2024-cn-testing-paper git:(main) cat tmp.c && cn tmp.c
void f(unsigned int x, unsigned int y)
/*@ requires ptr_eq(x,y);
   ensures true; @*/
{ }

[1/1]: f
dc-mak commented 2 months ago

The way to solve this would be to convert the definitions in backend/cn/lib/builtins.ml to LogicalFunction.defintion types and then adjust init_env in backend/cn/lib/compile.ml to have functions = (* builtins list to map *).