From ed94b75f8fdcb4dbb73500d7a7c5a0041db95625 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 9 Feb 2025 09:13:36 +0000 Subject: [PATCH 1/2] whitespace only: alignment in SMV parser --- src/smvlang/parser.y | 58 ++++++++++++++++++++++---------------------- 1 file changed, 29 insertions(+), 29 deletions(-) diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y index 1d2269b1..5fda139f 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -477,39 +477,39 @@ defines: define ; define : assignment_var BECOMES_Token formula ';' -{ - const irep_idt &identifier=stack_expr($1).get(ID_identifier); - smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier]; + { + const irep_idt &identifier=stack_expr($1).get(ID_identifier); + smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier]; - switch(var.var_class) - { - case smv_parse_treet::mc_vart::UNKNOWN: - var.type.make_nil(); - var.var_class=smv_parse_treet::mc_vart::DEFINED; - break; + switch(var.var_class) + { + case smv_parse_treet::mc_vart::UNKNOWN: + var.type.make_nil(); + var.var_class=smv_parse_treet::mc_vart::DEFINED; + break; - case smv_parse_treet::mc_vart::DECLARED: - var.var_class=smv_parse_treet::mc_vart::DEFINED; - break; + case smv_parse_treet::mc_vart::DECLARED: + var.var_class=smv_parse_treet::mc_vart::DEFINED; + break; - case smv_parse_treet::mc_vart::DEFINED: - yyerror("variable `"+id2string(identifier)+"' already defined"); - YYERROR; - break; - - case smv_parse_treet::mc_vart::ARGUMENT: - yyerror("variable `"+id2string(identifier)+"' already declared as argument"); - YYERROR; - break; - - default: - DATA_INVARIANT(false, "unexpected variable class"); - } + case smv_parse_treet::mc_vart::DEFINED: + yyerror("variable `"+id2string(identifier)+"' already defined"); + YYERROR; + break; - binary($$, $1, ID_equal, $3); - PARSER.module->add_define(to_equal_expr(stack_expr($$))); -} -; + case smv_parse_treet::mc_vart::ARGUMENT: + yyerror("variable `"+id2string(identifier)+"' already declared as argument"); + YYERROR; + break; + + default: + DATA_INVARIANT(false, "unexpected variable class"); + } + + binary($$, $1, ID_equal, $3); + PARSER.module->add_define(to_equal_expr(stack_expr($$))); + } + ; formula : term ; From 35ecf21ee4f12f02a638fb78b05664279da6b275 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 9 Feb 2025 09:15:00 +0000 Subject: [PATCH 2/2] SMV: do not allow defining identifiers that are already declared VAR x : ... followed by DEFINE x := ... must be errored. --- regression/smv/assign/assign1.desc | 8 ++++++++ regression/smv/assign/assign1.smv | 8 ++++++++ regression/smv/assign/assign2.desc | 8 ++++++++ regression/smv/assign/assign2.smv | 8 ++++++++ regression/smv/define/define2.desc | 8 ++++++++ regression/smv/define/define2.smv | 6 ++++++ regression/smv/define/define3.desc | 8 ++++++++ regression/smv/define/define3.smv | 6 ++++++ regression/smv/define/define4.desc | 8 ++++++++ regression/smv/define/define4.smv | 6 ++++++ regression/smv/define/define5.desc | 8 ++++++++ regression/smv/define/define5.smv | 6 ++++++ regression/smv/define/define6.desc | 8 ++++++++ regression/smv/define/define6.smv | 6 ++++++ src/smvlang/parser.y | 3 ++- 15 files changed, 104 insertions(+), 1 deletion(-) create mode 100644 regression/smv/assign/assign1.desc create mode 100644 regression/smv/assign/assign1.smv create mode 100644 regression/smv/assign/assign2.desc create mode 100644 regression/smv/assign/assign2.smv create mode 100644 regression/smv/define/define2.desc create mode 100644 regression/smv/define/define2.smv create mode 100644 regression/smv/define/define3.desc create mode 100644 regression/smv/define/define3.smv create mode 100644 regression/smv/define/define4.desc create mode 100644 regression/smv/define/define4.smv create mode 100644 regression/smv/define/define5.desc create mode 100644 regression/smv/define/define5.smv create mode 100644 regression/smv/define/define6.desc create mode 100644 regression/smv/define/define6.smv diff --git a/regression/smv/assign/assign1.desc b/regression/smv/assign/assign1.desc new file mode 100644 index 00000000..f6dcdeaa --- /dev/null +++ b/regression/smv/assign/assign1.desc @@ -0,0 +1,8 @@ +KNOWNBUG +assign1.smv + +^file .* line 6: variable `x' already assigned.*$ +^EXIT=1$ +^SIGNAL=0$ +-- +-- diff --git a/regression/smv/assign/assign1.smv b/regression/smv/assign/assign1.smv new file mode 100644 index 00000000..34d4106f --- /dev/null +++ b/regression/smv/assign/assign1.smv @@ -0,0 +1,8 @@ +MODULE main + +VAR x : 1..4; + +ASSIGN x := 1; + +-- not allowed, x is already assigned +ASSIGN init(x) := 2; diff --git a/regression/smv/assign/assign2.desc b/regression/smv/assign/assign2.desc new file mode 100644 index 00000000..f6dcdeaa --- /dev/null +++ b/regression/smv/assign/assign2.desc @@ -0,0 +1,8 @@ +KNOWNBUG +assign1.smv + +^file .* line 6: variable `x' already assigned.*$ +^EXIT=1$ +^SIGNAL=0$ +-- +-- diff --git a/regression/smv/assign/assign2.smv b/regression/smv/assign/assign2.smv new file mode 100644 index 00000000..07aa9736 --- /dev/null +++ b/regression/smv/assign/assign2.smv @@ -0,0 +1,8 @@ +MODULE main + +VAR x : 1..4; + +ASSIGN x := 1; + +-- not allowed, x is already assigned +ASSIGN next(x) := 2; diff --git a/regression/smv/define/define2.desc b/regression/smv/define/define2.desc new file mode 100644 index 00000000..50db7600 --- /dev/null +++ b/regression/smv/define/define2.desc @@ -0,0 +1,8 @@ +CORE +define2.smv + +^file .* line 6: variable `x' already declared.*$ +^EXIT=1$ +^SIGNAL=0$ +-- +-- diff --git a/regression/smv/define/define2.smv b/regression/smv/define/define2.smv new file mode 100644 index 00000000..0ade6776 --- /dev/null +++ b/regression/smv/define/define2.smv @@ -0,0 +1,6 @@ +MODULE main + +VAR x : boolean; + +-- not allowed, x is already a variable +DEFINE x := TRUE; diff --git a/regression/smv/define/define3.desc b/regression/smv/define/define3.desc new file mode 100644 index 00000000..259caa10 --- /dev/null +++ b/regression/smv/define/define3.desc @@ -0,0 +1,8 @@ +CORE +define3.smv + +^file .* line 6: variable `x' already defined.*$ +^EXIT=1$ +^SIGNAL=0$ +-- +-- diff --git a/regression/smv/define/define3.smv b/regression/smv/define/define3.smv new file mode 100644 index 00000000..d7fbafa2 --- /dev/null +++ b/regression/smv/define/define3.smv @@ -0,0 +1,6 @@ +MODULE main + +DEFINE x := TRUE; + +-- not allowed, x is already defined +VAR x : boolean; diff --git a/regression/smv/define/define4.desc b/regression/smv/define/define4.desc new file mode 100644 index 00000000..fbc9008f --- /dev/null +++ b/regression/smv/define/define4.desc @@ -0,0 +1,8 @@ +CORE +define4.smv + +^file .* line 6: variable `x' already defined.*$ +^EXIT=1$ +^SIGNAL=0$ +-- +-- diff --git a/regression/smv/define/define4.smv b/regression/smv/define/define4.smv new file mode 100644 index 00000000..ec64a0c5 --- /dev/null +++ b/regression/smv/define/define4.smv @@ -0,0 +1,6 @@ +MODULE main + +DEFINE x := TRUE; + +-- not allowed, x is already defined +ASSIGN x := TRUE; diff --git a/regression/smv/define/define5.desc b/regression/smv/define/define5.desc new file mode 100644 index 00000000..59f7e567 --- /dev/null +++ b/regression/smv/define/define5.desc @@ -0,0 +1,8 @@ +KNOWNBUG +define5.smv + +^file .* line 6: variable `x' already defined.*$ +^EXIT=1$ +^SIGNAL=0$ +-- +-- diff --git a/regression/smv/define/define5.smv b/regression/smv/define/define5.smv new file mode 100644 index 00000000..8f012eaf --- /dev/null +++ b/regression/smv/define/define5.smv @@ -0,0 +1,6 @@ +MODULE main + +DEFINE x := TRUE; + +-- not allowed, x is already defined +ASSIGN next(x) := TRUE; diff --git a/regression/smv/define/define6.desc b/regression/smv/define/define6.desc new file mode 100644 index 00000000..24cafa27 --- /dev/null +++ b/regression/smv/define/define6.desc @@ -0,0 +1,8 @@ +KNOWNBUG +define6.smv + +^file .* line 6: variable `x' already defined.*$ +^EXIT=1$ +^SIGNAL=0$ +-- +-- diff --git a/regression/smv/define/define6.smv b/regression/smv/define/define6.smv new file mode 100644 index 00000000..9b6b8f45 --- /dev/null +++ b/regression/smv/define/define6.smv @@ -0,0 +1,6 @@ +MODULE main + +DEFINE x := TRUE; + +-- not allowed, x is already defined +ASSIGN init(x) := TRUE; diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y index 5fda139f..982484b6 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -489,7 +489,8 @@ define : assignment_var BECOMES_Token formula ';' break; case smv_parse_treet::mc_vart::DECLARED: - var.var_class=smv_parse_treet::mc_vart::DEFINED; + yyerror("variable `"+id2string(identifier)+"' already declared"); + YYERROR; break; case smv_parse_treet::mc_vart::DEFINED: