Skip to content

Commit e9df10b

Browse files
author
Daniel Kroening
committed
codet now inherits from irept
1 parent c2d2070 commit e9df10b

18 files changed

+244
-105
lines changed

‎src/ansi-c/c_typecheck_code.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -31,8 +31,6 @@ void c_typecheck_baset::typecheck_code(codet &code)
3131
throw 0;
3232
}
3333

34-
code.type() = empty_typet();
35-
3634
const irep_idt &statement=code.get_statement();
3735

3836
if(statement==ID_expression)

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -772,7 +772,7 @@ void c_typecheck_baset::typecheck_expr_operands(exprt &expr)
772772
code_declt decl(symbol.symbol_expr());
773773
decl.add_source_location()=declaration.source_location();
774774

775-
expr.op0()=decl;
775+
expr.get_sub()[0] = decl;
776776

777777
typecheck_expr(expr.op1());
778778
}
@@ -990,7 +990,7 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
990990
ID_statement_expression, void_type(), expr.source_location());
991991
auto decl_block=code_blockt::from_list(clean_code);
992992
decl_block.set_statement(ID_decl_block);
993-
side_effect_expr.copy_to_operands(decl_block);
993+
side_effect_expr.get_sub().push_back(decl_block);
994994
clean_code.clear();
995995

996996
// We merge the side-effect into the operand of the typecast,
@@ -1047,7 +1047,7 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
10471047
ID_statement_expression, void_type(), expr.source_location());
10481048
auto decl_block=code_blockt::from_list(clean_code);
10491049
decl_block.set_statement(ID_decl_block);
1050-
side_effect_expr.copy_to_operands(decl_block);
1050+
side_effect_expr.get_sub().push_back(decl_block);
10511051
clean_code.clear();
10521052

10531053
// We merge the side-effect into the operand of the typecast,

‎src/cpp/cpp_destructor.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -64,7 +64,7 @@ optionalt<codet> cpp_typecheckt::cpp_destructor(
6464

6565
auto i_code = cpp_destructor(source_location, index);
6666
if(i_code.has_value())
67-
new_code.add_to_operands(std::move(i_code.value()));
67+
new_code.add(std::move(i_code.value()));
6868
}
6969

7070
return std::move(new_code);

‎src/cpp/cpp_typecheck_code.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -25,12 +25,10 @@ void cpp_typecheckt::typecheck_code(codet &code)
2525

2626
if(statement==ID_try_catch)
2727
{
28-
code.type() = empty_typet();
2928
typecheck_try_catch(code);
3029
}
3130
else if(statement==ID_member_initializer)
3231
{
33-
code.type() = empty_typet();
3432
typecheck_member_initializer(code);
3533
}
3634
else if(statement==ID_msc_if_exists ||

‎src/cpp/cpp_typecheck_compound_type.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -671,14 +671,16 @@ void cpp_typecheckt::typecheck_compound_declarator(
671671
exprt already_typechecked(ID_already_typechecked);
672672
already_typechecked.add_to_operands(std::move(expr_call));
673673

674-
func_symb.value = code_returnt(already_typechecked).make_block();
674+
func_symb.value =
675+
code_returnt(already_typechecked).make_block().as_expr();
675676
}
676677
else
677678
{
678679
exprt already_typechecked(ID_already_typechecked);
679680
already_typechecked.add_to_operands(std::move(expr_call));
680681

681-
func_symb.value = code_expressiont(already_typechecked).make_block();
682+
func_symb.value =
683+
code_expressiont(already_typechecked).make_block().as_expr();
682684
}
683685

684686
// add this new function to the list of components

‎src/cpp/cpp_typecheck_constructor.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ static void copy_parent(
4747
code_assignt code(dereference_exprt(op0), op1);
4848
code.add_source_location() = source_location;
4949

50-
block.operands().push_back(code);
50+
block.operands().push_back(code.as_expr());
5151
}
5252

5353
/// Generate code to copy the member.
@@ -76,7 +76,7 @@ static void copy_member(
7676
code_expressiont code(assign);
7777
code.add_source_location() = source_location;
7878

79-
block.operands().push_back(code);
79+
block.operands().push_back(code.as_expr());
8080
}
8181

8282
/// Generate code to copy the member.
@@ -113,7 +113,7 @@ static void copy_array(
113113
code_expressiont code(assign);
114114
code.add_source_location() = source_location;
115115

116-
block.operands().push_back(code);
116+
block.operands().push_back(code.as_expr());
117117
}
118118

119119
/// Generate code for implicit default constructors
@@ -579,6 +579,7 @@ void cpp_typecheckt::full_member_initialization(
579579

580580
code_ifthenelset cond(
581581
cpp_namet("@most_derived").as_expr(), std::move(block));
582+
582583
final_initializers.move_to_sub(cond);
583584
}
584585

‎src/cpp/cpp_typecheck_declaration.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -173,7 +173,7 @@ void cpp_typecheckt::convert_non_template_declaration(
173173
declarator.init_args().operands());
174174

175175
if(constructor.has_value())
176-
symbol.value = constructor.value();
176+
symbol.value = constructor.value().as_expr();
177177
else
178178
symbol.value = nil_exprt();
179179
}

