diff --git a/regression/smv/identifiers/complex_identifier1.desc b/regression/smv/identifiers/complex_identifier1.desc new file mode 100644 index 000000000..3d072e2a3 --- /dev/null +++ b/regression/smv/identifiers/complex_identifier1.desc @@ -0,0 +1,7 @@ +CORE +complex_identifier1.smv + +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/regression/smv/identifiers/complex_identifier1.smv b/regression/smv/identifiers/complex_identifier1.smv new file mode 100644 index 000000000..348ca30f6 --- /dev/null +++ b/regression/smv/identifiers/complex_identifier1.smv @@ -0,0 +1,12 @@ +MODULE main + +-- complex identifiers can use '[...]' and '.' +VAR some_var : boolean; +VAR some_var[3] : boolean; +VAR some_var[4].whatnot : boolean; +VAR some_var[5][2].whatnot : boolean; + +INIT some_var[5][2].whatnot + +-- spaces are ok +INIT some_var [4] . whatnot