agacek
commented
3 years ago Try using = instead of := for the struct fields.
On Sat, Jul 3, 2021 at 12:16 AM Verifier @.***> wrote:
I have two examples.
Example 1: type sPos_t = int[4]; const A : int = 1; const B : int = 2; const INVALID_SPOS : sPos_t = [A,B,A,B]; node main (inpu: sPos_t) returns (outp: bool); let outp = INVALID_SPOS[2] <> 0; --%PROPERTY outp; tel;
Example 2: type sPos_t = struct {iIdx: int; iAbs: int}; const A : int = -1; const B : int = 0; --const INVALID_SPOS : sPos_t = {A; B}; const INVALID_SPOS : sPos_t = {iIdx := A; iAbs := B}; node main (varia: sPos_t) returns(Outp: bool); let Outp = INVALID_SPOS.A > 0; --%PROPERTY Outp; tel;
The first example is correct, while the second example is wrong because the constant with struct type. In this situation, I do not care whether the property is valid or not.
In the grammar of Luster, it is ok. So, I was wondering if jkind supports the definition of constant with struct type. Or maybe it is my fault. Who can solve my question?
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/loonwerks/jkind/issues/62, or unsubscribe https://github.com/notifications/unsubscribe-auth/AABKBCEXH3CLWBMCHMIQJ63TV2MLZANCNFSM47XZAD7A .
verifierlife
I have two examples.
Example 1: type sPos_t = int[4]; const A : int = 1; const B : int = 2; const INVALID_SPOS : sPos_t = [A,B,A,B];
node main (inpu: sPos_t) returns (outp: bool); let outp = INVALID_SPOS[2] <> 0; --%PROPERTY outp; tel;
Example 2: type sPos_t = struct {iIdx: int; iAbs: int}; const A : int = -1; const B : int = 0; const INVALID_SPOS : sPos_t = {iIdx := A; iAbs := B}; --const INVALID_SPOS : sPos_t = {A; B};
node main (varia: sPos_t) returns(Outp: bool); let Outp = INVALID_SPOS.A > 0; --%PROPERTY Outp; tel;
The first example is correct, while the second example is wrong with the following error.
Parse error line 4:30 no viable alternative at input '{' const INVALID_SPOS : sPos_t = {iIdx := A; iAbs := B};Parse error line 4:42 extraneous input 'iAbs' expecting {<EOF>, 'const', 'node', 'type', 'function'} const INVALID_SPOS : sPos_t = {iIdx := A; iAbs := B};In the grammar of Luster, it is ok. In this situation, I do not care whether the property is valid or not. So, I was wondering if jkind supports the definition of constant with struct type. Or maybe I wrote the wrong sentence in example 2. Who can solve my question?