Bad code generation when dereferencing directly a rc_copy_alloc_id
The following example fails https://gitlab.mpi-sws.org/iris/refinedc/-/blob/master/examples/intptr.c#L68.
I tried fixing code generation with a hack, changing
let (e2, l2) = translate_expr lval None e2 in
let (e3, l3) = translate_expr lval None e3 in
(locate (CopyAID(e3, e2)), l2 @ l3)
into
let (e2, l2) = translate_expr false None e2 in
let (e3, l3) = translate_expr false None e3 in
let e = locate (CopyAID(e3, e2)) in
let e = if lval then locate (Deref(false, LPtr, e)) else e in
(e, l2 @ l3)
but with that the automation still gets stuck. In fact, there might also be a problem there, I'm not sure.
You end up with a read rule with a term of the form !{LPtr} (CopyAID ...)
.
Clearly, this is again a LValue versus RValue problem, but I can't find how to solve it. Any idea?