‎src/cpp/cpp_typecheck_function.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,7 @@ void cpp_typecheckt::convert_function(symbolt &symbol)
104104
!symbol.value.has_operands() || !symbol.value.op0().has_operands() ||
105105
symbol.value.op0().op0().id() != ID_already_typechecked)
106106
{
107-
symbol.value.copy_to_operands(dtor(msymb));
107+
symbol.value.copy_to_operands(dtor(msymb).as_expr());
108108
}
109109
}
110110

‎src/cpp/cpp_typecheck_initializer.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -183,7 +183,7 @@ void cpp_typecheckt::convert_initializer(symbolt &symbol)
183183
cpp_constructor(symbol.value.source_location(), expr_symbol, ops);
184184

185185
if(constructor.has_value())
186-
symbol.value = constructor.value();
186+
symbol.value = constructor.value().as_expr();
187187
else
188188
symbol.value = nil_exprt();
189189
}
@@ -310,7 +310,7 @@ void cpp_typecheckt::zero_initializer(
310310
already_typechecked(assign.lhs());
311311

312312
typecheck_code(assign);
313-
ops.push_back(assign);
313+
ops.push_back(assign.as_expr());
314314
}
315315
else
316316
{
@@ -331,6 +331,6 @@ void cpp_typecheckt::zero_initializer(
331331
already_typechecked(assign.lhs());
332332

333333
typecheck_code(assign);
334-
ops.push_back(assign);
334+
ops.push_back(assign.as_expr());
335335
}
336336
}

‎src/cpp/expr2cpp.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -398,15 +398,15 @@ std::string expr2cppt::convert_code(
398398
const codet &src,
399399
unsigned indent)
400400
{
401-
const irep_idt &statement=src.get(ID_statement);
401+
const irep_idt &statement = src.get_statement();
402402

403403
if(statement==ID_cpp_delete ||
404404
statement==ID_cpp_delete_array)
405-
return convert_code_cpp_delete(src, indent);
405+
return convert_code_cpp_delete(src.as_expr(), indent);
406406

407407
if(statement==ID_cpp_new ||
408408
statement==ID_cpp_new_array)
409-
return convert_cpp_new(src, indent);
409+
return convert_cpp_new(src.as_expr(), indent);
410410

411411
return expr2ct::convert_code(src, indent);
412412
}

‎src/cpp/parse.cpp

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -2710,7 +2710,7 @@ bool Parser::rConstructorDecl(
27102710
{
27112711
case TOK_INTEGER:
27122712
{
2713-
constructor.value()=codet("cpp-pure-virtual");
2713+
constructor.value() = exprt("cpp-pure-virtual");
27142714
set_location(constructor.value(), value);
27152715
}
27162716
break;
@@ -2723,7 +2723,7 @@ bool Parser::rConstructorDecl(
27232723
return false;
27242724
}
27252725

2726-
constructor.value()=codet(ID_default);
2726+
constructor.value() = exprt(ID_default);
27272727
set_location(constructor.value(), value);
27282728
}
27292729
break;
@@ -2736,7 +2736,7 @@ bool Parser::rConstructorDecl(
27362736
return false;
27372737
}
27382738

2739-
constructor.value()=codet(ID_cpp_delete);
2739+
constructor.value() = exprt(ID_cpp_delete);
27402740
set_location(constructor.value(), value);
27412741
}
27422742
break;
@@ -2901,7 +2901,7 @@ bool Parser::rDeclaratorWithInit(
29012901
}
29022902

29032903
lex.get_token(tk);
2904-
declarator.value()=codet(ID_default);
2904+
declarator.value() = exprt(ID_default);
29052905
set_location(declarator.value(), tk);
29062906
}
29072907
else if(lex.LookAhead(0)==TOK_DELETE) // C++0x
@@ -2913,7 +2913,7 @@ bool Parser::rDeclaratorWithInit(
29132913
}
29142914

29152915
lex.get_token(tk);
2916-
declarator.value()=codet(ID_cpp_delete);
2916+
declarator.value() = exprt(ID_cpp_delete);
29172917
set_location(declarator.value(), tk);
29182918
}
29192919
else
@@ -3411,7 +3411,7 @@ bool Parser::rMemberInit(exprt &init)
34113411
std::cout << std::string(__indent, ' ') << "Parser::rMemberInit 2\n";
34123412
#endif
34133413

3414-
init=codet(ID_member_initializer);
3414+
init = exprt(ID_member_initializer);
34153415
init.add(ID_member).swap(name);
34163416

34173417
cpp_tokent tk1, tk2;
@@ -6575,7 +6575,7 @@ bool Parser::rMSC_if_existsStatement(codet &code)
65756575
if(lex.get_token(tk2)!='{')
65766576
return false;
65776577

6578-
codet block;
6578+
code_blockt block;
65796579

65806580
while(lex.LookAhead(0)!='}')
65816581
{
@@ -6584,7 +6584,7 @@ bool Parser::rMSC_if_existsStatement(codet &code)
65846584
if(!rStatement(statement))
65856585
return false;
65866586

6587-
block.add_to_operands(std::move(statement));
6587+
block.add(std::move(statement));
65886588
}
65896589

