File tree Expand file tree Collapse file tree 1 file changed +3
-7
lines changed Expand file tree Collapse file tree 1 file changed +3
-7
lines changed Original file line number Diff line number Diff line change @@ -114,16 +114,12 @@ void convert(
114
114
if (expr.id () == ID_symbol)
115
115
{
116
116
const symbolt &symbol = ns.lookup (expr.get (ID_identifier));
117
- // Don't break sharing unless need to write to it
118
- const irept::named_subt &comments =
119
- static_cast <const exprt &>(expr).get_comments ();
120
- if (comments.count (ID_C_base_name) != 0 )
117
+ if (expr.find (ID_C_base_name).is_not_nil ())
121
118
INVARIANT (
122
- comments. at (ID_C_base_name).id () == symbol.base_name ,
119
+ expr. find (ID_C_base_name).id () == symbol.base_name ,
123
120
" base_name comment does not match symbol's base_name" );
124
121
else
125
- expr.get_comments ().emplace (
126
- ID_C_base_name, irept (symbol.base_name ));
122
+ expr.add (ID_C_base_name, irept (symbol.base_name ));
127
123
}
128
124
}
129
125
};
You can’t perform that action at this time.
0 commit comments