diff --git a/regression/verilog/functioncall/named_block1.desc b/regression/verilog/functioncall/named_block1.desc index 883cc6df4..17a4bf380 100644 --- a/regression/verilog/functioncall/named_block1.desc +++ b/regression/verilog/functioncall/named_block1.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE named_block1.sv ^\[.*\] always main\.foo\(\) == 123: PROVED$ diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 493dd1008..73a1224e3 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -273,9 +273,11 @@ void verilog_typecheckt::convert_function_or_task(verilog_declt &decl) { irep_idt decl_class=decl.get_class(); - const std::string identifier= - id2string(module_identifier)+"."+ - id2string(decl.get_identifier()); + // the base name of the function/task + auto base_name = decl.get_identifier(); + + const std::string identifier = + id2string(module_identifier) + "." + id2string(base_name); auto result=symbol_table.get_writeable(identifier); @@ -292,11 +294,18 @@ void verilog_typecheckt::convert_function_or_task(verilog_declt &decl) function_or_task_name = symbol.name; + // function/tasks have an implicit named block with the name + // of the function + + named_blocks.push_back(id2string(base_name) + "."); + for(auto &inner_decl : decl.declarations()) convert_decl(inner_decl); convert_statement(decl.body()); + named_blocks.pop_back(); + function_or_task_name=""; symbol.value=decl.body(); @@ -336,6 +345,11 @@ exprt verilog_typecheckt::elaborate_constant_function_call( function_or_task_name = function_symbol.name; + // function/tasks have an implicit named block with the name + // of the function + + named_blocks.push_back(id2string(function_symbol.base_name) + "."); + for(auto &inner_decl : decl.declarations()) convert_decl(inner_decl); @@ -380,6 +394,8 @@ exprt verilog_typecheckt::elaborate_constant_function_call( // interpret it verilog_interpreter(decl.body()); + named_blocks.pop_back(); + function_or_task_name=""; // get return value @@ -429,16 +445,9 @@ void verilog_typecheckt::convert_decl(verilog_declt &decl) named_block = named_blocks.back(); // fix the type and identifier - irep_idt full_identifier; - - if(!function_or_task_name.empty()) - full_identifier = id2string(function_or_task_name) + "." + - id2string(named_block) + - id2string(declarator.base_name()); - else - full_identifier = id2string(module_identifier) + "." + - id2string(named_block) + - id2string(declarator.base_name()); + auto full_identifier = id2string(module_identifier) + "." + + id2string(named_block) + + id2string(declarator.base_name()); symbolt &symbol = symbol_table_lookup(full_identifier); declarator.type() = symbol.type; diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index cdca2a721..d98306f62 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -1177,24 +1177,10 @@ exprt verilog_typecheck_exprt::convert_symbol( { const irep_idt &identifier = expr.get_identifier(); - std::string full_identifier; - - // in a task or function? Try local ones first if(function_or_task_name!="") - { - full_identifier= - id2string(function_or_task_name)+ - "."+id2string(identifier); - - const symbolt *symbol; - if(!ns.lookup(full_identifier, symbol)) - { // found! - expr.type()=symbol->type; - expr.set_identifier(full_identifier); - return std::move(expr); - } - } - + DATA_INVARIANT(!named_blocks.empty(), "must have named block"); + + std::string full_identifier; std::string named_block; // try named blocks, beginning with inner one