65906590
if(lex.get_token(tk2)!='}')
@@ -7187,7 +7187,7 @@ bool Parser::rFunctionBody(cpp_declaratort &declarator)
71877187
if(lex.get_token(cb)!='}')
71887188
return false;
71897189

7190-
declarator.value()=body;
7190+
declarator.value() = body.as_expr();
71917191
return true;
71927192
}
71937193
else
@@ -7203,7 +7203,7 @@ bool Parser::rFunctionBody(cpp_declaratort &declarator)
72037203
return false;
72047204
}
72057205

7206-
declarator.value()=body;
7206+
declarator.value() = body.as_expr();
72077207

72087208
current_function.clear();
72097209

@@ -7827,7 +7827,7 @@ bool Parser::rTryStatement(codet &statement)
78277827

78287828
assert(body.get_statement()==ID_block);
78297829

7830-
body.operands().insert(body.operands().begin(), catch_op);
7830+
body.operands().insert(body.operands().begin(), catch_op.as_expr());
78317831

78327832
statement.add_to_operands(std::move(body));
78337833
}

‎src/goto-symex/goto_symex.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -219,6 +219,7 @@ class goto_symext
219219
// c) clean up byte_extract on the lhs of an assignment
220220
void clean_expr(
221221
exprt &, statet &, bool write);
222+
void clean_expr(codet &, statet &, bool write);
222223

223224
void trigger_auto_object(const exprt &, statet &);
224225
void initialize_auto_object(const exprt &, statet &);
@@ -408,7 +409,7 @@ class goto_symext
408409
statet &, const exprt &lhs, const side_effect_exprt &);
409410
virtual void symex_fkt(statet &, const code_function_callt &);
410411
virtual void symex_trace(statet &, const code_function_callt &);
411-
virtual void symex_printf(statet &, const exprt &rhs);
412+
virtual void symex_printf(statet &, const irept &);
412413
virtual void symex_input(statet &, const codet &);
413414
virtual void symex_output(statet &, const codet &);
414415

‎src/goto-symex/symex_builtin_functions.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -302,12 +302,11 @@ irep_idt get_string_argument(const exprt &src, const namespacet &ns)
302302
return get_string_argument_rec(tmp);
303303
}
304304

305-
void goto_symext::symex_printf(
306-
statet &state,
307-
const exprt &rhs)
305+
void goto_symext::symex_printf(statet &state, const irept &rhs)
308306
{
309-
PRECONDITION(!rhs.operands().empty());
307+
//PRECONDITION(!rhs.operands().empty());
310308

309+
#if 0
311310
exprt tmp_rhs=rhs;
312311
state.rename(tmp_rhs, ns);
313312
do_simplify(tmp_rhs);
@@ -325,6 +324,7 @@ void goto_symext::symex_printf(
325324
target.output_fmt(
326325
state.guard.as_expr(),
327326
state.source, "printf", format_string, args);
327+
#endif
328328
}
329329

330330
void goto_symext::symex_input(

‎src/jsil/jsil_entry_point.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ static void create_initialize(symbol_tablet &symbol_table)
3838
code_assignt a(rounding_mode, from_integer(0, rounding_mode.type()));
3939
init_code.add(a);
4040

41-
initialize.value=init_code;
41+
initialize.value = init_code.as_expr();
4242

4343
if(symbol_table.add(initialize))
4444
throw "failed to add " INITIALIZE_FUNCTION;

‎src/jsil/parser.y

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -210,7 +210,7 @@ statements: statement
210210

211211
statement: TOK_NEWLINE
212212
{
213-
newstack($$)=code_skipt();
213+
newstack($$)=code_skipt().as_expr();
214214
}
215215
| instruction TOK_NEWLINE
216216
{
@@ -241,7 +241,7 @@ instruction: TOK_LABEL TOK_IDENTIFIER
241241
}
242242
| TOK_SKIP
243243
{
244-
newstack($$)=code_skipt();
244+
newstack($$)=code_skipt().as_expr();
245245
}
246246
| TOK_IDENTIFIER TOK_DEFEQ rhs
247247
{

‎src/linking/static_lifetime_init.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -109,10 +109,8 @@ void static_lifetime_init(
109109

110110
symbolt &init_symbol = symbol_table.get_writeable_ref(INITIALIZE_FUNCTION);
111111

112-
init_symbol.value=code_blockt();
113-
init_symbol.value.add_source_location()=source_location;
114-
115-
code_blockt &dest=to_code_block(to_code(init_symbol.value));
112+
code_blockt dest;
113+
dest.add_source_location() = source_location;
116114

117115
// add the magic label to hide
118116
dest.add(code_labelt(CPROVER_PREFIX "HIDE", code_skipt()));
@@ -164,4 +162,6 @@ void static_lifetime_init(
164162
dest.add(function_call);
165163
}
166164
}
165+
166+
init_symbol.value = dest.as_expr();
167167
}

0 commit comments

Comments
 (0)