diff --git a/regression/smv/define/define8.desc b/regression/smv/define/define8.desc new file mode 100644 index 000000000..5acb877bd --- /dev/null +++ b/regression/smv/define/define8.desc @@ -0,0 +1,8 @@ +CORE +define8.smv + +^file .* line 6: identifier x already used as enum$ +^EXIT=2$ +^SIGNAL=0$ +-- +-- diff --git a/regression/smv/define/define8.smv b/regression/smv/define/define8.smv new file mode 100644 index 000000000..911e2bc37 --- /dev/null +++ b/regression/smv/define/define8.smv @@ -0,0 +1,6 @@ +MODULE main + +VAR some_enum : {x, y, z}; + +-- x is already defined as an enum +DEFINE x := 123; diff --git a/regression/smv/var/already_declared5.desc b/regression/smv/var/already_declared5.desc index be316c863..96e218534 100644 --- a/regression/smv/var/already_declared5.desc +++ b/regression/smv/var/already_declared5.desc @@ -1,8 +1,8 @@ -KNOWNBUG +CORE already_declared5.smv +^file .* line 6: identifier x already used as enum$ ^EXIT=2$ ^SIGNAL=0$ -- -- -This crashes. diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index eb7cdc4ac..91a68783c 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -2137,6 +2137,9 @@ void smv_typecheckt::create_var_symbols( { const irep_idt mode = "SMV"; + // to catch variables that have the same name as enums + std::unordered_set enums; + for(const auto &item : items) { if(item.is_var() || item.is_ivar()) @@ -2144,6 +2147,13 @@ void smv_typecheckt::create_var_symbols( irep_idt base_name = to_smv_identifier_expr(item.expr).identifier(); irep_idt identifier = module + "::var::" + id2string(base_name); + // already used as enum? + if(enums.find(base_name) != enums.end()) + { + throw errort{}.with_location(item.expr.source_location()) + << "identifier " << base_name << " already used as enum"; + } + auto symbol_ptr = symbol_table.lookup(identifier); if(symbol_ptr != nullptr) { @@ -2185,6 +2195,13 @@ void smv_typecheckt::create_var_symbols( irep_idt base_name = identifier_expr.identifier(); irep_idt identifier = module + "::var::" + id2string(base_name); + // already used as enum? + if(enums.find(base_name) != enums.end()) + { + throw errort{}.with_location(identifier_expr.source_location()) + << "identifier " << base_name << " already used as enum"; + } + auto symbol_ptr = symbol_table.lookup(identifier); if(symbol_ptr != nullptr) { @@ -2226,6 +2243,8 @@ void smv_typecheckt::create_var_symbols( << "enum " << base_name << " already declared, at " << symbol_ptr->location; } + + enums.insert(base_name); } } }