stainless
stainless copied to clipboard
GenC: incorrect use of copy instead of reference when binding values (with `if` expressions)
Similar to https://github.com/epfl-lara/stainless/issues/1284, the following snippet is incorrectly translated:
import stainless.proof._
import stainless.io._
import stainless.lang._
import stainless.annotation._
object GenCRefCopy2 {
@cCode.noMangling
case class Ref(var x: Int, var y: Int)
@cCode.`export`
def main(): Int = {
implicit val state = stainless.io.newState
val cond = false
val r1 = Ref(1, 2)
val r2 = if (cond) Ref(12, 34) else r1 // Note: if we don't use ifs, r2 gets correctly translated to a reference to r1
r2.x = 10
assert(r1.x == 10) // Valid VC
StdOut.println(r1.x) // Transpiled code prints 1 instead of 10
0
}
}
Generated (cleaned) code:
typedef struct {
int32_t x;
int32_t y;
} Ref;
int32_t main(void) {
bool cond = false;
Ref r1 = (Ref) { .x = 1, .y = 2 };
Ref norm;
if (cond) {
norm = (Ref) { .x = 12, .y = 34 }; // Ok
} else {
norm = r1; // Copy instead of a reference!
}
Ref* r2 = &norm;
r2->x = 10;
printf("%d\n", r1.x);
return 0;
}