The declaration of a constant with struct type
Closed this issue · 4 comments
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?
It does not work.
Even I try to use the following cases:
--const INVALID_SPOS : sPos_t = {iIdx = A; iAbs = B};
--const INVALID_SPOS : sPos_t = {A; B};
--const INVALID_SPOS : sPos_t = {A, B};
--const INVALID_SPOS : sPos_t = {iIdx := A; iAbs := B};
--const INVALID_SPOS : sPos_t = {iIdx : A; iAbs : B};
--const INVALID_SPOS : sPos_t = {iIdx = A, iAbs = B};
--const INVALID_SPOS : sPos_t = {iIdx := A, iAbs := B};
const INVALID_SPOS : sPos_t = {iIdx : A, iAbs : B};
Actually, they all failed.
Thanks a lot.