File tree 1 file changed +5
-2
lines changed
1 file changed +5
-2
lines changed Original file line number Diff line number Diff line change @@ -66,6 +66,9 @@ void goto_symext::symex_allocate(
66
66
67
67
exprt size=code.op0 ();
68
68
typet object_type=nil_typet ();
69
+ auto function_symbol = outer_symbol_table.lookup (state.source .pc ->function );
70
+ INVARIANT (function_symbol, " function associated with instruction not found" );
71
+ const irep_idt &mode = function_symbol->mode ;
69
72
70
73
// is the type given?
71
74
if (code.type ().id ()==ID_pointer && code.type ().subtype ().id ()!=ID_empty)
@@ -142,7 +145,7 @@ void goto_symext::symex_allocate(
142
145
size_symbol.name =" symex_dynamic::" +id2string (size_symbol.base_name );
143
146
size_symbol.is_lvalue =true ;
144
147
size_symbol.type =tmp_size.type ();
145
- size_symbol.mode =ID_C ;
148
+ size_symbol.mode = mode ;
146
149
147
150
state.symbol_table .add (size_symbol);
148
151
@@ -161,7 +164,7 @@ void goto_symext::symex_allocate(
161
164
value_symbol.is_lvalue =true ;
162
165
value_symbol.type =object_type;
163
166
value_symbol.type .set (" #dynamic" , true );
164
- value_symbol.mode =ID_C ;
167
+ value_symbol.mode = mode ;
165
168
166
169
state.symbol_table .add (value_symbol);
167
170
You can’t perform that action at this time.
0 commit comments