You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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 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
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.The text was updated successfully, but these errors were encountered: