We should document our weirdly-named DEDORSE construct, which is a hacky workaround for memory allocation in C.
Here's the deal. In C, a malloc call returns a void*, and then you cast it to the correct type. (This is dumb, what are you gonna do?) This means you want it to sometimes give you a precise pointer and sometimes an approximate pointer. You currently can't do this in the syntax—you can't do (APPROX int *)malloc(...)—so the typechecker special-cases malloc and friends to work correctly whether you use it in a precise or approximate context.
This special-casing obviously does not work if the user writes their own memory allocation wrappers. For this case, we provide a DEDORSE cast that turns a precise pointer into an approximate pointer. It should really only be used for allocation and similar constructs, but it's worth documenting.
We should document our weirdly-named
DEDORSEconstruct, which is a hacky workaround for memory allocation in C.Here's the deal. In C, a
malloccall returns avoid*, and then you cast it to the correct type. (This is dumb, what are you gonna do?) This means you want it to sometimes give you a precise pointer and sometimes an approximate pointer. You currently can't do this in the syntax—you can't do(APPROX int *)malloc(...)—so the typechecker special-cases malloc and friends to work correctly whether you use it in a precise or approximate context.This special-casing obviously does not work if the user writes their own memory allocation wrappers. For this case, we provide a
DEDORSEcast that turns a precise pointer into an approximate pointer. It should really only be used for allocation and similar constructs, but it's worth documenting.