Skip to content

Commit 5aa449b

Browse files
authored
Merge pull request #606 from diffblue/use_verilog_module_source
Verilog typechecker now uses verilog_module_sourcet
2 parents 214a024 + cb9edcc commit 5aa449b

File tree

4 files changed

+31
-24
lines changed

4 files changed

+31
-24
lines changed

src/verilog/verilog_expr.h

Lines changed: 13 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1893,9 +1893,14 @@ to_verilog_assume_statement(verilog_statementt &statement)
18931893
class verilog_module_sourcet : public irept
18941894
{
18951895
public:
1896-
irep_idt name() const
1896+
irep_idt base_name() const
1897+
{
1898+
return get(ID_base_name);
1899+
}
1900+
1901+
void base_name(irep_idt base_name)
18971902
{
1898-
return get(ID_name);
1903+
return set(ID_base_name, base_name);
18991904
}
19001905

19011906
using parameter_port_listt = verilog_parameter_declt::declaratorst;
@@ -1930,10 +1935,15 @@ class verilog_module_sourcet : public irept
19301935
return (module_itemst &)(add(ID_module_items).get_sub());
19311936
}
19321937

1933-
const source_locationt &source_location()
1938+
const source_locationt &source_location() const
19341939
{
19351940
return static_cast<const source_locationt &>(find(ID_C_source_location));
19361941
}
1942+
1943+
source_locationt &add_source_location()
1944+
{
1945+
return static_cast<source_locationt &>(add(ID_C_source_location));
1946+
}
19371947
};
19381948

19391949
inline const verilog_module_sourcet &to_verilog_module_source(const irept &irep)

src/verilog/verilog_module.h

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -9,9 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
99
#ifndef CPROVER_VERILOG_MODULE_H
1010
#define CPROVER_VERILOG_MODULE_H
1111

12-
#include <string>
13-
14-
#include <util/expr.h>
12+
#include "verilog_expr.h"
1513

1614
struct verilog_modulet
1715
{
@@ -20,14 +18,15 @@ struct verilog_modulet
2018
exprt ports;
2119
exprt module_items;
2220
source_locationt location;
23-
24-
irept to_irep() const
21+
22+
verilog_module_sourcet to_irep() const
2523
{
26-
irept irep;
27-
irep.set(ID_name, name);
24+
verilog_module_sourcet irep;
25+
irep.base_name(name);
2826
irep.add(ID_parameter_port_list) = parameter_port_list;
2927
irep.add(ID_ports)=ports;
3028
irep.add(ID_module_items) = module_items;
29+
irep.add_source_location() = location;
3130
return irep;
3231
}
3332

src/verilog/verilog_typecheck.cpp

Lines changed: 11 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1837,7 +1837,7 @@ bool verilog_typecheck(
18371837
verilog_parse_treet::module_mapt::const_iterator it=
18381838
parse_tree.module_map.find(
18391839
id2string(verilog_module_name(module)));
1840-
1840+
18411841
if(it==parse_tree.module_map.end())
18421842
{
18431843
messaget message(message_handler);
@@ -1848,7 +1848,7 @@ bool verilog_typecheck(
18481848

18491849
return verilog_typecheck(
18501850
symbol_table,
1851-
it->second->verilog_module,
1851+
it->second->verilog_module.to_irep(),
18521852
parse_tree.standard,
18531853
message_handler);
18541854
}
@@ -1867,25 +1867,23 @@ Function: verilog_typecheck
18671867

18681868
bool verilog_typecheck(
18691869
symbol_table_baset &symbol_table,
1870-
const verilog_modulet &verilog_module,
1870+
const verilog_module_sourcet &verilog_module_source,
18711871
verilog_standardt standard,
18721872
message_handlert &message_handler)
18731873
{
18741874
// create symbol
18751875

1876-
symbolt symbol;
1876+
irep_idt base_name = verilog_module_source.base_name();
1877+
1878+
symbolt symbol{verilog_module_symbol(base_name), module_typet{}, ID_Verilog};
18771879

1878-
symbol.mode=ID_Verilog;
1879-
symbol.base_name=verilog_module.name;
1880-
symbol.type=module_typet();
1881-
symbol.name=verilog_module_symbol(verilog_module.name);
1882-
symbol.base_name=verilog_module.name;
1883-
symbol.pretty_name=verilog_module.name;
1880+
symbol.base_name = base_name;
1881+
symbol.pretty_name = base_name;
18841882
symbol.module=symbol.name;
1885-
symbol.location=verilog_module.location;
1883+
symbol.location = verilog_module_source.source_location();
1884+
1885+
symbol.type.add(ID_module_source) = verilog_module_source;
18861886

1887-
symbol.type.add(ID_module_source)=verilog_module.to_irep();
1888-
18891887
// put symbol in symbol_table
18901888

18911889
symbolt *new_symbol;

src/verilog/verilog_typecheck.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ bool verilog_typecheck(
2727

2828
bool verilog_typecheck(
2929
symbol_table_baset &,
30-
const verilog_modulet &verilog_module,
30+
const verilog_module_sourcet &verilog_module_source,
3131
verilog_standardt,
3232
message_handlert &message_handler);
3333

0 commit comments

Comments
 (0)