Missing variable declaration in printed C function when using stack allocation.

[RasmusHoldsbjergCSAU]

I have been using the ToCString printer to generate C functions, but there appears to be problem with stack allocation.
When printing to C this function:
https://github.com/RasmusHoldsbjergCSAU/fiat-crypto/blob/master/src/Bedrock/Field/Synthesis/Examples/quadratic_extension_bls12.v#L191-L222

The output is the following:

void Fp2_mul(uintptr_t outr, uintptr_t outi, uintptr_t xr, uintptr_t xi, uintptr_t yr, uintptr_t yi) {
uintptr_t v0;
v0 = alloca((uintptr_t)48ULL); // TODO untested
v1 = alloca((uintptr_t)48ULL); // TODO untested
v2 = alloca((uintptr_t)48ULL); // TODO untested
bls12_mul(v0, xr, yr);
bls12_mul(v1, xi, yi);
bls12_sub(outr, v0, v1);
bls12_add(v2, xr, xi);
bls12_add(outi, yr, yi);
bls12_mul(outi, v2, outi);
bls12_sub(outi, outi, v0);
bls12_sub(outi, outi, v1);
return;
}

The thing to notice is the first 4 lines of the function body: Although memory is allocated for three arrays, only one is declared.

I am able to reproduce this issue in the "stackalloc.v" example by modifying this line here:
https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/bedrock2Examples/stackalloc.v#L17
to:
("stackdisj", ([]:list String.string, [], bedrock_func_body:(

i.e. by not returning pointers to the allocated memory.

Is this a bug or am I missing something?

[samuelgruetter]

I just pushed a bugfix, can you try if that solves the problem for you?

[RasmusHoldsbjergCSAU]

Great Thanks, this worked! : )