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(
114114 if (expr.id () == ID_symbol)
115115 {
116116 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 ())
121118 INVARIANT (
122- comments. at (ID_C_base_name).id () == symbol.base_name ,
119+ expr. find (ID_C_base_name).id () == symbol.base_name ,
123120 " base_name comment does not match symbol's base_name" );
124121 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 ));
127123 }
128124 }
129125 };
You can’t perform that action at this time.
0 commit comments