parsing of record field names that collide with variable names about uclid HOT 4 OPEN

Hi Matt,

Is this expected? In my thinking, x is a record instance. But Uclid5 does not seem to enjoy its field having the same name.

Let's say I don't think this is deliberate but I am not surprised.. can you work around by having different names and I'll look into it. At the very least we should throw a more meaningful error.

arr[0].a = 10;

Yes, we currently don't parse this, it's on my list of things to add. It's a bit laborious, especially with a big record type, but instead you can write:

arr[0] = {10, arr[0].b};

Thanks for the minimal bug reports!

from uclid.

Hi Elizabeth, thanks for the speedy reply!

Renaming the field might be a little complicated, as I'm translating user input so they're free to write whatever's legal in the source language (Murphi). I might have to just detect and reject input like this.

Thanks for the record work around. I think this is achievable, but I have to think more deeply about it. Murphi unfortunately allows arbitrary nesting here so a naive translation might produce things like a[0].b.c[2].d[3].

from uclid.

Ok, I'll aim to have a look at both the issues next week and let you know

from uclid.

I realized the work around for array assignment actually won't work for my use case. Coming from Murphi, the index can be a variable. E.g. the originating Murphi code might look like:

procedure foo(var r: complex_type_t; var i: 0..10); begin
  r[i].a := 10;
end;

I can't think of a way to translate this to Uclid5 other than some kind of 11-alternative if-then-else branch on the value of i. Obviously this also causes complications if i is not just a variable but a more complex expression like a call to an impure function. E.g. r[my_func()].a := 10.

Because this is all related to generated code from artificial test cases, I think you should probably ignore this issue for now. Maybe something to revisit if another user has a real world model that hits this problem.

from uclid.