search

rems-project / cerberus

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

[CN] _ExtInt value not representable #278

Open podhrmic opened 4 months ago

podhrmic commented 4 months ago

We have some Cryptol generated code that uses _ExtInt() primitive, which triggers this error:

/src/variants/../generated/C/saturation_impl.c:88:16: error: integer value not representable at type signed int
    app_4158 = (signed _ExtInt(32)) t4762 < (signed _ExtInt(32)) (w32) 35;
               ^~~~~~~~~~~~~~~~~~
kmemarian commented 4 months ago

_ExtInt()/_BitInt() are a C23 feature that Cerberus does not support.