Skip to content

Commit 1a70f89

Browse files
Associate dynamic objects with respective language mode
1 parent 1b5b877 commit 1a70f89

File tree

1 file changed

+5
-3
lines changed

1 file changed

+5
-3
lines changed

src/goto-symex/symex_builtin_functions.cpp

+5-3
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,9 @@ void goto_symext::symex_allocate(
6666

6767
exprt size=code.op0();
6868
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;
6972

7073
// is the type given?
7174
if(code.type().id()==ID_pointer && code.type().subtype().id()!=ID_empty)
@@ -142,7 +145,7 @@ void goto_symext::symex_allocate(
142145
size_symbol.name="symex_dynamic::"+id2string(size_symbol.base_name);
143146
size_symbol.is_lvalue=true;
144147
size_symbol.type=tmp_size.type();
145-
size_symbol.mode=ID_C;
148+
size_symbol.mode = mode;
146149

147150
state.symbol_table.add(size_symbol);
148151

@@ -161,7 +164,7 @@ void goto_symext::symex_allocate(
161164
value_symbol.is_lvalue=true;
162165
value_symbol.type=object_type;
163166
value_symbol.type.set("#dynamic", true);
164-
value_symbol.mode=ID_C;
167+
value_symbol.mode = mode;
165168

166169
state.symbol_table.add(value_symbol);
167170

@@ -401,7 +404,6 @@ void goto_symext::symex_cpp_new(
401404

402405
if(code.type().id()!=ID_pointer)
403406
throw "new expected to return pointer";
404-
405407
do_array =
406408
(code.get(ID_statement) == ID_cpp_new_array ||
407409
code.get(ID_statement) == ID_java_new_array_data);

0 commit comments

Comments
 (0)