ClemsonRSRG/RESOLVE — pull request #141 by Welchd1 (2014-11-14 19:50:54+00:00)
Title: temporary fix for initialization assignment statements (involves sideste...

Given a piece of code with an initialization like the following,

Type Stack is represented by Record
Contents: Array 1..Max_Depth of Entry;
Top: Integer;
end;
convention
1 <= S.Top <= Max_Depth + 1;
correspondence
Conc.S = Reverse(Iterated_Concatenation(1, S.Top-1,
lambda(i : Z).()));
initialization
S.Top := 1;
end;
end;

the Java translator will now generate the following correct initialization code:

class Stack_Rep {
Static_Array_Template.Static_Array Contents;
Integer_Template.Integer Top;

Stack_Rep() {
Contents = _Contents_Array_Fac_1.createStatic_Array();
Top = Std_Integer_Fac.createInteger();
Std_Integer_Fac.assign(Top, Std_Integer_Fac.createInteger(1));
}
...
}

Prior to the changes proposed here, the translator would (understandably) consider the lhs of "S.Top := 1" a
VariableDotExp and generate the corresponding, normally correct code:

Std_Integer_Fac.assign(((Init_Array_Realiz.Stack)S).rep.Top, Std_Integer_Fac.createInteger(1));

However, unlike the source, there is no S in anywhere in our Java representation (Stack_Rep) resulting in a Java error. There are a couple things I'll look at beyond this pull request:

1. Tweaking the Java code model: This is most preferable to me, however I don't think there is a way to do so (maybe somehow adding S as a field to Stack_Rep?) without running into infinite constructor invocation issues.

2. Come up with initialization clauses where a variable dot expression -- this type of output: ((Init_Array_Realiz.Stack)S).rep.Top -- will actually be needed in the constructor for Stack_Rep.