diff --git a/jbmc/src/java_bytecode/assignments_from_json.cpp b/jbmc/src/java_bytecode/assignments_from_json.cpp index 27c245224997..ecc1d3450d62 100644 --- a/jbmc/src/java_bytecode/assignments_from_json.cpp +++ b/jbmc/src/java_bytecode/assignments_from_json.cpp @@ -16,11 +16,11 @@ Author: Diffblue Ltd. #include #include -#include - #include #include +#include + #include "ci_lazy_methods_needed.h" #include "code_with_references.h" #include "java_static_initializers.h" diff --git a/src/ansi-c/goto-conversion/builtin_functions.cpp b/src/ansi-c/goto-conversion/builtin_functions.cpp index 9277593a30e1..67c263793c2d 100644 --- a/src/ansi-c/goto-conversion/builtin_functions.cpp +++ b/src/ansi-c/goto-conversion/builtin_functions.cpp @@ -38,16 +38,16 @@ void goto_convertt::do_prob_uniform( const irep_idt &identifier = function.get_identifier(); // make it a side effect if there is an LHS - if(arguments.size()!=2) + if(arguments.size() != 2) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have two arguments" << eom; throw 0; } if(lhs.is_nil()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have LHS" << eom; throw 0; } @@ -55,27 +55,26 @@ void goto_convertt::do_prob_uniform( auto rhs = side_effect_exprt("prob_uniform", lhs.type(), function.source_location()); - if(lhs.type().id()!=ID_unsignedbv && - lhs.type().id()!=ID_signedbv) + if(lhs.type().id() != ID_unsignedbv && lhs.type().id() != ID_signedbv) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected other type" << eom; throw 0; } - if(arguments[0].type().id()!=lhs.type().id() || - arguments[1].type().id()!=lhs.type().id()) + if( + arguments[0].type().id() != lhs.type().id() || + arguments[1].type().id() != lhs.type().id()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected operands to be of same type as LHS" << eom; throw 0; } - if(!arguments[0].is_constant() || - !arguments[1].is_constant()) + if(!arguments[0].is_constant() || !arguments[1].is_constant()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected operands to be constant literals" << eom; throw 0; @@ -87,14 +86,14 @@ void goto_convertt::do_prob_uniform( to_integer(to_constant_expr(arguments[0]), lb) || to_integer(to_constant_expr(arguments[1]), ub)) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "error converting operands" << eom; throw 0; } if(lb > ub) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "expected lower bound to be smaller or equal to the " << "upper bound" << eom; throw 0; @@ -103,7 +102,7 @@ void goto_convertt::do_prob_uniform( rhs.add_to_operands(exprt{arguments[0]}, exprt{arguments[1]}); code_assignt assignment(lhs, rhs); - assignment.add_source_location()=function.source_location(); + assignment.add_source_location() = function.source_location(); copy(assignment, ASSIGN, dest); } @@ -116,32 +115,32 @@ void goto_convertt::do_prob_coin( const irep_idt &identifier = function.get_identifier(); // make it a side effect if there is an LHS - if(arguments.size()!=2) + if(arguments.size() != 2) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have two arguments" << eom; throw 0; } if(lhs.is_nil()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have LHS" << eom; throw 0; } side_effect_exprt rhs("prob_coin", lhs.type(), function.source_location()); - if(lhs.type()!=bool_typet()) + if(lhs.type() != bool_typet()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected bool" << eom; throw 0; } if(arguments[0].type().id() != ID_unsignedbv || !arguments[0].is_constant()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected first operand to be " << "a constant literal of type unsigned long" << eom; throw 0; @@ -161,21 +160,21 @@ void goto_convertt::do_prob_coin( to_integer(to_constant_expr(arguments[0]), num) || to_integer(to_constant_expr(arguments[1]), den)) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "error converting operands" << eom; throw 0; } - if(num-den > mp_integer(0)) + if(num - den > mp_integer(0)) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "probability has to be smaller than 1" << eom; throw 0; } if(den == mp_integer(0)) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "denominator may not be zero" << eom; throw 0; } @@ -186,7 +185,7 @@ void goto_convertt::do_prob_coin( rhs.copy_to_operands(from_rational(prob)); code_assignt assignment(lhs, rhs); - assignment.add_source_location()=function.source_location(); + assignment.add_source_location() = function.source_location(); copy(assignment, ASSIGN, dest); } @@ -212,11 +211,11 @@ void goto_convertt::do_scanf( { const irep_idt &f_id = function.get_identifier(); - if(f_id==CPROVER_PREFIX "scanf") + if(f_id == CPROVER_PREFIX "scanf") { if(arguments.empty()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "scanf takes at least one argument" << eom; throw 0; } @@ -226,10 +225,10 @@ void goto_convertt::do_scanf( if(!get_string_constant(arguments[0], format_string)) { // use our model - format_token_listt token_list= + format_token_listt token_list = parse_format_string(id2string(format_string)); - std::size_t argument_number=1; + std::size_t argument_number = 1; for(const auto &t : token_list) { @@ -237,7 +236,7 @@ void goto_convertt::do_scanf( if(type.has_value()) { - if(argument_numberid() == ID_array) { - #if 0 +#if 0 // A string. We first need a nondeterministic size. exprt size=side_effect_expr_nondett(size_type()); to_array_type(*type).size()=size; @@ -269,16 +268,16 @@ void goto_convertt::do_scanf( function.source_location(); copy(array_copy_statement, OTHER, dest); - #else +#else const index_exprt new_lhs( dereference_exprt{ptr}, from_integer(0, c_index_type())); const side_effect_expr_nondett rhs( to_array_type(*type).element_type(), function.source_location()); code_assignt assign(new_lhs, rhs); - assign.add_source_location()=function.source_location(); + assign.add_source_location() = function.source_location(); copy(assign, ASSIGN, dest); - #endif +#endif } else { @@ -287,7 +286,7 @@ void goto_convertt::do_scanf( const side_effect_expr_nondett rhs( *type, function.source_location()); code_assignt assign(new_lhs, rhs); - assign.add_source_location()=function.source_location(); + assign.add_source_location() = function.source_location(); copy(assign, ASSIGN, dest); } } @@ -298,7 +297,7 @@ void goto_convertt::do_scanf( { // we'll just do nothing code_function_callt function_call(lhs, function, arguments); - function_call.add_source_location()=function.source_location(); + function_call.add_source_location() = function.source_location(); copy(function_call, FUNCTION_CALL, dest); } @@ -312,9 +311,9 @@ void goto_convertt::do_input( const exprt::operandst &arguments, goto_programt &dest) { - if(arguments.size()<2) + if(arguments.size() < 2) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "input takes at least two arguments" << eom; throw 0; } @@ -327,9 +326,9 @@ void goto_convertt::do_output( const exprt::operandst &arguments, goto_programt &dest) { - if(arguments.size()<2) + if(arguments.size() < 2) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "output takes at least two arguments" << eom; throw 0; } @@ -345,14 +344,14 @@ void goto_convertt::do_atomic_begin( { if(lhs.is_not_nil()) { - error().source_location=lhs.find_source_location(); + error().source_location = lhs.find_source_location(); error() << "atomic_begin does not expect an LHS" << eom; throw 0; } if(!arguments.empty()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "atomic_begin takes no arguments" << eom; throw 0; } @@ -368,14 +367,14 @@ void goto_convertt::do_atomic_end( { if(lhs.is_not_nil()) { - error().source_location=lhs.find_source_location(); + error().source_location = lhs.find_source_location(); error() << "atomic_end does not expect an LHS" << eom; throw 0; } if(!arguments.empty()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "atomic_end takes no arguments" << eom; throw 0; } @@ -390,16 +389,15 @@ void goto_convertt::do_cpp_new( { if(lhs.is_nil()) { - error().source_location=lhs.find_source_location(); + error().source_location = lhs.find_source_location(); error() << "do_cpp_new without lhs is yet to be implemented" << eom; throw 0; } // build size expression - exprt object_size= - static_cast(rhs.find(ID_sizeof)); + exprt object_size = static_cast(rhs.find(ID_sizeof)); - bool new_array=rhs.get(ID_statement)==ID_cpp_new_array; + bool new_array = rhs.get(ID_statement) == ID_cpp_new_array; exprt count; @@ -418,14 +416,12 @@ void goto_convertt::do_cpp_new( if(rhs.operands().empty()) // no, "regular" one { // call __new or __new_array - exprt new_symbol= - ns.lookup(new_array?"__new_array":"__new").symbol_expr(); + exprt new_symbol = + ns.lookup(new_array ? "__new_array" : "__new").symbol_expr(); - const code_typet &code_type= - to_code_type(new_symbol.type()); + const code_typet &code_type = to_code_type(new_symbol.type()); - const typet &return_type= - code_type.return_type(); + const typet &return_type = code_type.return_type(); DATA_INVARIANT( code_type.parameters().size() == 1 || code_type.parameters().size() == 2, @@ -434,7 +430,7 @@ void goto_convertt::do_cpp_new( const symbolt &tmp_symbol = new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp); - tmp_symbol_expr=tmp_symbol.symbol_expr(); + tmp_symbol_expr = tmp_symbol.symbol_expr(); code_function_callt new_call(new_symbol); if(new_array) @@ -442,22 +438,21 @@ void goto_convertt::do_cpp_new( new_call.arguments().push_back(object_size); new_call.set( ID_C_cxx_alloc_type, to_type_with_subtype(lhs.type()).subtype()); - new_call.lhs()=tmp_symbol_expr; - new_call.add_source_location()=rhs.source_location(); + new_call.lhs() = tmp_symbol_expr; + new_call.add_source_location() = rhs.source_location(); convert(new_call, dest, ID_cpp); } - else if(rhs.operands().size()==1) + else if(rhs.operands().size() == 1) { // call __placement_new - exprt new_symbol= - ns.lookup( - new_array?"__placement_new_array":"__placement_new").symbol_expr(); + exprt new_symbol = + ns.lookup(new_array ? "__placement_new_array" : "__placement_new") + .symbol_expr(); - const code_typet &code_type= - to_code_type(new_symbol.type()); + const code_typet &code_type = to_code_type(new_symbol.type()); - const typet &return_type=code_type.return_type(); + const typet &return_type = code_type.return_type(); DATA_INVARIANT( code_type.parameters().size() == 2 || code_type.parameters().size() == 3, @@ -466,7 +461,7 @@ void goto_convertt::do_cpp_new( const symbolt &tmp_symbol = new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp); - tmp_symbol_expr=tmp_symbol.symbol_expr(); + tmp_symbol_expr = tmp_symbol.symbol_expr(); code_function_callt new_call(new_symbol); if(new_array) @@ -475,10 +470,10 @@ void goto_convertt::do_cpp_new( new_call.arguments().push_back(to_unary_expr(rhs).op()); // memory location new_call.set( ID_C_cxx_alloc_type, to_type_with_subtype(lhs.type()).subtype()); - new_call.lhs()=tmp_symbol_expr; - new_call.add_source_location()=rhs.source_location(); + new_call.lhs() = tmp_symbol_expr; + new_call.add_source_location() = rhs.source_location(); - for(std::size_t i=0; i(rhs.find(ID_initializer)); + exprt initializer = static_cast(rhs.find(ID_initializer)); if(initializer.is_not_nil()) { - if(rhs.get_statement()=="cpp_new[]") + if(rhs.get_statement() == "cpp_new[]") { // build loop } - else if(rhs.get_statement()==ID_cpp_new) + else if(rhs.get_statement() == ID_cpp_new) { // just one object const dereference_exprt deref_lhs( @@ -536,12 +530,12 @@ void goto_convertt::cpp_new_initializer( exprt goto_convertt::get_array_argument(const exprt &src) { - if(src.id()==ID_typecast) + if(src.id() == ID_typecast) return get_array_argument(to_typecast_expr(src).op()); - if(src.id()!=ID_address_of) + if(src.id() != ID_address_of) { - error().source_location=src.find_source_location(); + error().source_location = src.find_source_location(); error() << "expected array-pointer as argument" << eom; throw 0; } @@ -550,7 +544,7 @@ exprt goto_convertt::get_array_argument(const exprt &src) if(address_of_expr.object().id() != ID_index) { - error().source_location=src.find_source_location(); + error().source_location = src.find_source_location(); error() << "expected array-element as argument" << eom; throw 0; } @@ -559,7 +553,7 @@ exprt goto_convertt::get_array_argument(const exprt &src) if(index_expr.array().type().id() != ID_array) { - error().source_location=src.find_source_location(); + error().source_location = src.find_source_location(); error() << "expected array as argument" << eom; throw 0; } @@ -574,16 +568,16 @@ void goto_convertt::do_array_op( const exprt::operandst &arguments, goto_programt &dest) { - if(arguments.size()!=2) + if(arguments.size() != 2) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << id << " expects two arguments" << eom; throw 0; } codet array_op_statement(id); - array_op_statement.operands()=arguments; - array_op_statement.add_source_location()=function.source_location(); + array_op_statement.operands() = arguments; + array_op_statement.add_source_location() = function.source_location(); // lhs is only used with array_equal, in all other cases it should be nil (as // they are of type void) @@ -812,19 +806,19 @@ void goto_convertt::do_function_call_symbol( return; // ignore // lookup symbol - const irep_idt &identifier=function.get_identifier(); + const irep_idt &identifier = function.get_identifier(); const symbolt *symbol; if(ns.lookup(identifier, symbol)) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "error: function '" << identifier << "' not found" << eom; throw 0; } - if(symbol->type.id()!=ID_code) + if(symbol->type.id() != ID_code) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "error: function '" << identifier << "' type mismatch: expected code" << eom; throw 0; @@ -865,9 +859,9 @@ void goto_convertt::do_function_call_symbol( else if( identifier == CPROVER_PREFIX "assume" || identifier == "__VERIFIER_assume") { - if(arguments.size()!=1) + if(arguments.size() != 1) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have one argument" << eom; throw 0; } @@ -881,16 +875,16 @@ void goto_convertt::do_function_call_symbol( if(lhs.is_not_nil()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << identifier << " expected not to have LHS" << eom; throw 0; } } - else if(identifier=="__VERIFIER_error") + else if(identifier == "__VERIFIER_error") { if(!arguments.empty()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have no arguments" << eom; throw 0; } @@ -902,7 +896,7 @@ void goto_convertt::do_function_call_symbol( if(lhs.is_not_nil()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << identifier << " expected not to have LHS" << eom; throw 0; } @@ -918,9 +912,9 @@ void goto_convertt::do_function_call_symbol( identifier == "assert" && to_code_type(symbol->type).return_type() == signed_int_type()) { - if(arguments.size()!=1) + if(arguments.size() != 1) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have one argument" << eom; throw 0; } @@ -937,7 +931,7 @@ void goto_convertt::do_function_call_symbol( if(lhs.is_not_nil()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << identifier << " expected not to have LHS" << eom; throw 0; } @@ -947,19 +941,17 @@ void goto_convertt::do_function_call_symbol( identifier == CPROVER_PREFIX "precondition" || identifier == CPROVER_PREFIX "postcondition") { - if(arguments.size()!=2) + if(arguments.size() != 2) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have two arguments" << eom; throw 0; } - bool is_precondition= - identifier==CPROVER_PREFIX "precondition"; + bool is_precondition = identifier == CPROVER_PREFIX "precondition"; bool is_postcondition = identifier == CPROVER_PREFIX "postcondition"; - const irep_idt description= - get_string_constant(arguments[1]); + const irep_idt description = get_string_constant(arguments[1]); // let's double-check the type of the argument source_locationt annotated_location = function.source_location(); @@ -986,23 +978,23 @@ void goto_convertt::do_function_call_symbol( if(lhs.is_not_nil()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << identifier << " expected not to have LHS" << eom; throw 0; } } - else if(identifier==CPROVER_PREFIX "havoc_object") + else if(identifier == CPROVER_PREFIX "havoc_object") { - if(arguments.size()!=1) + if(arguments.size() != 1) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have one argument" << eom; throw 0; } if(lhs.is_not_nil()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << identifier << " expected not to have LHS" << eom; throw 0; } @@ -1013,53 +1005,55 @@ void goto_convertt::do_function_call_symbol( dest.add(goto_programt::make_other(havoc, function.source_location())); } - else if(identifier==CPROVER_PREFIX "printf") + else if(identifier == CPROVER_PREFIX "printf") { do_printf(lhs, function, arguments, dest); } - else if(identifier==CPROVER_PREFIX "scanf") + else if(identifier == CPROVER_PREFIX "scanf") { do_scanf(lhs, function, arguments, dest); } - else if(identifier==CPROVER_PREFIX "input" || - identifier=="__CPROVER::input") + else if( + identifier == CPROVER_PREFIX "input" || identifier == "__CPROVER::input") { if(lhs.is_not_nil()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << identifier << " expected not to have LHS" << eom; throw 0; } do_input(function, arguments, dest); } - else if(identifier==CPROVER_PREFIX "output" || - identifier=="__CPROVER::output") + else if( + identifier == CPROVER_PREFIX "output" || identifier == "__CPROVER::output") { if(lhs.is_not_nil()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << identifier << " expected not to have LHS" << eom; throw 0; } do_output(function, arguments, dest); } - else if(identifier==CPROVER_PREFIX "atomic_begin" || - identifier=="__CPROVER::atomic_begin" || - identifier=="java::org.cprover.CProver.atomicBegin:()V" || - identifier=="__VERIFIER_atomic_begin") + else if( + identifier == CPROVER_PREFIX "atomic_begin" || + identifier == "__CPROVER::atomic_begin" || + identifier == "java::org.cprover.CProver.atomicBegin:()V" || + identifier == "__VERIFIER_atomic_begin") { do_atomic_begin(lhs, function, arguments, dest); } - else if(identifier==CPROVER_PREFIX "atomic_end" || - identifier=="__CPROVER::atomic_end" || - identifier=="java::org.cprover.CProver.atomicEnd:()V" || - identifier=="__VERIFIER_atomic_end") + else if( + identifier == CPROVER_PREFIX "atomic_end" || + identifier == "__CPROVER::atomic_end" || + identifier == "java::org.cprover.CProver.atomicEnd:()V" || + identifier == "__VERIFIER_atomic_end") { do_atomic_end(lhs, function, arguments, dest); } - else if(identifier==CPROVER_PREFIX "prob_biased_coin") + else if(identifier == CPROVER_PREFIX "prob_biased_coin") { do_prob_coin(lhs, function, arguments, dest); } @@ -1079,11 +1073,11 @@ void goto_convertt::do_function_call_symbol( // We need to special-case for _Bool, which // can only be 0 or 1. - if(lhs.type().id()==ID_c_bool) + if(lhs.type().id() == ID_c_bool) { rhs = side_effect_expr_nondett(bool_typet(), function.source_location()); rhs.set(ID_C_identifier, identifier); - rhs=typecast_exprt(rhs, lhs.type()); + rhs = typecast_exprt(rhs, lhs.type()); } else { @@ -1092,7 +1086,7 @@ void goto_convertt::do_function_call_symbol( } code_assignt assignment(lhs, rhs); - assignment.add_source_location()=function.source_location(); + assignment.add_source_location() = function.source_location(); copy(assignment, ASSIGN, dest); } else if(identifier.starts_with(CPROVER_PREFIX "uninterpreted_")) @@ -1114,35 +1108,34 @@ void goto_convertt::do_function_call_symbol( mathematical_function_typet::domaint domain; for(const auto ¶meter : function_call_type.parameters()) domain.push_back(parameter.type()); - mathematical_function_typet function_type{domain, - function_call_type.return_type()}; + mathematical_function_typet function_type{ + domain, function_call_type.return_type()}; const function_application_exprt rhs( symbol_exprt{function.get_identifier(), function_type}, arguments); code_assignt assignment(lhs, rhs); - assignment.add_source_location()=function.source_location(); + assignment.add_source_location() = function.source_location(); copy(assignment, ASSIGN, dest); } - else if(identifier==CPROVER_PREFIX "array_equal") + else if(identifier == CPROVER_PREFIX "array_equal") { do_array_op(ID_array_equal, lhs, function, arguments, dest); } - else if(identifier==CPROVER_PREFIX "array_set") + else if(identifier == CPROVER_PREFIX "array_set") { do_array_op(ID_array_set, lhs, function, arguments, dest); } - else if(identifier==CPROVER_PREFIX "array_copy") + else if(identifier == CPROVER_PREFIX "array_copy") { do_array_op(ID_array_copy, lhs, function, arguments, dest); } - else if(identifier==CPROVER_PREFIX "array_replace") + else if(identifier == CPROVER_PREFIX "array_replace") { do_array_op(ID_array_replace, lhs, function, arguments, dest); } - else if(identifier=="__assert_fail" || - identifier=="_assert" || - identifier=="__assert_c99" || - identifier=="_wassert") + else if( + identifier == "__assert_fail" || identifier == "_assert" || + identifier == "__assert_c99" || identifier == "_wassert") { // __assert_fail is Linux // These take four arguments: @@ -1163,17 +1156,16 @@ void goto_convertt::do_function_call_symbol( // _wassert is Windows. The arguments are // L"expression", L"file.c", line - if(arguments.size()!=4 && - arguments.size()!=3) + if(arguments.size() != 4 && arguments.size() != 3) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have four arguments" << eom; throw 0; } - const irep_idt description= - "assertion "+id2string(get_string_constant(arguments[0])); + const irep_idt description = + "assertion " + id2string(get_string_constant(arguments[0])); source_locationt annotated_location = function.source_location(); annotated_location.set("user-provided", true); @@ -1182,8 +1174,7 @@ void goto_convertt::do_function_call_symbol( dest.add(goto_programt::make_assertion(false_exprt(), annotated_location)); // we ignore any LHS } - else if(identifier=="__assert_rtn" || - identifier=="__assert") + else if(identifier == "__assert_rtn" || identifier == "__assert") { // __assert_rtn has been seen on MacOS; // __assert is FreeBSD and Solaris 11. @@ -1194,19 +1185,17 @@ void goto_convertt::do_function_call_symbol( irep_idt description; - if(arguments.size()==4) + if(arguments.size() == 4) { - description= - "assertion "+id2string(get_string_constant(arguments[3])); + description = "assertion " + id2string(get_string_constant(arguments[3])); } - else if(arguments.size()==3) + else if(arguments.size() == 3) { - description= - "assertion "+id2string(get_string_constant(arguments[1])); + description = "assertion " + id2string(get_string_constant(arguments[1])); } else { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have four arguments" << eom; throw 0; @@ -1228,9 +1217,9 @@ void goto_convertt::do_function_call_symbol( // __assert13 is NetBSD // These take four arguments: // "file.c", line, __func__, "expression" - if(arguments.size()!=4) + if(arguments.size() != 4) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have four arguments" << eom; throw 0; @@ -1239,14 +1228,14 @@ void goto_convertt::do_function_call_symbol( irep_idt description; try { - description="assertion "+id2string(get_string_constant(arguments[3])); + description = "assertion " + id2string(get_string_constant(arguments[3])); } catch(int) { // we might be building newlib, where __assert_func is passed // a pointer-typed symbol; the warning will still have been // printed - description="assertion"; + description = "assertion"; } source_locationt annotated_location = function.source_location(); @@ -1256,11 +1245,11 @@ void goto_convertt::do_function_call_symbol( dest.add(goto_programt::make_assertion(false_exprt(), annotated_location)); // we ignore any LHS } - else if(identifier==CPROVER_PREFIX "fence") + else if(identifier == CPROVER_PREFIX "fence") { if(arguments.empty()) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have at least one argument" << eom; throw 0; @@ -1273,15 +1262,15 @@ void goto_convertt::do_function_call_symbol( dest.add(goto_programt::make_other(fence, function.source_location())); } - else if(identifier=="__builtin_prefetch") + else if(identifier == "__builtin_prefetch") { // does nothing } - else if(identifier=="__builtin_unreachable") + else if(identifier == "__builtin_unreachable") { // says something like UNREACHABLE; } - else if(identifier==ID_gcc_builtin_va_arg) + else if(identifier == ID_gcc_builtin_va_arg) { // This does two things. // 1) Return value of argument. @@ -1289,14 +1278,14 @@ void goto_convertt::do_function_call_symbol( // 2) Move list pointer to next argument. // This is just an increment. - if(arguments.size()!=1) + if(arguments.size() != 1) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have one argument" << eom; throw 0; } - exprt list_arg=make_va_list(arguments[0]); + exprt list_arg = make_va_list(arguments[0]); if(lhs.is_not_nil()) { @@ -1309,10 +1298,10 @@ void goto_convertt::do_function_call_symbol( typecast_exprt{list_arg, pointer_type(pointer_type(empty_typet{}))}; } - typet t=pointer_type(lhs.type()); + typet t = pointer_type(lhs.type()); dereference_exprt rhs{ typecast_exprt{dereference_exprt{std::move(list_arg_cast)}, t}}; - rhs.add_source_location()=function.source_location(); + rhs.add_source_location() = function.source_location(); dest.add( goto_programt::make_assignment(lhs, rhs, function.source_location())); } @@ -1324,21 +1313,21 @@ void goto_convertt::do_function_call_symbol( dest.add(goto_programt::make_assignment( std::move(assign), function.source_location())); } - else if(identifier=="__builtin_va_copy") + else if(identifier == "__builtin_va_copy") { - if(arguments.size()!=2) + if(arguments.size() != 2) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have two arguments" << eom; throw 0; } - exprt dest_expr=make_va_list(arguments[0]); + exprt dest_expr = make_va_list(arguments[0]); const typecast_exprt src_expr(arguments[1], dest_expr.type()); if(!is_assignable(dest_expr)) { - error().source_location=dest_expr.find_source_location(); + error().source_location = dest_expr.find_source_location(); error() << "va_copy argument expected to be lvalue" << eom; throw 0; } @@ -1350,18 +1339,18 @@ void goto_convertt::do_function_call_symbol( { // Set the list argument to be the address of the // parameter argument. - if(arguments.size()!=2) + if(arguments.size() != 2) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have two arguments" << eom; throw 0; } - exprt dest_expr=make_va_list(arguments[0]); + exprt dest_expr = make_va_list(arguments[0]); if(!is_assignable(dest_expr)) { - error().source_location=dest_expr.find_source_location(); + error().source_location = dest_expr.find_source_location(); error() << "va_start argument expected to be lvalue" << eom; throw 0; } @@ -1382,21 +1371,21 @@ void goto_convertt::do_function_call_symbol( dest.add(goto_programt::make_assignment( std::move(dest_expr), std::move(rhs), function.source_location())); } - else if(identifier=="__builtin_va_end") + else if(identifier == "__builtin_va_end") { // Invalidates the argument. We do so by setting it to NULL. - if(arguments.size()!=1) + if(arguments.size() != 1) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have one argument" << eom; throw 0; } - exprt dest_expr=make_va_list(arguments[0]); + exprt dest_expr = make_va_list(arguments[0]); if(!is_assignable(dest_expr)) { - error().source_location=dest_expr.find_source_location(); + error().source_location = dest_expr.find_source_location(); error() << "va_end argument expected to be lvalue" << eom; throw 0; } @@ -1420,22 +1409,23 @@ void goto_convertt::do_function_call_symbol( { // these support two double or two float arguments; we call the // appropriate internal version - if(arguments.size()!=2 || - (arguments[0].type()!=double_type() && - arguments[0].type()!=float_type()) || - (arguments[1].type()!=double_type() && - arguments[1].type()!=float_type())) + if( + arguments.size() != 2 || + (arguments[0].type() != double_type() && + arguments[0].type() != float_type()) || + (arguments[1].type() != double_type() && + arguments[1].type() != float_type())) { - error().source_location=function.find_source_location(); + error().source_location = function.find_source_location(); error() << "'" << identifier << "' expected to have two float/double arguments" << eom; throw 0; } - exprt::operandst new_arguments=arguments; + exprt::operandst new_arguments = arguments; - bool use_double=arguments[0].type()==double_type(); - if(arguments[0].type()!=arguments[1].type()) + bool use_double = arguments[0].type() == double_type(); + if(arguments[0].type() != arguments[1].type()) { if(use_double) { @@ -1446,31 +1436,31 @@ void goto_convertt::do_function_call_symbol( { new_arguments[0] = typecast_exprt(new_arguments[0], arguments[1].type()); - use_double=true; + use_double = true; } } - code_typet f_type=to_code_type(function.type()); + code_typet f_type = to_code_type(function.type()); f_type.remove_ellipsis(); - const typet &a_t=new_arguments[0].type(); - f_type.parameters()= + const typet &a_t = new_arguments[0].type(); + f_type.parameters() = code_typet::parameterst(2, code_typet::parametert(a_t)); // replace __builtin_ by CPROVER_PREFIX - std::string name=CPROVER_PREFIX+id2string(identifier).substr(10); + std::string name = CPROVER_PREFIX + id2string(identifier).substr(10); // append d or f for double/float - name+=use_double?'d':'f'; + name += use_double ? 'd' : 'f'; DATA_INVARIANT( ns.lookup(name).type == f_type, "builtin declaration should match constructed type"); - symbol_exprt new_function=function; + symbol_exprt new_function = function; new_function.set_identifier(name); - new_function.type()=f_type; + new_function.type() = f_type; code_function_callt function_call(lhs, new_function, new_arguments); - function_call.add_source_location()=function.source_location(); + function_call.add_source_location() = function.source_location(); copy(function_call, FUNCTION_CALL, dest); } @@ -1486,7 +1476,7 @@ void goto_convertt::do_function_call_symbol( // use symbol->symbol_expr() to ensure we use the type from the symbol table code_function_callt function_call( lhs, symbol->symbol_expr().with_source_location(function), arguments); - function_call.add_source_location()=function.source_location(); + function_call.add_source_location() = function.source_location(); // remove void-typed assignments, which may have been created when the // front-end was unable to detect them in type checking for a lack of diff --git a/src/ansi-c/goto-conversion/destructor.cpp b/src/ansi-c/goto-conversion/destructor.cpp index 2ecc88dfa7a1..3ac1d4298b70 100644 --- a/src/ansi-c/goto-conversion/destructor.cpp +++ b/src/ansi-c/goto-conversion/destructor.cpp @@ -11,22 +11,20 @@ Author: Daniel Kroening, kroening@kroening.com #include "destructor.h" -#include - #include #include -code_function_callt get_destructor( - const namespacet &ns, - const typet &type) +#include + +code_function_callt get_destructor(const namespacet &ns, const typet &type) { if(type.id() == ID_struct_tag) { return get_destructor(ns, ns.follow_tag(to_struct_tag_type(type))); } - else if(type.id()==ID_struct) + else if(type.id() == ID_struct) { - const exprt &methods=static_cast(type.find(ID_methods)); + const exprt &methods = static_cast(type.find(ID_methods)); for(const auto &op : methods.operands()) { @@ -34,10 +32,11 @@ code_function_callt get_destructor( { const code_typet &code_type = to_code_type(op.type()); - if(code_type.return_type().id()==ID_destructor && - code_type.parameters().size()==1) + if( + code_type.return_type().id() == ID_destructor && + code_type.parameters().size() == 1) { - const typet &arg_type=code_type.parameters().front().type(); + const typet &arg_type = code_type.parameters().front().type(); if( arg_type.id() == ID_pointer && diff --git a/src/ansi-c/goto-conversion/destructor.h b/src/ansi-c/goto-conversion/destructor.h index 8c887a2426b2..7cfbb594a61d 100644 --- a/src/ansi-c/goto-conversion/destructor.h +++ b/src/ansi-c/goto-conversion/destructor.h @@ -15,8 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com class namespacet; class typet; -class code_function_callt get_destructor( - const namespacet &ns, - const typet &type); +class code_function_callt +get_destructor(const namespacet &ns, const typet &type); #endif // CPROVER_GOTO_PROGRAMS_DESTRUCTOR_H diff --git a/src/ansi-c/goto-conversion/format_strings.cpp b/src/ansi-c/goto-conversion/format_strings.cpp index ecbf78e5fe50..8ed4d1671a19 100644 --- a/src/ansi-c/goto-conversion/format_strings.cpp +++ b/src/ansi-c/goto-conversion/format_strings.cpp @@ -18,57 +18,56 @@ Author: CM Wintersteiger #include -void parse_flags( - std::string::const_iterator &it, - format_tokent &curtok) +void parse_flags(std::string::const_iterator &it, format_tokent &curtok) { - while(*it=='#' || *it=='0' || - *it=='-' || *it==' ' || *it=='+') + while(*it == '#' || *it == '0' || *it == '-' || *it == ' ' || *it == '+') { switch(*it) { - case '#': - curtok.flags.push_back(format_tokent::flag_typet::ALTERNATE); break; - case '0': - curtok.flags.push_back(format_tokent::flag_typet::ZERO_PAD); break; - case '-': - curtok.flags.push_back(format_tokent::flag_typet::LEFT_ADJUST); break; - case ' ': - curtok.flags.push_back(format_tokent::flag_typet::SIGNED_SPACE); break; - case '+': - curtok.flags.push_back(format_tokent::flag_typet::SIGN); break; - default: - throw unsupported_operation_exceptiont( - std::string("unsupported format specifier flag: '") + *it + "'"); + case '#': + curtok.flags.push_back(format_tokent::flag_typet::ALTERNATE); + break; + case '0': + curtok.flags.push_back(format_tokent::flag_typet::ZERO_PAD); + break; + case '-': + curtok.flags.push_back(format_tokent::flag_typet::LEFT_ADJUST); + break; + case ' ': + curtok.flags.push_back(format_tokent::flag_typet::SIGNED_SPACE); + break; + case '+': + curtok.flags.push_back(format_tokent::flag_typet::SIGN); + break; + default: + throw unsupported_operation_exceptiont( + std::string("unsupported format specifier flag: '") + *it + "'"); } it++; } } -void parse_field_width( - std::string::const_iterator &it, - format_tokent &curtok) +void parse_field_width(std::string::const_iterator &it, format_tokent &curtok) { - if(*it=='*') + if(*it == '*') { curtok.flags.push_back(format_tokent::flag_typet::ASTERISK); it++; } std::string tmp; - for( ; isdigit(*it); it++) tmp+=*it; - curtok.field_width=string2integer(tmp); + for(; isdigit(*it); it++) + tmp += *it; + curtok.field_width = string2integer(tmp); } -void parse_precision( - std::string::const_iterator &it, - format_tokent &curtok) +void parse_precision(std::string::const_iterator &it, format_tokent &curtok) { - if(*it=='.') + if(*it == '.') { it++; - if(*it=='*') + if(*it == '*') { curtok.flags.push_back(format_tokent::flag_typet::ASTERISK); it++; @@ -76,8 +75,9 @@ void parse_precision( else { std::string tmp; - for( ; isdigit(*it); it++) tmp+=*it; - curtok.precision=string2integer(tmp); + for(; isdigit(*it); it++) + tmp += *it; + curtok.precision = string2integer(tmp); } } } @@ -86,31 +86,31 @@ void parse_length_modifier( std::string::const_iterator &it, format_tokent &curtok) { - if(*it=='h') + if(*it == 'h') { it++; - if(*it=='h') + if(*it == 'h') it++; curtok.length_modifier = format_tokent::length_modifierst::LEN_h; } - else if(*it=='l') + else if(*it == 'l') { it++; - if(*it=='l') + if(*it == 'l') it++; curtok.length_modifier = format_tokent::length_modifierst::LEN_l; } - else if(*it=='L') + else if(*it == 'L') { it++; curtok.length_modifier = format_tokent::length_modifierst::LEN_L; } - else if(*it=='j') + else if(*it == 'j') { it++; curtok.length_modifier = format_tokent::length_modifierst::LEN_j; } - else if(*it=='t') + else if(*it == 't') { it++; curtok.length_modifier = format_tokent::length_modifierst::LEN_L; @@ -124,61 +124,77 @@ void parse_conversion_specifier( { switch(*it) { - case 'd': - case 'i': - curtok.type=format_tokent::token_typet::INT; - curtok.representation=format_tokent::representationt::SIGNED_DEC; - break; - case 'o': - curtok.type=format_tokent::token_typet::INT; - curtok.representation=format_tokent::representationt::UNSIGNED_OCT; - break; - case 'u': - curtok.type=format_tokent::token_typet::INT; - curtok.representation=format_tokent::representationt::UNSIGNED_DEC; - break; - case 'x': - case 'X': - curtok.type=format_tokent::token_typet::INT; - curtok.representation=format_tokent::representationt::UNSIGNED_HEX; - break; - case 'e': - case 'E': curtok.type=format_tokent::token_typet::FLOAT; break; - case 'f': - case 'F': curtok.type=format_tokent::token_typet::FLOAT; break; - case 'g': - case 'G': curtok.type=format_tokent::token_typet::FLOAT; break; - case 'a': - case 'A': curtok.type=format_tokent::token_typet::FLOAT; break; - case 'c': curtok.type=format_tokent::token_typet::CHAR; break; - case 's': curtok.type=format_tokent::token_typet::STRING; break; - case 'p': curtok.type=format_tokent::token_typet::POINTER; break; - case '%': - curtok.type=format_tokent::token_typet::TEXT; - curtok.value="%"; - break; - case '[': // pattern matching in, e.g., fscanf. + case 'd': + case 'i': + curtok.type = format_tokent::token_typet::INT; + curtok.representation = format_tokent::representationt::SIGNED_DEC; + break; + case 'o': + curtok.type = format_tokent::token_typet::INT; + curtok.representation = format_tokent::representationt::UNSIGNED_OCT; + break; + case 'u': + curtok.type = format_tokent::token_typet::INT; + curtok.representation = format_tokent::representationt::UNSIGNED_DEC; + break; + case 'x': + case 'X': + curtok.type = format_tokent::token_typet::INT; + curtok.representation = format_tokent::representationt::UNSIGNED_HEX; + break; + case 'e': + case 'E': + curtok.type = format_tokent::token_typet::FLOAT; + break; + case 'f': + case 'F': + curtok.type = format_tokent::token_typet::FLOAT; + break; + case 'g': + case 'G': + curtok.type = format_tokent::token_typet::FLOAT; + break; + case 'a': + case 'A': + curtok.type = format_tokent::token_typet::FLOAT; + break; + case 'c': + curtok.type = format_tokent::token_typet::CHAR; + break; + case 's': + curtok.type = format_tokent::token_typet::STRING; + break; + case 'p': + curtok.type = format_tokent::token_typet::POINTER; + break; + case '%': + curtok.type = format_tokent::token_typet::TEXT; + curtok.value = "%"; + break; + case '[': // pattern matching in, e.g., fscanf. + { + std::string tmp; + it++; + if(*it == '^') // if it's there, it must be first { - std::string tmp; + tmp += '^'; it++; - if(*it=='^') // if it's there, it must be first + if(*it == ']') // if it's there, it must be here { - tmp+='^'; it++; - if(*it==']') // if it's there, it must be here - { - tmp+=']'; it++; - } + tmp += ']'; + it++; } + } - for( ; it!=arg_string.end() && *it!=']'; it++) - tmp+=*it; + for(; it != arg_string.end() && *it != ']'; it++) + tmp += *it; - break; - } + break; + } - default: - throw unsupported_operation_exceptiont( - std::string("unsupported format conversion specifier: '") + *it + "'"); + default: + throw unsupported_operation_exceptiont( + std::string("unsupported format conversion specifier: '") + *it + "'"); } it++; } @@ -187,14 +203,14 @@ format_token_listt parse_format_string(const std::string &arg_string) { format_token_listt token_list; - std::string::const_iterator it=arg_string.begin(); + std::string::const_iterator it = arg_string.begin(); - while(it!=arg_string.end()) + while(it != arg_string.end()) { - if(*it=='%') + if(*it == '%') { token_list.push_back(format_tokent()); - format_tokent &curtok=token_list.back(); + format_tokent &curtok = token_list.back(); it++; parse_flags(it, curtok); @@ -205,20 +221,21 @@ format_token_listt parse_format_string(const std::string &arg_string) } else { - if(token_list.empty() || - token_list.back().type!=format_tokent::token_typet::TEXT) + if( + token_list.empty() || + token_list.back().type != format_tokent::token_typet::TEXT) token_list.push_back(format_tokent(format_tokent::token_typet::TEXT)); std::string tmp; - for( ; it!=arg_string.end() && *it!='%'; it++) - tmp+=*it; + for(; it != arg_string.end() && *it != '%'; it++) + tmp += *it; INVARIANT( !token_list.empty() && - token_list.back().type == format_tokent::token_typet::TEXT, + token_list.back().type == format_tokent::token_typet::TEXT, "must already have a TEXT token at the back of the token list"); - token_list.back().value=tmp; + token_list.back().value = tmp; } } @@ -233,25 +250,25 @@ std::optional get_type(const format_tokent &token) switch(token.length_modifier) { case format_tokent::length_modifierst::LEN_h: - if(token.representation==format_tokent::representationt::SIGNED_DEC) + if(token.representation == format_tokent::representationt::SIGNED_DEC) return signed_char_type(); else return unsigned_char_type(); case format_tokent::length_modifierst::LEN_hh: - if(token.representation==format_tokent::representationt::SIGNED_DEC) + if(token.representation == format_tokent::representationt::SIGNED_DEC) return signed_short_int_type(); else return unsigned_short_int_type(); case format_tokent::length_modifierst::LEN_l: - if(token.representation==format_tokent::representationt::SIGNED_DEC) + if(token.representation == format_tokent::representationt::SIGNED_DEC) return signed_long_int_type(); else return unsigned_long_int_type(); case format_tokent::length_modifierst::LEN_ll: - if(token.representation==format_tokent::representationt::SIGNED_DEC) + if(token.representation == format_tokent::representationt::SIGNED_DEC) return signed_long_long_int_type(); else return unsigned_long_long_int_type(); @@ -260,7 +277,7 @@ std::optional get_type(const format_tokent &token) case format_tokent::length_modifierst::LEN_j: case format_tokent::length_modifierst::LEN_L: case format_tokent::length_modifierst::LEN_undef: - if(token.representation==format_tokent::representationt::SIGNED_DEC) + if(token.representation == format_tokent::representationt::SIGNED_DEC) return signed_int_type(); else return unsigned_int_type(); @@ -269,8 +286,10 @@ std::optional get_type(const format_tokent &token) case format_tokent::token_typet::FLOAT: switch(token.length_modifier) { - case format_tokent::length_modifierst::LEN_l: return double_type(); - case format_tokent::length_modifierst::LEN_L: return long_double_type(); + case format_tokent::length_modifierst::LEN_l: + return double_type(); + case format_tokent::length_modifierst::LEN_L: + return long_double_type(); case format_tokent::length_modifierst::LEN_h: case format_tokent::length_modifierst::LEN_hh: case format_tokent::length_modifierst::LEN_j: @@ -283,7 +302,8 @@ std::optional get_type(const format_tokent &token) case format_tokent::token_typet::CHAR: switch(token.length_modifier) { - case format_tokent::length_modifierst::LEN_l: return wchar_t_type(); + case format_tokent::length_modifierst::LEN_l: + return wchar_t_type(); case format_tokent::length_modifierst::LEN_h: case format_tokent::length_modifierst::LEN_hh: case format_tokent::length_modifierst::LEN_j: diff --git a/src/ansi-c/goto-conversion/format_strings.h b/src/ansi-c/goto-conversion/format_strings.h index 7e77c032caea..667bc17552d8 100644 --- a/src/ansi-c/goto-conversion/format_strings.h +++ b/src/ansi-c/goto-conversion/format_strings.h @@ -28,9 +28,9 @@ class format_tokent { UNKNOWN, TEXT, - INT, // d, i, o, u, x - FLOAT, // a, e, f, g - CHAR, // c + INT, // d, i, o, u, x + FLOAT, // a, e, f, g + CHAR, // c STRING, // s POINTER // p }; @@ -70,13 +70,14 @@ class format_tokent : type(_type), length_modifier(length_modifierst::LEN_undef), representation(representationt::SIGNED_undef) - { } - format_tokent(): - type(token_typet::UNKNOWN), - length_modifier(length_modifierst::LEN_undef), - representation(representationt::SIGNED_undef) - { } - + { + } + format_tokent() + : type(token_typet::UNKNOWN), + length_modifier(length_modifierst::LEN_undef), + representation(representationt::SIGNED_undef) + { + } token_typet type; std::list flags; diff --git a/src/ansi-c/goto-conversion/goto_asm.cpp b/src/ansi-c/goto-conversion/goto_asm.cpp index 63492b5d9ce9..9b85ff0cb7f0 100644 --- a/src/ansi-c/goto-conversion/goto_asm.cpp +++ b/src/ansi-c/goto-conversion/goto_asm.cpp @@ -11,9 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_convert_class.h" -void goto_convertt::convert_asm( - const code_asmt &code, - goto_programt &dest) +void goto_convertt::convert_asm(const code_asmt &code, goto_programt &dest) { // copy as OTHER copy(code, OTHER, dest); diff --git a/src/ansi-c/goto-conversion/goto_check_c.cpp b/src/ansi-c/goto-conversion/goto_check_c.cpp index 39451755393d..036845ff8a8f 100644 --- a/src/ansi-c/goto-conversion/goto_check_c.cpp +++ b/src/ansi-c/goto-conversion/goto_check_c.cpp @@ -36,11 +36,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include -#include - #include class goto_check_ct @@ -1169,11 +1168,10 @@ void goto_check_ct::float_overflow_check(const exprt &expr, const guardt &guard) isinf_exprt(to_binary_expr(expr).op1()), not_exprt(isinf_exprt(expr))); - std::string kind = expr.id() == ID_plus - ? "addition" - : expr.id() == ID_minus - ? "subtraction" - : expr.id() == ID_mult ? "multiplication" : ""; + std::string kind = expr.id() == ID_plus ? "addition" + : expr.id() == ID_minus ? "subtraction" + : expr.id() == ID_mult ? "multiplication" + : ""; add_guarded_property( std::move(overflow_check), diff --git a/src/ansi-c/goto-conversion/goto_clean_expr.cpp b/src/ansi-c/goto-conversion/goto_clean_expr.cpp index 2c9e1f32f4f5..f8de1cff1edd 100644 --- a/src/ansi-c/goto-conversion/goto_clean_expr.cpp +++ b/src/ansi-c/goto-conversion/goto_clean_expr.cpp @@ -22,7 +22,7 @@ symbol_exprt goto_convertt::make_compound_literal( goto_programt &dest, const irep_idt &mode) { - const source_locationt source_location=expr.find_source_location(); + const source_locationt source_location = expr.find_source_location(); symbolt &new_symbol = get_fresh_aux_symbol( expr.type(), @@ -32,13 +32,13 @@ symbol_exprt goto_convertt::make_compound_literal( mode, symbol_table); new_symbol.is_static_lifetime = lifetime != lifetimet::AUTOMATIC_LOCAL; - new_symbol.value=expr; + new_symbol.value = expr; // The value might depend on a variable, thus // generate code for this. - symbol_exprt result=new_symbol.symbol_expr(); - result.add_source_location()=source_location; + symbol_exprt result = new_symbol.symbol_expr(); + result.add_source_location() = source_location; // The lifetime of compound literals is really that of // the block they are in. @@ -46,7 +46,7 @@ symbol_exprt goto_convertt::make_compound_literal( copy(code_declt(result), DECL, dest); code_assignt code_assign(result, expr); - code_assign.add_source_location()=source_location; + code_assign.add_source_location() = source_location; convert(code_assign, dest, mode); // now create a 'dead' instruction @@ -87,7 +87,7 @@ bool goto_convertt::needs_cleaning(const exprt &expr) // g1 = (i == 0) // g2 = (i > 10) // forall (i : int) (g1 || g2) - if(expr.id()==ID_forall || expr.id()==ID_exists) + if(expr.id() == ID_forall || expr.id() == ID_exists) return false; for(const auto &op : expr.operands()) @@ -115,10 +115,11 @@ void goto_convertt::rewrite_boolean(exprt &expr) // re-write "a ==> b" into a?b:1 if(auto implies = expr_try_dynamic_cast(expr)) { - expr = if_exprt{std::move(implies->lhs()), - std::move(implies->rhs()), - true_exprt{}, - bool_typet{}}; + expr = if_exprt{ + std::move(implies->lhs()), + std::move(implies->rhs()), + true_exprt{}, + bool_typet{}}; return; } @@ -127,27 +128,25 @@ void goto_convertt::rewrite_boolean(exprt &expr) exprt tmp; - if(expr.id()==ID_and) - tmp=true_exprt(); + if(expr.id() == ID_and) + tmp = true_exprt(); else // ID_or - tmp=false_exprt(); + tmp = false_exprt(); - exprt::operandst &ops=expr.operands(); + exprt::operandst &ops = expr.operands(); // start with last one - for(exprt::operandst::reverse_iterator - it=ops.rbegin(); - it!=ops.rend(); + for(exprt::operandst::reverse_iterator it = ops.rbegin(); it != ops.rend(); ++it) { - exprt &op=*it; + exprt &op = *it; DATA_INVARIANT_WITH_DIAGNOSTICS( op.is_boolean(), "boolean operators must have only boolean operands", expr.find_source_location()); - if(expr.id()==ID_and) + if(expr.id() == ID_and) { if_exprt if_e(op, tmp, false_exprt()); tmp.swap(if_e); @@ -191,27 +190,28 @@ void goto_convertt::clean_expr( clean_expr(expr, dest, mode, result_is_used); return; } - else if(expr.id()==ID_if) + else if(expr.id() == ID_if) { // first clean condition clean_expr(to_if_expr(expr).cond(), dest, mode, true); // possibly done now - if(!needs_cleaning(to_if_expr(expr).true_case()) && - !needs_cleaning(to_if_expr(expr).false_case())) + if( + !needs_cleaning(to_if_expr(expr).true_case()) && + !needs_cleaning(to_if_expr(expr).false_case())) return; // copy expression - if_exprt if_expr=to_if_expr(expr); + if_exprt if_expr = to_if_expr(expr); DATA_INVARIANT_WITH_DIAGNOSTICS( if_expr.cond().is_boolean(), "condition for an 'if' must be boolean", if_expr.find_source_location()); - const source_locationt source_location=expr.find_source_location(); + const source_locationt source_location = expr.find_source_location(); - #if 0 +#if 0 // We do some constant-folding here, to mimic // what typical compilers do. { @@ -230,7 +230,7 @@ void goto_convertt::clean_expr( return; } } - #endif +#endif goto_programt tmp_true; clean_expr(if_expr.true_case(), tmp_true, mode, result_is_used); @@ -244,19 +244,19 @@ void goto_convertt::clean_expr( new_tmp_symbol(expr.type(), "if_expr", dest, source_location, mode); code_assignt assignment_true; - assignment_true.lhs()=new_symbol.symbol_expr(); - assignment_true.rhs()=if_expr.true_case(); - assignment_true.add_source_location()=source_location; + assignment_true.lhs() = new_symbol.symbol_expr(); + assignment_true.rhs() = if_expr.true_case(); + assignment_true.add_source_location() = source_location; convert(assignment_true, tmp_true, mode); code_assignt assignment_false; - assignment_false.lhs()=new_symbol.symbol_expr(); - assignment_false.rhs()=if_expr.false_case(); - assignment_false.add_source_location()=source_location; + assignment_false.lhs() = new_symbol.symbol_expr(); + assignment_false.rhs() = if_expr.false_case(); + assignment_false.add_source_location() = source_location; convert(assignment_false, tmp_false, mode); // overwrites expr - expr=new_symbol.symbol_expr(); + expr = new_symbol.symbol_expr(); } else { @@ -279,7 +279,7 @@ void goto_convertt::clean_expr( convert(code_expression, tmp_false, mode); } - expr=nil_exprt(); + expr = nil_exprt(); } // generate guard for argument side-effects @@ -295,7 +295,7 @@ void goto_convertt::clean_expr( return; } - else if(expr.id()==ID_comma) + else if(expr.id() == ID_comma) { if(result_is_used) { @@ -303,7 +303,7 @@ void goto_convertt::clean_expr( Forall_operands(it, expr) { - bool last=(it==--expr.operands().end()); + bool last = (it == --expr.operands().end()); // special treatment for last one if(last) @@ -334,12 +334,12 @@ void goto_convertt::clean_expr( convert(code_expressiont(*it), dest, mode); } - expr=nil_exprt(); + expr = nil_exprt(); } return; } - else if(expr.id()==ID_typecast) + else if(expr.id() == ID_typecast) { typecast_exprt &typecast = to_typecast_expr(expr); @@ -351,18 +351,18 @@ void goto_convertt::clean_expr( return; } - else if(expr.id()==ID_side_effect) + else if(expr.id() == ID_side_effect) { // some of the side-effects need special treatment! - const irep_idt statement=to_side_effect_expr(expr).get_statement(); + const irep_idt statement = to_side_effect_expr(expr).get_statement(); - if(statement==ID_gcc_conditional_expression) + if(statement == ID_gcc_conditional_expression) { // need to do separately remove_gcc_conditional_expression(expr, dest, mode); return; } - else if(statement==ID_statement_expression) + else if(statement == ID_statement_expression) { // need to do separately to prevent that // the operands of expr get 'cleaned' @@ -370,7 +370,7 @@ void goto_convertt::clean_expr( to_side_effect_expr(expr), dest, mode, result_is_used); return; } - else if(statement==ID_assign) + else if(statement == ID_assign) { // we do a special treatment for x=f(...) INVARIANT( @@ -402,7 +402,7 @@ void goto_convertt::clean_expr( exprt new_rhs = typecast_exprt::conditional_cast( side_effect_assign.rhs(), new_lhs.type()); code_assignt assignment(std::move(new_lhs), new_rhs); - assignment.add_source_location()=expr.source_location(); + assignment.add_source_location() = expr.source_location(); convert_assign(assignment, dest, mode); if(result_is_used) @@ -413,13 +413,13 @@ void goto_convertt::clean_expr( } } } - else if(expr.id()==ID_forall || expr.id()==ID_exists) + else if(expr.id() == ID_forall || expr.id() == ID_exists) { DATA_INVARIANT( !has_subexpr(expr, ID_side_effect), "the front-end should check quantified expressions for side-effects"); } - else if(expr.id()==ID_address_of) + else if(expr.id() == ID_address_of) { address_of_exprt &addr = to_address_of_expr(expr); clean_expr_address_of(addr.object(), dest, mode); @@ -431,12 +431,12 @@ void goto_convertt::clean_expr( Forall_operands(it, expr) clean_expr(*it, dest, mode); - if(expr.id()==ID_side_effect) + if(expr.id() == ID_side_effect) { remove_side_effect( to_side_effect_expr(expr), dest, mode, result_is_used, false); } - else if(expr.id()==ID_compound_literal) + else if(expr.id() == ID_compound_literal) { // This is simply replaced by the literal DATA_INVARIANT( @@ -453,30 +453,30 @@ void goto_convertt::clean_expr_address_of( // The address of object constructors can be taken, // which is re-written into the address of a variable. - if(expr.id()==ID_compound_literal) + if(expr.id() == ID_compound_literal) { DATA_INVARIANT( expr.operands().size() == 1, "ID_compound_literal has a single operand"); clean_expr(to_unary_expr(expr).op(), dest, mode); expr = make_compound_literal(to_unary_expr(expr).op(), dest, mode); } - else if(expr.id()==ID_string_constant) + else if(expr.id() == ID_string_constant) { // Leave for now, but long-term these might become static symbols. // LLVM appears to do precisely that. } - else if(expr.id()==ID_index) + else if(expr.id() == ID_index) { index_exprt &index_expr = to_index_expr(expr); clean_expr_address_of(index_expr.array(), dest, mode); clean_expr(index_expr.index(), dest, mode); } - else if(expr.id()==ID_dereference) + else if(expr.id() == ID_dereference) { dereference_exprt &deref_expr = to_dereference_expr(expr); clean_expr(deref_expr.pointer(), dest, mode); } - else if(expr.id()==ID_comma) + else if(expr.id() == ID_comma) { // Yes, one can take the address of a comma expression. // Treatment is similar to clean_expr() above. @@ -485,7 +485,7 @@ void goto_convertt::clean_expr_address_of( Forall_operands(it, expr) { - bool last=(it==--expr.operands().end()); + bool last = (it == --expr.operands().end()); // special treatment for last one if(last) diff --git a/src/ansi-c/goto-conversion/goto_convert.cpp b/src/ansi-c/goto-conversion/goto_convert.cpp index 2a79ffd9f353..f7e2961a1e65 100644 --- a/src/ansi-c/goto-conversion/goto_convert.cpp +++ b/src/ansi-c/goto-conversion/goto_convert.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Program Transformation -#include "destructor.h" #include "goto_convert.h" #include "goto_convert_class.h" @@ -27,6 +26,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "destructor.h" + static bool is_empty(const goto_programt &goto_program) { forall_goto_program_instructions(it, goto_program) @@ -67,7 +68,7 @@ static void finish_catch_push_targets(goto_programt &dest) if(instruction.targets.empty()) { - bool handler_added=true; + bool handler_added = true; const code_push_catcht::exception_listt &handler_list = to_code_push_catch(instruction.code()).exception_list(); @@ -75,9 +76,9 @@ static void finish_catch_push_targets(goto_programt &dest) { // some handlers may not have been converted (if there was no // exception to be caught); in such a situation we abort - if(label_targets.find(handler.get_label())==label_targets.end()) + if(label_targets.find(handler.get_label()) == label_targets.end()) { - handler_added=false; + handler_added = false; break; } } @@ -245,7 +246,7 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode) for(const auto &g_it : targets.gotos) { - goto_programt::instructiont &i=*(g_it.first); + goto_programt::instructiont &i = *(g_it.first); if(i.is_start_thread()) { @@ -346,7 +347,7 @@ void goto_convertt::finish_computed_gotos(goto_programt &goto_program) { for(auto &g_it : targets.computed_gotos) { - goto_programt::instructiont &i=*g_it; + goto_programt::instructiont &i = *g_it; dereference_exprt destination = to_dereference_expr(i.code().op0()); const exprt pointer = destination.pointer(); @@ -455,7 +456,7 @@ void goto_convertt::convert_label( const irep_idt &mode) { // grab the label - const irep_idt &label=code.get_label(); + const irep_idt &label = code.get_label(); goto_programt tmp; @@ -474,14 +475,14 @@ void goto_convertt::convert_label( // thread block (START_THREAD...END_THREAD). code_blockt thread_body; thread_body.add(to_code_label(code).code()); - thread_body.add_source_location()=code.source_location(); + thread_body.add_source_location() = code.source_location(); generate_thread_block(thread_body, dest, mode); } else { convert(to_code_label(code).code(), tmp, mode); - goto_programt::targett target=tmp.instructions.begin(); + goto_programt::targett target = tmp.instructions.begin(); dest.destructive_append(tmp); targets.labels.insert( @@ -490,9 +491,7 @@ void goto_convertt::convert_label( } } -void goto_convertt::convert_gcc_local_label( - const codet &, - goto_programt &) +void goto_convertt::convert_gcc_local_label(const codet &, goto_programt &) { // ignore for now } @@ -505,7 +504,7 @@ void goto_convertt::convert_switch_case( goto_programt tmp; convert(code.code(), tmp, mode); - goto_programt::targett target=tmp.instructions.begin(); + goto_programt::targett target = tmp.instructions.begin(); dest.destructive_append(tmp); // is a default target given? @@ -516,15 +515,16 @@ void goto_convertt::convert_switch_case( { // cases? - cases_mapt::iterator cases_entry=targets.cases_map.find(target); - if(cases_entry==targets.cases_map.end()) + cases_mapt::iterator cases_entry = targets.cases_map.find(target); + if(cases_entry == targets.cases_map.end()) { targets.cases.push_back(std::make_pair(target, caset())); - cases_entry=targets.cases_map.insert(std::make_pair( - target, --targets.cases.end())).first; + cases_entry = + targets.cases_map.insert(std::make_pair(target, --targets.cases.end())) + .first; } - exprt::operandst &case_op_dest=cases_entry->second->second; + exprt::operandst &case_op_dest = cases_entry->second->second; case_op_dest.push_back(code.case_op()); // make sure we have a source location in the case operand as otherwise we // end up with a GOTO instruction without a source location @@ -571,9 +571,9 @@ void goto_convertt::convert_gcc_switch_case_range( } // create a skeleton for case_guard - cases_entry->second->second.push_back( - and_exprt{binary_relation_exprt{code.lower(), ID_le, nil_exprt{}}, - binary_relation_exprt{nil_exprt{}, ID_le, code.upper()}}); + cases_entry->second->second.push_back(and_exprt{ + binary_relation_exprt{code.lower(), ID_le, nil_exprt{}}, + binary_relation_exprt{nil_exprt{}, ID_le, code.upper()}}); } /// converts 'code' and appends the result to 'dest' @@ -582,83 +582,82 @@ void goto_convertt::convert( goto_programt &dest, const irep_idt &mode) { - const irep_idt &statement=code.get_statement(); + const irep_idt &statement = code.get_statement(); - if(statement==ID_block) + if(statement == ID_block) convert_block(to_code_block(code), dest, mode); - else if(statement==ID_decl) + else if(statement == ID_decl) convert_frontend_decl(to_code_frontend_decl(code), dest, mode); - else if(statement==ID_decl_type) + else if(statement == ID_decl_type) convert_decl_type(code, dest); - else if(statement==ID_expression) + else if(statement == ID_expression) convert_expression(to_code_expression(code), dest, mode); - else if(statement==ID_assign) + else if(statement == ID_assign) convert_assign(to_code_assign(code), dest, mode); - else if(statement==ID_assert) + else if(statement == ID_assert) convert_assert(to_code_assert(code), dest, mode); - else if(statement==ID_assume) + else if(statement == ID_assume) convert_assume(to_code_assume(code), dest, mode); - else if(statement==ID_function_call) + else if(statement == ID_function_call) convert_function_call(to_code_function_call(code), dest, mode); - else if(statement==ID_label) + else if(statement == ID_label) convert_label(to_code_label(code), dest, mode); - else if(statement==ID_gcc_local_label) + else if(statement == ID_gcc_local_label) convert_gcc_local_label(code, dest); - else if(statement==ID_switch_case) + else if(statement == ID_switch_case) convert_switch_case(to_code_switch_case(code), dest, mode); - else if(statement==ID_gcc_switch_case_range) + else if(statement == ID_gcc_switch_case_range) convert_gcc_switch_case_range( to_code_gcc_switch_case_range(code), dest, mode); - else if(statement==ID_for) + else if(statement == ID_for) convert_for(to_code_for(code), dest, mode); - else if(statement==ID_while) + else if(statement == ID_while) convert_while(to_code_while(code), dest, mode); - else if(statement==ID_dowhile) + else if(statement == ID_dowhile) convert_dowhile(to_code_dowhile(code), dest, mode); - else if(statement==ID_switch) + else if(statement == ID_switch) convert_switch(to_code_switch(code), dest, mode); - else if(statement==ID_break) + else if(statement == ID_break) convert_break(to_code_break(code), dest, mode); - else if(statement==ID_return) + else if(statement == ID_return) convert_return(to_code_frontend_return(code), dest, mode); - else if(statement==ID_continue) + else if(statement == ID_continue) convert_continue(to_code_continue(code), dest, mode); - else if(statement==ID_goto) + else if(statement == ID_goto) convert_goto(to_code_goto(code), dest); - else if(statement==ID_gcc_computed_goto) + else if(statement == ID_gcc_computed_goto) convert_gcc_computed_goto(code, dest); - else if(statement==ID_skip) + else if(statement == ID_skip) convert_skip(code, dest); - else if(statement==ID_ifthenelse) + else if(statement == ID_ifthenelse) convert_ifthenelse(to_code_ifthenelse(code), dest, mode); - else if(statement==ID_start_thread) + else if(statement == ID_start_thread) convert_start_thread(code, dest); - else if(statement==ID_end_thread) + else if(statement == ID_end_thread) convert_end_thread(code, dest); - else if(statement==ID_atomic_begin) + else if(statement == ID_atomic_begin) convert_atomic_begin(code, dest); - else if(statement==ID_atomic_end) + else if(statement == ID_atomic_end) convert_atomic_end(code, dest); - else if(statement==ID_cpp_delete || - statement=="cpp_delete[]") + else if(statement == ID_cpp_delete || statement == "cpp_delete[]") convert_cpp_delete(code, dest); - else if(statement==ID_msc_try_except) + else if(statement == ID_msc_try_except) convert_msc_try_except(code, dest, mode); - else if(statement==ID_msc_try_finally) + else if(statement == ID_msc_try_finally) convert_msc_try_finally(code, dest, mode); - else if(statement==ID_msc_leave) + else if(statement == ID_msc_leave) convert_msc_leave(code, dest, mode); - else if(statement==ID_try_catch) // C++ try/catch + else if(statement == ID_try_catch) // C++ try/catch convert_try_catch(code, dest, mode); - else if(statement==ID_CPROVER_try_catch) // CPROVER-homemade + else if(statement == ID_CPROVER_try_catch) // CPROVER-homemade convert_CPROVER_try_catch(code, dest, mode); - else if(statement==ID_CPROVER_throw) // CPROVER-homemade + else if(statement == ID_CPROVER_throw) // CPROVER-homemade convert_CPROVER_throw(code, dest, mode); - else if(statement==ID_CPROVER_try_finally) + else if(statement == ID_CPROVER_try_finally) convert_CPROVER_try_finally(code, dest, mode); - else if(statement==ID_asm) + else if(statement == ID_asm) convert_asm(to_code_asm(code), dest); - else if(statement==ID_static_assert) + else if(statement == ID_static_assert) { PRECONDITION(code.operands().size() == 2); exprt assertion = @@ -669,16 +668,16 @@ void goto_convertt::convert( "static assertion " + id2string(get_string_constant(code.op1())), code.op0().find_source_location()); } - else if(statement==ID_dead) + else if(statement == ID_dead) copy(code, DEAD, dest); - else if(statement==ID_decl_block) + else if(statement == ID_decl_block) { for(const auto &op : code.operands()) convert(to_code(op), dest, mode); } - else if(statement==ID_push_catch || - statement==ID_pop_catch || - statement==ID_exception_landingpad) + else if( + statement == ID_push_catch || statement == ID_pop_catch || + statement == ID_exception_landingpad) copy(code, CATCH, dest); else copy(code, OTHER, dest); @@ -695,7 +694,7 @@ void goto_convertt::convert_block( goto_programt &dest, const irep_idt &mode) { - const source_locationt &end_location=code.end_location(); + const source_locationt &end_location = code.end_location(); // this saves the index of the destructor stack node_indext old_stack_top = targets.scope_stack.get_current_node(); @@ -726,18 +725,18 @@ void goto_convertt::convert_expression( { exprt expr = code.expression(); - if(expr.id()==ID_if) + if(expr.id() == ID_if) { // We do a special treatment for c?t:f // by compiling to if(c) t; else f; - const if_exprt &if_expr=to_if_expr(expr); + const if_exprt &if_expr = to_if_expr(expr); code_ifthenelset tmp_code( if_expr.cond(), code_expressiont(if_expr.true_case()), code_expressiont(if_expr.false_case())); - tmp_code.add_source_location()=expr.source_location(); - tmp_code.then_case().add_source_location()=expr.source_location(); - tmp_code.else_case().add_source_location()=expr.source_location(); + tmp_code.add_source_location() = expr.source_location(); + tmp_code.then_case().add_source_location() = expr.source_location(); + tmp_code.else_case().add_source_location() = expr.source_location(); convert_ifthenelse(tmp_code, dest, mode); } else @@ -748,9 +747,9 @@ void goto_convertt::convert_expression( // We keep it to add checks later. if(expr.is_not_nil()) { - codet tmp=code; - tmp.op0()=expr; - tmp.add_source_location()=expr.source_location(); + codet tmp = code; + tmp.op0() = expr; + tmp.add_source_location() = expr.source_location(); copy(tmp, OTHER, dest); } } @@ -765,8 +764,7 @@ void goto_convertt::convert_frontend_decl( const symbolt &symbol = ns.lookup(identifier); - if(symbol.is_static_lifetime || - symbol.type.id()==ID_code) + if(symbol.is_static_lifetime || symbol.type.id() == ID_code) return; // this is a SKIP! const goto_programt::targett declaration_iterator = [&]() { @@ -778,7 +776,7 @@ void goto_convertt::convert_frontend_decl( exprt initializer = code.op1(); - codet tmp=code; + codet tmp = code; tmp.operands().resize(1); // hide this declaration-without-initializer step in the goto trace tmp.add_source_location().set_hide(); @@ -814,7 +812,7 @@ void goto_convertt::convert_frontend_decl( } // do destructor - code_function_callt destructor=get_destructor(ns, symbol.type); + code_function_callt destructor = get_destructor(ns, symbol.type); if(destructor.is_not_nil()) { @@ -826,9 +824,7 @@ void goto_convertt::convert_frontend_decl( } } -void goto_convertt::convert_decl_type( - const codet &, - goto_programt &) +void goto_convertt::convert_decl_type(const codet &, goto_programt &) { // we remove these } @@ -838,13 +834,11 @@ void goto_convertt::convert_assign( goto_programt &dest, const irep_idt &mode) { - exprt lhs=code.lhs(), - rhs=code.rhs(); + exprt lhs = code.lhs(), rhs = code.rhs(); clean_expr(lhs, dest, mode); - if(rhs.id()==ID_side_effect && - rhs.get(ID_statement)==ID_function_call) + if(rhs.id() == ID_side_effect && rhs.get(ID_statement) == ID_function_call) { const auto &rhs_function_call = to_side_effect_expr_function_call(rhs); @@ -863,9 +857,9 @@ void goto_convertt::convert_assign( dest, mode); } - else if(rhs.id()==ID_side_effect && - (rhs.get(ID_statement)==ID_cpp_new || - rhs.get(ID_statement)==ID_cpp_new_array)) + else if( + rhs.id() == ID_side_effect && (rhs.get(ID_statement) == ID_cpp_new || + rhs.get(ID_statement) == ID_cpp_new_array)) { Forall_operands(it, rhs) clean_expr(*it, dest, mode); @@ -898,8 +892,8 @@ void goto_convertt::convert_assign( clean_expr(*it, dest, mode); code_assignt new_assign(code); - new_assign.lhs()=lhs; - new_assign.rhs()=rhs; + new_assign.lhs() = lhs; + new_assign.rhs() = rhs; copy(new_assign, ASSIGN, dest); } @@ -909,51 +903,49 @@ void goto_convertt::convert_assign( clean_expr(rhs, dest, mode); code_assignt new_assign(code); - new_assign.lhs()=lhs; - new_assign.rhs()=rhs; + new_assign.lhs() = lhs; + new_assign.rhs() = rhs; copy(new_assign, ASSIGN, dest); } } -void goto_convertt::convert_cpp_delete( - const codet &code, - goto_programt &dest) +void goto_convertt::convert_cpp_delete(const codet &code, goto_programt &dest) { INVARIANT_WITH_DIAGNOSTICS( code.operands().size() == 1, "cpp_delete statement takes one operand", code.find_source_location()); - exprt tmp_op=code.op0(); + exprt tmp_op = code.op0(); clean_expr(tmp_op, dest, ID_cpp); // we call the destructor, and then free - const exprt &destructor= + const exprt &destructor = static_cast(code.find(ID_destructor)); irep_idt delete_identifier; - if(code.get_statement()==ID_cpp_delete_array) - delete_identifier="__delete_array"; - else if(code.get_statement()==ID_cpp_delete) - delete_identifier="__delete"; + if(code.get_statement() == ID_cpp_delete_array) + delete_identifier = "__delete_array"; + else if(code.get_statement() == ID_cpp_delete) + delete_identifier = "__delete"; else UNREACHABLE; if(destructor.is_not_nil()) { - if(code.get_statement()==ID_cpp_delete_array) + if(code.get_statement() == ID_cpp_delete_array) { // build loop } - else if(code.get_statement()==ID_cpp_delete) + else if(code.get_statement() == ID_cpp_delete) { // just one object const dereference_exprt deref_op(tmp_op); - codet tmp_code=to_code(destructor); + codet tmp_code = to_code(destructor); replace_new_object(deref_op, tmp_code); convert(tmp_code, dest, ID_cpp); } @@ -962,18 +954,18 @@ void goto_convertt::convert_cpp_delete( } // now do "free" - exprt delete_symbol=ns.lookup(delete_identifier).symbol_expr(); + exprt delete_symbol = ns.lookup(delete_identifier).symbol_expr(); DATA_INVARIANT( to_code_type(delete_symbol.type()).parameters().size() == 1, "delete statement takes 1 parameter"); - typet arg_type= + typet arg_type = to_code_type(delete_symbol.type()).parameters().front().type(); code_function_callt delete_call( delete_symbol, {typecast_exprt(tmp_op, arg_type)}); - delete_call.add_source_location()=code.source_location(); + delete_call.add_source_location() = code.source_location(); convert(delete_call, dest, ID_cpp); } @@ -983,7 +975,7 @@ void goto_convertt::convert_assert( goto_programt &dest, const irep_idt &mode) { - exprt cond=code.assertion(); + exprt cond = code.assertion(); clean_expr(cond, dest, mode); @@ -992,9 +984,7 @@ void goto_convertt::convert_assert( dest.add(goto_programt::make_assertion(cond, annotated_location)); } -void goto_convertt::convert_skip( - const codet &code, - goto_programt &dest) +void goto_convertt::convert_skip(const codet &code, goto_programt &dest) { dest.add(goto_programt::instructiont( code, code.source_location(), SKIP, nil_exprt(), {})); @@ -1005,7 +995,7 @@ void goto_convertt::convert_assume( goto_programt &dest, const irep_idt &mode) { - exprt op=code.assumption(); + exprt op = code.assumption(); clean_expr(op, dest, mode); @@ -1074,7 +1064,7 @@ void goto_convertt::convert_for( if(code.init().is_not_nil()) convert(to_code(code.init()), dest, mode); - exprt cond=code.cond(); + exprt cond = code.cond(); goto_programt sideeffects; clean_expr(cond, sideeffects, mode); @@ -1083,7 +1073,7 @@ void goto_convertt::convert_for( break_continue_targetst old_targets(targets); // do the u label - goto_programt::targett u=sideeffects.instructions.begin(); + goto_programt::targett u = sideeffects.instructions.begin(); // do the v label goto_programt tmp_v; @@ -1103,7 +1093,7 @@ void goto_convertt::convert_for( } else { - exprt tmp_B=code.iter(); + exprt tmp_B = code.iter(); clean_expr(tmp_B, tmp_x, mode, false); @@ -1113,7 +1103,7 @@ void goto_convertt::convert_for( // optimize the v label if(sideeffects.instructions.empty()) - u=v; + u = v; // set the targets targets.set_break(z); @@ -1151,8 +1141,8 @@ void goto_convertt::convert_while( goto_programt &dest, const irep_idt &mode) { - const exprt &cond=code.cond(); - const source_locationt &source_location=code.source_location(); + const exprt &cond = code.cond(); + const source_locationt &source_location = code.source_location(); // while(c) P; //-------------------- @@ -1175,7 +1165,7 @@ void goto_convertt::convert_while( boolean_negate(cond), z, source_location, tmp_branch, mode); // do the v label - goto_programt::targett v=tmp_branch.instructions.begin(); + goto_programt::targett v = tmp_branch.instructions.begin(); // y: goto v; goto_programt tmp_y; @@ -1213,9 +1203,9 @@ void goto_convertt::convert_dowhile( code.find_source_location()); // save source location - source_locationt condition_location=code.cond().find_source_location(); + source_locationt condition_location = code.cond().find_source_location(); - exprt cond=code.cond(); + exprt cond = code.cond(); goto_programt sideeffects; clean_expr(cond, sideeffects, mode); @@ -1243,9 +1233,9 @@ void goto_convertt::convert_dowhile( // do the x label goto_programt::targett x; if(sideeffects.instructions.empty()) - x=y; + x = y; else - x=sideeffects.instructions.begin(); + x = sideeffects.instructions.begin(); // set the targets targets.set_break(z); @@ -1254,7 +1244,7 @@ void goto_convertt::convert_dowhile( // do the w label goto_programt tmp_w; convert(code.body(), tmp_w, mode); - goto_programt::targett w=tmp_w.instructions.begin(); + goto_programt::targett w = tmp_w.instructions.begin(); // y: if(c) goto w; y->complete_goto(w); @@ -1327,13 +1317,13 @@ void goto_convertt::convert_switch( // get the location of the end of the body, but // default to location of switch, if none - source_locationt body_end_location= - code.body().get_statement()==ID_block? - to_code_block(code.body()).end_location(): - code.source_location(); + source_locationt body_end_location = + code.body().get_statement() == ID_block + ? to_code_block(code.body()).end_location() + : code.source_location(); // do the value we switch over - exprt argument=code.value(); + exprt argument = code.value(); goto_programt sideeffects; clean_expr(argument, sideeffects, mode); @@ -1390,20 +1380,20 @@ void goto_convertt::convert_switch( // case 10: // case_number 3 // ...; // } - size_t case_number=1; + size_t case_number = 1; for(auto &case_pair : targets.cases) { - const caset &case_ops=case_pair.second; + const caset &case_ops = case_pair.second; - if (case_ops.empty()) + if(case_ops.empty()) continue; - exprt guard_expr=case_guard(argument, case_ops); + exprt guard_expr = case_guard(argument, case_ops); - source_locationt source_location=case_ops.front().find_source_location(); + source_locationt source_location = case_ops.front().find_source_location(); source_location.set_case_number(std::to_string(case_number)); case_number++; - guard_expr.add_source_location()=source_location; + guard_expr.add_source_location() = source_location; tmp_cases.add(goto_programt::make_goto( case_pair.first, std::move(guard_expr), source_location)); @@ -1458,8 +1448,7 @@ void goto_convertt::convert_return( if(new_code.has_return_value()) { - bool result_is_used= - new_code.return_value().type().id()!=ID_empty; + bool result_is_used = new_code.return_value().type().id() != ID_empty; goto_programt sideeffects; clean_expr(new_code.return_value(), sideeffects, mode, result_is_used); @@ -1539,9 +1528,7 @@ void goto_convertt::convert_gcc_computed_goto( targets.computed_gotos.push_back(t); } -void goto_convertt::convert_start_thread( - const codet &code, - goto_programt &dest) +void goto_convertt::convert_start_thread(const codet &code, goto_programt &dest) { goto_programt::targett start_thread = dest.add(goto_programt::instructiont( code, code.source_location(), START_THREAD, nil_exprt(), {})); @@ -1551,9 +1538,7 @@ void goto_convertt::convert_start_thread( start_thread, targets.scope_stack.get_current_node()); } -void goto_convertt::convert_end_thread( - const codet &code, - goto_programt &dest) +void goto_convertt::convert_end_thread(const codet &code, goto_programt &dest) { INVARIANT_WITH_DIAGNOSTICS( code.operands().empty(), @@ -1563,9 +1548,7 @@ void goto_convertt::convert_end_thread( copy(code, END_THREAD, dest); } -void goto_convertt::convert_atomic_begin( - const codet &code, - goto_programt &dest) +void goto_convertt::convert_atomic_begin(const codet &code, goto_programt &dest) { INVARIANT_WITH_DIAGNOSTICS( code.operands().empty(), @@ -1575,9 +1558,7 @@ void goto_convertt::convert_atomic_begin( copy(code, ATOMIC_BEGIN, dest); } -void goto_convertt::convert_atomic_end( - const codet &code, - goto_programt &dest) +void goto_convertt::convert_atomic_end(const codet &code, goto_programt &dest) { INVARIANT_WITH_DIAGNOSTICS( code.operands().empty(), @@ -1594,10 +1575,9 @@ void goto_convertt::convert_ifthenelse( { DATA_INVARIANT(code.then_case().is_not_nil(), "cannot accept an empty body"); - bool has_else= - !code.else_case().is_nil(); + bool has_else = !code.else_case().is_nil(); - const source_locationt &source_location=code.source_location(); + const source_locationt &source_location = code.source_location(); // We do a bit of special treatment for && in the condition // in case cleaning would be needed otherwise. @@ -1636,7 +1616,7 @@ void goto_convertt::convert_ifthenelse( : code.else_case().source_location(); } - exprt tmp_guard=code.cond(); + exprt tmp_guard = code.cond(); clean_expr(tmp_guard, dest, mode); generate_ifthenelse( @@ -1655,7 +1635,7 @@ void goto_convertt::collect_operands( const irep_idt &id, std::list &dest) { - if(expr.id()!=id) + if(expr.id() != id) { dest.push_back(expr); } @@ -1673,7 +1653,7 @@ void goto_convertt::collect_operands( static inline bool is_size_one(const goto_programt &g) { return (!g.instructions.empty()) && - ++g.instructions.begin()==g.instructions.end(); + ++g.instructions.begin() == g.instructions.end(); } /// if(guard) true_case; else false_case; @@ -1687,8 +1667,7 @@ void goto_convertt::generate_ifthenelse( goto_programt &dest, const irep_idt &mode) { - if(is_empty(true_case) && - is_empty(false_case)) + if(is_empty(true_case) && is_empty(false_case)) { // hmpf. Useless branch. goto_programt tmp_z; @@ -1765,7 +1744,7 @@ void goto_convertt::generate_ifthenelse( mode); } - bool has_else=!is_empty(false_case); + bool has_else = !is_empty(false_case); // if(c) P; //-------------------- @@ -1797,7 +1776,7 @@ void goto_convertt::generate_ifthenelse( if(has_else) { tmp_y.swap(false_case); - y=tmp_y.instructions.begin(); + y = tmp_y.instructions.begin(); } // v: if(!c) goto z/y; @@ -1849,7 +1828,7 @@ static bool has_and_or(const exprt &expr) return true; } - if(expr.id()==ID_and || expr.id()==ID_or) + if(expr.id() == ID_and || expr.id() == ID_or) return true; return false; @@ -1881,7 +1860,7 @@ void goto_convertt::generate_conditional_branch( else { // simple branch - exprt cond=guard; + exprt cond = guard; clean_expr(cond, dest, mode); dest.add(goto_programt::make_goto(target_true, cond, source_location)); @@ -1897,7 +1876,7 @@ void goto_convertt::generate_conditional_branch( goto_programt &dest, const irep_idt &mode) { - if(guard.id()==ID_not) + if(guard.id() == ID_not) { // simply swap targets generate_conditional_branch( @@ -1910,7 +1889,7 @@ void goto_convertt::generate_conditional_branch( return; } - if(guard.id()==ID_and) + if(guard.id() == ID_and) { // turn // if(a && b) goto target_true; else goto target_false; @@ -1930,7 +1909,7 @@ void goto_convertt::generate_conditional_branch( return; } - else if(guard.id()==ID_or) + else if(guard.id() == ID_or) { // turn // if(a || b) goto target_true; else goto target_false; @@ -1953,7 +1932,7 @@ void goto_convertt::generate_conditional_branch( return; } - exprt cond=guard; + exprt cond = guard; clean_expr(cond, dest, mode); // true branch @@ -1963,9 +1942,7 @@ void goto_convertt::generate_conditional_branch( dest.add(goto_programt::make_goto(target_false, source_location)); } -bool goto_convertt::get_string_constant( - const exprt &expr, - irep_idt &value) +bool goto_convertt::get_string_constant(const exprt &expr, irep_idt &value) { if(expr.id() == ID_typecast) return get_string_constant(to_typecast_expr(expr).op(), value); @@ -1978,12 +1955,12 @@ bool goto_convertt::get_string_constant( get_constant(to_index_expr(to_address_of_expr(expr).object()).array()); simplify(index_op, ns); - if(index_op.id()==ID_string_constant) + if(index_op.id() == ID_string_constant) { value = to_string_constant(index_op).value(); return false; } - else if(index_op.id()==ID_array) + else if(index_op.id() == ID_array) { std::string result; for(const auto &op : as_const(index_op).operands()) @@ -1999,11 +1976,11 @@ bool goto_convertt::get_string_constant( } } - return value=result, false; + return value = result, false; } } - if(expr.id()==ID_string_constant) + if(expr.id() == ID_string_constant) { value = to_string_constant(expr).value(); return false; @@ -2028,20 +2005,19 @@ irep_idt goto_convertt::get_string_constant(const exprt &expr) exprt goto_convertt::get_constant(const exprt &expr) { - if(expr.id()==ID_symbol) + if(expr.id() == ID_symbol) { - const symbolt &symbol= - ns.lookup(to_symbol_expr(expr)); + const symbolt &symbol = ns.lookup(to_symbol_expr(expr)); return symbol.value; } - else if(expr.id()==ID_member) + else if(expr.id() == ID_member) { auto tmp = to_member_expr(expr); tmp.compound() = get_constant(tmp.compound()); return std::move(tmp); } - else if(expr.id()==ID_index) + else if(expr.id() == ID_index) { auto tmp = to_index_expr(expr); tmp.op0() = get_constant(tmp.op0()); @@ -2069,7 +2045,7 @@ symbolt &goto_convertt::new_tmp_symbol( symbol_table); code_frontend_declt decl(new_symbol.symbol_expr()); - decl.add_source_location()=source_location; + decl.add_source_location() = source_location; convert_frontend_decl(decl, dest, mode); return new_symbol; @@ -2081,19 +2057,19 @@ void goto_convertt::make_temp_symbol( goto_programt &dest, const irep_idt &mode) { - const source_locationt source_location=expr.find_source_location(); + const source_locationt source_location = expr.find_source_location(); symbolt &new_symbol = new_tmp_symbol(expr.type(), suffix, dest, source_location, mode); code_assignt assignment; - assignment.lhs()=new_symbol.symbol_expr(); - assignment.rhs()=expr; - assignment.add_source_location()=source_location; + assignment.lhs() = new_symbol.symbol_expr(); + assignment.rhs() = expr; + assignment.add_source_location() = source_location; convert(assignment, dest, mode); - expr=new_symbol.symbol_expr(); + expr = new_symbol.symbol_expr(); } void goto_convert( @@ -2121,7 +2097,7 @@ void goto_convert( DATA_INVARIANT( s_it != symbol_table.symbols.end(), "failed to find main symbol"); - const symbolt &symbol=s_it->second; + const symbolt &symbol = s_it->second; ::goto_convert( to_code(symbol.value), symbol_table, dest, message_handler, symbol.mode); diff --git a/src/ansi-c/goto-conversion/goto_convert_class.h b/src/ansi-c/goto-conversion/goto_convert_class.h index b23f569b6922..3a8a741476bc 100644 --- a/src/ansi-c/goto-conversion/goto_convert_class.h +++ b/src/ansi-c/goto-conversion/goto_convert_class.h @@ -17,20 +17,20 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include -#include +#include "scope_tree.h" #include #include #include -#include "scope_tree.h" - class side_effect_expr_overflowt; struct build_declaration_hops_inputst; -class goto_convertt:public messaget +class goto_convertt : public messaget { public: void @@ -38,11 +38,11 @@ class goto_convertt:public messaget goto_convertt( symbol_table_baset &_symbol_table, - message_handlert &_message_handler): - messaget(_message_handler), - symbol_table(_symbol_table), - ns(_symbol_table), - tmp_symbol_prefix("goto_convertt") + message_handlert &_message_handler) + : messaget(_message_handler), + symbol_table(_symbol_table), + ns(_symbol_table), + tmp_symbol_prefix("goto_convertt") { } @@ -141,17 +141,13 @@ class goto_convertt:public messaget side_effect_exprt &expr, goto_programt &dest, bool result_is_used); - void remove_cpp_delete( - side_effect_exprt &expr, - goto_programt &dest); + void remove_cpp_delete(side_effect_exprt &expr, goto_programt &dest); void remove_malloc( side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used); - void remove_temporary_object( - side_effect_exprt &expr, - goto_programt &dest); + void remove_temporary_object(side_effect_exprt &expr, goto_programt &dest); void remove_statement_expression( side_effect_exprt &expr, goto_programt &dest, @@ -182,9 +178,7 @@ class goto_convertt:public messaget const side_effect_exprt &rhs, goto_programt &dest); - static void replace_new_object( - const exprt &object, - exprt &dest); + static void replace_new_object(const exprt &object, exprt &dest); void cpp_new_initializer( const exprt &lhs, @@ -376,14 +370,12 @@ class goto_convertt:public messaget void finish_computed_gotos(goto_programt &dest); void optimize_guarded_gotos(goto_programt &dest); - typedef std::map> + typedef std::map> labelst; - typedef std::list> - gotost; + typedef std::list> gotost; typedef std::list computed_gotost; typedef exprt::operandst caset; - typedef std::list > casest; + typedef std::list> casest; typedef std::map< goto_programt::targett, casest::iterator, @@ -395,8 +387,8 @@ class goto_convertt:public messaget goto_programt *prefix = nullptr; goto_programt *suffix = nullptr; - bool return_set, has_return_value, break_set, continue_set, - default_set, throw_set, leave_set; + bool return_set, has_return_value, break_set, continue_set, default_set, + throw_set, leave_set; labelst labels; gotost gotos; @@ -410,60 +402,60 @@ class goto_convertt:public messaget default_target, throw_target, leave_target; node_indext break_stack_node, continue_stack_node, throw_stack_node, - leave_stack_node; - - targetst(): - return_set(false), - has_return_value(false), - break_set(false), - continue_set(false), - default_set(false), - throw_set(false), - leave_set(false), - break_stack_node(), - continue_stack_node(), - throw_stack_node(), - leave_stack_node() + leave_stack_node; + + targetst() + : return_set(false), + has_return_value(false), + break_set(false), + continue_set(false), + default_set(false), + throw_set(false), + leave_set(false), + break_stack_node(), + continue_stack_node(), + throw_stack_node(), + leave_stack_node() { } void set_break(goto_programt::targett _break_target) { - break_set=true; - break_target=_break_target; + break_set = true; + break_target = _break_target; break_stack_node = scope_stack.get_current_node(); } void set_continue(goto_programt::targett _continue_target) { - continue_set=true; - continue_target=_continue_target; + continue_set = true; + continue_target = _continue_target; continue_stack_node = scope_stack.get_current_node(); } void set_default(goto_programt::targett _default_target) { - default_set=true; - default_target=_default_target; + default_set = true; + default_target = _default_target; } void set_return(goto_programt::targett _return_target) { - return_set=true; - return_target=_return_target; + return_set = true; + return_target = _return_target; } void set_throw(goto_programt::targett _throw_target) { - throw_set=true; - throw_target=_throw_target; + throw_set = true; + throw_target = _throw_target; throw_stack_node = scope_stack.get_current_node(); } void set_leave(goto_programt::targett _leave_target) { - leave_set=true; - leave_target=_leave_target; + leave_set = true; + leave_target = _leave_target; leave_stack_node = scope_stack.get_current_node(); } } targets; @@ -474,18 +466,18 @@ class goto_convertt:public messaget explicit break_continue_targetst(const targetst &targets) { - break_set=targets.break_set; - continue_set=targets.continue_set; - break_target=targets.break_target; - continue_target=targets.continue_target; + break_set = targets.break_set; + continue_set = targets.continue_set; + break_target = targets.break_target; + continue_target = targets.continue_target; } void restore(targetst &targets) { - targets.break_set=break_set; - targets.continue_set=continue_set; - targets.break_target=break_target; - targets.continue_target=continue_target; + targets.break_set = break_set; + targets.continue_set = continue_set; + targets.break_target = break_target; + targets.continue_target = continue_target; } goto_programt::targett break_target; @@ -499,23 +491,23 @@ class goto_convertt:public messaget explicit break_switch_targetst(const targetst &targets) { - break_set=targets.break_set; - default_set=targets.default_set; - break_target=targets.break_target; - default_target=targets.default_target; + break_set = targets.break_set; + default_set = targets.default_set; + break_target = targets.break_target; + default_target = targets.default_target; break_stack_node = targets.scope_stack.get_current_node(); - cases=targets.cases; - cases_map=targets.cases_map; + cases = targets.cases; + cases_map = targets.cases_map; } void restore(targetst &targets) { - targets.break_set=break_set; - targets.default_set=default_set; - targets.break_target=break_target; - targets.default_target=default_target; - targets.cases=cases; - targets.cases_map=cases_map; + targets.break_set = break_set; + targets.default_set = default_set; + targets.break_target = break_target; + targets.default_target = default_target; + targets.cases = cases; + targets.cases_map = cases_map; } goto_programt::targett break_target; @@ -533,15 +525,15 @@ class goto_convertt:public messaget explicit throw_targett(const targetst &targets) { - throw_set=targets.throw_set; - throw_target=targets.throw_target; + throw_set = targets.throw_set; + throw_target = targets.throw_target; throw_stack_node = targets.scope_stack.get_current_node(); } void restore(targetst &targets) { - targets.throw_set=throw_set; - targets.throw_target=throw_target; + targets.throw_set = throw_set; + targets.throw_target = throw_target; } goto_programt::targett throw_target; @@ -555,15 +547,15 @@ class goto_convertt:public messaget explicit leave_targett(const targetst &targets) { - leave_set=targets.leave_set; - leave_target=targets.leave_target; + leave_set = targets.leave_set; + leave_target = targets.leave_target; leave_stack_node = targets.scope_stack.get_current_node(); } void restore(targetst &targets) { - targets.leave_set=leave_set; - targets.leave_target=leave_target; + targets.leave_set = leave_set; + targets.leave_target = leave_target; } goto_programt::targett leave_target; @@ -571,9 +563,7 @@ class goto_convertt:public messaget node_indext leave_stack_node; }; - exprt case_guard( - const exprt &value, - const caset &case_op); + exprt case_guard(const exprt &value, const caset &case_op); // if(cond) { true_case } else { false_case } void generate_ifthenelse( diff --git a/src/ansi-c/goto-conversion/goto_convert_exceptions.cpp b/src/ansi-c/goto-conversion/goto_convert_exceptions.cpp index cc42054c27d5..f7a87a0554ce 100644 --- a/src/ansi-c/goto-conversion/goto_convert_exceptions.cpp +++ b/src/ansi-c/goto-conversion/goto_convert_exceptions.cpp @@ -101,7 +101,7 @@ void goto_convertt::convert_try_catch( // the CATCH-push instruction is annotated with a list of IDs, // one per target - code_push_catcht::exception_listt &exception_list= + code_push_catcht::exception_listt &exception_list = push_catch_code.exception_list(); // add a SKIP target for the end of everything @@ -119,9 +119,9 @@ void goto_convertt::convert_try_catch( // add a goto to the end of the 'try' block dest.add(goto_programt::make_goto(end_target)); - for(std::size_t i=1; icomplete_goto(y); @@ -151,7 +151,7 @@ void goto_convertt::do_function_call_other( { // don't know what to do with it code_function_callt function_call(lhs, function, arguments); - function_call.add_source_location()=function.source_location(); + function_call.add_source_location() = function.source_location(); dest.add(goto_programt::make_function_call( function_call, function.source_location())); } diff --git a/src/ansi-c/goto-conversion/goto_convert_functions.cpp b/src/ansi-c/goto-conversion/goto_convert_functions.cpp index c12dd711bf7f..07a3c3713e18 100644 --- a/src/ansi-c/goto-conversion/goto_convert_functions.cpp +++ b/src/ansi-c/goto-conversion/goto_convert_functions.cpp @@ -13,10 +13,10 @@ Date: June 2003 #include #include -#include - #include +#include + goto_convert_functionst::goto_convert_functionst( symbol_table_baset &_symbol_table, message_handlert &_message_handler) diff --git a/src/ansi-c/goto-conversion/goto_convert_functions.h b/src/ansi-c/goto-conversion/goto_convert_functions.h index b19d9008fa5b..70d1f856f667 100644 --- a/src/ansi-c/goto-conversion/goto_convert_functions.h +++ b/src/ansi-c/goto-conversion/goto_convert_functions.h @@ -27,9 +27,7 @@ void goto_convert( message_handlert &); // convert it all! -void goto_convert( - goto_modelt &, - message_handlert &); +void goto_convert(goto_modelt &, message_handlert &); // just convert a specific function void goto_convert( @@ -38,7 +36,7 @@ void goto_convert( goto_functionst &functions, message_handlert &); -class goto_convert_functionst:public goto_convertt +class goto_convert_functionst : public goto_convertt { public: void goto_convert(goto_functionst &functions); diff --git a/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp b/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp index 6c76fcbb2717..b5720722e68e 100644 --- a/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp +++ b/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp @@ -29,11 +29,11 @@ void goto_convertt::remove_assignment( bool address_taken, const irep_idt &mode) { - const irep_idt statement=expr.get_statement(); + const irep_idt statement = expr.get_statement(); std::optional replacement_expr_opt; - if(statement==ID_assign) + if(statement == ID_assign) { auto &old_assignment = to_side_effect_expr_assign(expr); exprt new_lhs = skip_typecast(old_assignment.lhs()); @@ -56,17 +56,13 @@ void goto_convertt::remove_assignment( convert_assign(new_assignment, dest, mode); } - else if(statement==ID_assign_plus || - statement==ID_assign_minus || - statement==ID_assign_mult || - statement==ID_assign_div || - statement==ID_assign_mod || - statement==ID_assign_shl || - statement==ID_assign_ashr || - statement==ID_assign_lshr || - statement==ID_assign_bitand || - statement==ID_assign_bitxor || - statement==ID_assign_bitor) + else if( + statement == ID_assign_plus || statement == ID_assign_minus || + statement == ID_assign_mult || statement == ID_assign_div || + statement == ID_assign_mod || statement == ID_assign_shl || + statement == ID_assign_ashr || statement == ID_assign_lshr || + statement == ID_assign_bitand || statement == ID_assign_bitxor || + statement == ID_assign_bitor) { INVARIANT_WITH_DIAGNOSTICS( expr.operands().size() == 2, @@ -75,28 +71,28 @@ void goto_convertt::remove_assignment( irep_idt new_id; - if(statement==ID_assign_plus) - new_id=ID_plus; - else if(statement==ID_assign_minus) - new_id=ID_minus; - else if(statement==ID_assign_mult) - new_id=ID_mult; - else if(statement==ID_assign_div) - new_id=ID_div; - else if(statement==ID_assign_mod) - new_id=ID_mod; - else if(statement==ID_assign_shl) - new_id=ID_shl; - else if(statement==ID_assign_ashr) - new_id=ID_ashr; - else if(statement==ID_assign_lshr) - new_id=ID_lshr; - else if(statement==ID_assign_bitand) - new_id=ID_bitand; - else if(statement==ID_assign_bitxor) - new_id=ID_bitxor; - else if(statement==ID_assign_bitor) - new_id=ID_bitor; + if(statement == ID_assign_plus) + new_id = ID_plus; + else if(statement == ID_assign_minus) + new_id = ID_minus; + else if(statement == ID_assign_mult) + new_id = ID_mult; + else if(statement == ID_assign_div) + new_id = ID_div; + else if(statement == ID_assign_mod) + new_id = ID_mod; + else if(statement == ID_assign_shl) + new_id = ID_shl; + else if(statement == ID_assign_ashr) + new_id = ID_ashr; + else if(statement == ID_assign_lshr) + new_id = ID_lshr; + else if(statement == ID_assign_bitand) + new_id = ID_bitand; + else if(statement == ID_assign_bitxor) + new_id = ID_bitxor; + else if(statement == ID_assign_bitor) + new_id = ID_bitor; else { UNREACHABLE; @@ -125,7 +121,7 @@ void goto_convertt::remove_assignment( rhs = typecast_exprt::conditional_cast(rhs, new_lhs.type()); rhs.add_source_location() = expr.source_location(); code_assignt assignment(new_lhs, rhs); - assignment.add_source_location()=expr.source_location(); + assignment.add_source_location() = expr.source_location(); convert(assignment, dest, mode); } @@ -177,7 +173,7 @@ void goto_convertt::remove_pre( "preincrement/predecrement must have one operand", expr.find_source_location()); - const irep_idt statement=expr.get_statement(); + const irep_idt statement = expr.get_statement(); DATA_INVARIANT( statement == ID_preincrement || statement == ID_predecrement, @@ -235,7 +231,7 @@ void goto_convertt::remove_pre( make_temp_symbol(rhs, "pre", dest, mode); code_assignt assignment(lhs, rhs); - assignment.add_source_location()=expr.find_source_location(); + assignment.add_source_location() = expr.find_source_location(); convert(assignment, dest, mode); @@ -272,7 +268,7 @@ void goto_convertt::remove_post( "postincrement/postdecrement must have one operand", expr.find_source_location()); - const irep_idt statement=expr.get_statement(); + const irep_idt statement = expr.get_statement(); DATA_INVARIANT( statement == ID_postincrement || statement == ID_postdecrement, @@ -314,7 +310,7 @@ void goto_convertt::remove_post( rhs.add_source_location() = expr.source_location(); code_assignt assignment(op, rhs); - assignment.add_source_location()=expr.find_source_location(); + assignment.add_source_location() = expr.find_source_location(); convert(assignment, tmp2, mode); @@ -349,7 +345,7 @@ void goto_convertt::remove_function_call( if(!result_is_used) { code_function_callt call(expr.function(), expr.arguments()); - call.add_source_location()=expr.source_location(); + call.add_source_location() = expr.source_location(); convert_function_call(call, dest, mode); expr.make_nil(); return; @@ -365,8 +361,8 @@ void goto_convertt::remove_function_call( to_symbol_expr(expr.function()).get_identifier(); const symbolt &symbol = ns.lookup(identifier); - new_base_name+='_'; - new_base_name+=id2string(symbol.base_name); + new_base_name += '_'; + new_base_name += id2string(symbol.base_name); new_symbol_mode = symbol.mode; } @@ -380,7 +376,7 @@ void goto_convertt::remove_function_call( { code_frontend_declt decl(new_symbol.symbol_expr()); - decl.add_source_location()=new_symbol.location; + decl.add_source_location() = new_symbol.location; convert_frontend_decl(decl, dest, mode); } @@ -388,19 +384,17 @@ void goto_convertt::remove_function_call( goto_programt tmp_program2; code_function_callt call( new_symbol.symbol_expr(), expr.function(), expr.arguments()); - call.add_source_location()=new_symbol.location; + call.add_source_location() = new_symbol.location; convert_function_call(call, dest, mode); } - static_cast(expr)=new_symbol.symbol_expr(); + static_cast(expr) = new_symbol.symbol_expr(); } -void goto_convertt::replace_new_object( - const exprt &object, - exprt &dest) +void goto_convertt::replace_new_object(const exprt &object, exprt &dest) { - if(dest.id()=="new_object") - dest=object; + if(dest.id() == "new_object") + dest = object; else Forall_operands(it, dest) replace_new_object(object, *it); @@ -420,13 +414,13 @@ void goto_convertt::remove_cpp_new( symbol_table); code_frontend_declt decl(new_symbol.symbol_expr()); - decl.add_source_location()=new_symbol.location; + decl.add_source_location() = new_symbol.location; convert_frontend_decl(decl, dest, ID_cpp); const code_assignt call(new_symbol.symbol_expr(), expr); if(result_is_used) - static_cast(expr)=new_symbol.symbol_expr(); + static_cast(expr) = new_symbol.symbol_expr(); else expr.make_nil(); @@ -440,7 +434,7 @@ void goto_convertt::remove_cpp_delete( DATA_INVARIANT(expr.operands().size() == 1, "cpp_delete expects one operand"); codet tmp(expr.get_statement()); - tmp.add_source_location()=expr.source_location(); + tmp.add_source_location() = expr.source_location(); tmp.copy_to_operands(to_unary_expr(expr).op()); tmp.set(ID_destructor, expr.find(ID_destructor)); @@ -466,13 +460,13 @@ void goto_convertt::remove_malloc( symbol_table); code_frontend_declt decl(new_symbol.symbol_expr()); - decl.add_source_location()=new_symbol.location; + decl.add_source_location() = new_symbol.location; convert_frontend_decl(decl, dest, mode); code_assignt call(new_symbol.symbol_expr(), expr); - call.add_source_location()=expr.source_location(); + call.add_source_location() = expr.source_location(); - static_cast(expr)=new_symbol.symbol_expr(); + static_cast(expr) = new_symbol.symbol_expr(); convert(call, dest, mode); } @@ -492,10 +486,10 @@ void goto_convertt::remove_temporary_object( "temporary_object takes zero or one operands", expr.find_source_location()); - symbolt &new_symbol = new_tmp_symbol( - expr.type(), "obj", dest, expr.find_source_location(), mode); + symbolt &new_symbol = + new_tmp_symbol(expr.type(), "obj", dest, expr.find_source_location(), mode); - if(expr.operands().size()==1) + if(expr.operands().size() == 1) { const code_assignt assignment( new_symbol.symbol_expr(), to_unary_expr(expr).op()); @@ -509,13 +503,13 @@ void goto_convertt::remove_temporary_object( expr.operands().empty(), "temporary_object takes zero operands", expr.find_source_location()); - exprt initializer=static_cast(expr.find(ID_initializer)); + exprt initializer = static_cast(expr.find(ID_initializer)); replace_new_object(new_symbol.symbol_expr(), initializer); convert(to_code(initializer), dest, mode); } - static_cast(expr)=new_symbol.symbol_expr(); + static_cast(expr) = new_symbol.symbol_expr(); } void goto_convertt::remove_statement_expression( @@ -549,28 +543,28 @@ void goto_convertt::remove_statement_expression( expr.find_source_location()); // get last statement from block, following labels - codet &last=to_code_block(code).find_last_statement(); + codet &last = to_code_block(code).find_last_statement(); - source_locationt source_location=last.find_source_location(); + source_locationt source_location = last.find_source_location(); symbolt &new_symbol = new_tmp_symbol( expr.type(), "statement_expression", dest, source_location, mode); symbol_exprt tmp_symbol_expr(new_symbol.name, new_symbol.type); - tmp_symbol_expr.add_source_location()=source_location; + tmp_symbol_expr.add_source_location() = source_location; - if(last.get(ID_statement)==ID_expression) + if(last.get(ID_statement) == ID_expression) { // we turn this into an assignment - exprt e=to_code_expression(last).expression(); - last=code_assignt(tmp_symbol_expr, e); - last.add_source_location()=source_location; + exprt e = to_code_expression(last).expression(); + last = code_assignt(tmp_symbol_expr, e); + last.add_source_location() = source_location; } - else if(last.get(ID_statement)==ID_assign) + else if(last.get(ID_statement) == ID_assign) { - exprt e=to_code_assign(last).lhs(); + exprt e = to_code_assign(last).lhs(); code_assignt assignment(tmp_symbol_expr, e); - assignment.add_source_location()=source_location; + assignment.add_source_location() = source_location; code.operands().push_back(assignment); } else @@ -584,7 +578,7 @@ void goto_convertt::remove_statement_expression( dest.destructive_append(tmp); } - static_cast(expr)=tmp_symbol_expr; + static_cast(expr) = tmp_symbol_expr; } void goto_convertt::remove_overflow( @@ -621,12 +615,10 @@ void goto_convertt::remove_overflow( else { const typet &arith_type = to_pointer_type(result.type()).base_type(); - irep_idt arithmetic_operation = - statement == ID_overflow_plus - ? ID_plus - : statement == ID_overflow_minus - ? ID_minus - : statement == ID_overflow_mult ? ID_mult : ID_nil; + irep_idt arithmetic_operation = statement == ID_overflow_plus ? ID_plus + : statement == ID_overflow_minus ? ID_minus + : statement == ID_overflow_mult ? ID_mult + : ID_nil; CHECK_RETURN(arithmetic_operation != ID_nil); exprt overflow_with_result = overflow_result_exprt{ typecast_exprt::conditional_cast(lhs, arith_type), @@ -666,51 +658,42 @@ void goto_convertt::remove_side_effect( bool result_is_used, bool address_taken) { - const irep_idt &statement=expr.get_statement(); + const irep_idt &statement = expr.get_statement(); - if(statement==ID_function_call) + if(statement == ID_function_call) remove_function_call( to_side_effect_expr_function_call(expr), dest, mode, result_is_used); - else if(statement==ID_assign || - statement==ID_assign_plus || - statement==ID_assign_minus || - statement==ID_assign_mult || - statement==ID_assign_div || - statement==ID_assign_bitor || - statement==ID_assign_bitxor || - statement==ID_assign_bitand || - statement==ID_assign_lshr || - statement==ID_assign_ashr || - statement==ID_assign_shl || - statement==ID_assign_mod) + else if( + statement == ID_assign || statement == ID_assign_plus || + statement == ID_assign_minus || statement == ID_assign_mult || + statement == ID_assign_div || statement == ID_assign_bitor || + statement == ID_assign_bitxor || statement == ID_assign_bitand || + statement == ID_assign_lshr || statement == ID_assign_ashr || + statement == ID_assign_shl || statement == ID_assign_mod) remove_assignment(expr, dest, result_is_used, address_taken, mode); - else if(statement==ID_postincrement || - statement==ID_postdecrement) + else if(statement == ID_postincrement || statement == ID_postdecrement) remove_post(expr, dest, mode, result_is_used); - else if(statement==ID_preincrement || - statement==ID_predecrement) + else if(statement == ID_preincrement || statement == ID_predecrement) remove_pre(expr, dest, result_is_used, address_taken, mode); - else if(statement==ID_cpp_new || - statement==ID_cpp_new_array) + else if(statement == ID_cpp_new || statement == ID_cpp_new_array) remove_cpp_new(expr, dest, result_is_used); - else if(statement==ID_cpp_delete || - statement==ID_cpp_delete_array) + else if(statement == ID_cpp_delete || statement == ID_cpp_delete_array) remove_cpp_delete(expr, dest); - else if(statement==ID_allocate) + else if(statement == ID_allocate) remove_malloc(expr, dest, mode, result_is_used); - else if(statement==ID_temporary_object) + else if(statement == ID_temporary_object) remove_temporary_object(expr, dest); - else if(statement==ID_statement_expression) + else if(statement == ID_statement_expression) remove_statement_expression(expr, dest, mode, result_is_used); - else if(statement==ID_nondet) + else if(statement == ID_nondet) { // these are fine } - else if(statement==ID_skip) + else if(statement == ID_skip) { expr.make_nil(); } - else if(statement==ID_throw) + else if(statement == ID_throw) { codet code = code_expressiont(side_effect_expr_throwt( expr.find(ID_exception_list), expr.type(), expr.source_location())); diff --git a/src/ansi-c/goto-conversion/link_to_library.cpp b/src/ansi-c/goto-conversion/link_to_library.cpp index b66fe9fec938..cc814e1965ad 100644 --- a/src/ansi-c/goto-conversion/link_to_library.cpp +++ b/src/ansi-c/goto-conversion/link_to_library.cpp @@ -11,12 +11,12 @@ Author: Daniel Kroening, kroening@kroening.com #include "link_to_library.h" -#include - #include #include #include +#include + #include "goto_convert_functions.h" /// Try to add \p missing_function from \p library to \p goto_model. diff --git a/src/ansi-c/goto-conversion/link_to_library.h b/src/ansi-c/goto-conversion/link_to_library.h index 8ddf2d3b0b88..4420fa4b7253 100644 --- a/src/ansi-c/goto-conversion/link_to_library.h +++ b/src/ansi-c/goto-conversion/link_to_library.h @@ -12,11 +12,11 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_PROGRAMS_LINK_TO_LIBRARY_H #define CPROVER_GOTO_PROGRAMS_LINK_TO_LIBRARY_H +#include + #include #include -#include - class goto_modelt; class message_handlert; class symbol_tablet; diff --git a/src/ansi-c/goto-conversion/string_instrumentation.cpp b/src/ansi-c/goto-conversion/string_instrumentation.cpp index 84138e98d4cb..873dee0006ec 100644 --- a/src/ansi-c/goto-conversion/string_instrumentation.cpp +++ b/src/ansi-c/goto-conversion/string_instrumentation.cpp @@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "string_instrumentation.h" -#include - #include #include #include @@ -25,6 +23,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "format_strings.h" +#include + exprt is_zero_string(const exprt &what, bool write) { unary_exprt result{"is_zero_string", what, c_bool_type()}; @@ -33,9 +33,7 @@ exprt is_zero_string(const exprt &what, bool write) return notequal_exprt{result, from_integer(0, c_bool_type())}; } -exprt zero_string_length( - const exprt &what, - bool write) +exprt zero_string_length(const exprt &what, bool write) { exprt result("zero_string_length", size_type()); result.copy_to_operands(what); @@ -67,7 +65,7 @@ class string_instrumentationt void make_type(exprt &dest, const typet &type) { - if(ns.follow(dest.type())!=ns.follow(type)) + if(ns.follow(dest.type()) != ns.follow(type)) dest = typecast_exprt(dest, type); } @@ -177,16 +175,13 @@ void string_instrumentation( void string_instrumentation(goto_modelt &goto_model) { - string_instrumentation( - goto_model.symbol_table, - goto_model.goto_functions); + string_instrumentation(goto_model.symbol_table, goto_model.goto_functions); } void string_instrumentationt::operator()(goto_functionst &dest) { - for(goto_functionst::function_mapt::iterator - it=dest.function_map.begin(); - it!=dest.function_map.end(); + for(goto_functionst::function_mapt::iterator it = dest.function_map.begin(); + it != dest.function_map.end(); it++) { (*this)(it->second.body); @@ -215,41 +210,40 @@ void string_instrumentationt::do_function_call( const exprt &function = as_const(*target).call_function(); const auto &arguments = as_const(*target).call_arguments(); - if(function.id()==ID_symbol) + if(function.id() == ID_symbol) { - const irep_idt &identifier= - to_symbol_expr(function).get_identifier(); + const irep_idt &identifier = to_symbol_expr(function).get_identifier(); - if(identifier=="strcoll") + if(identifier == "strcoll") { } - else if(identifier=="strncmp") + else if(identifier == "strncmp") do_strncmp(dest, target, lhs, arguments); - else if(identifier=="strxfrm") + else if(identifier == "strxfrm") { } - else if(identifier=="strchr") + else if(identifier == "strchr") do_strchr(dest, target, lhs, arguments); - else if(identifier=="strcspn") + else if(identifier == "strcspn") { } - else if(identifier=="strpbrk") + else if(identifier == "strpbrk") { } - else if(identifier=="strrchr") + else if(identifier == "strrchr") do_strrchr(dest, target, lhs, arguments); - else if(identifier=="strspn") + else if(identifier == "strspn") { } - else if(identifier=="strerror") + else if(identifier == "strerror") do_strerror(dest, target, lhs, arguments); - else if(identifier=="strstr") + else if(identifier == "strstr") do_strstr(dest, target, lhs, arguments); - else if(identifier=="strtok") + else if(identifier == "strtok") do_strtok(dest, target, lhs, arguments); - else if(identifier=="sprintf") + else if(identifier == "sprintf") do_sprintf(dest, target, lhs, arguments); - else if(identifier=="snprintf") + else if(identifier == "snprintf") do_snprintf(dest, target, lhs, arguments); else if(identifier == "fscanf" || identifier == "__isoc99_fscanf") do_fscanf(dest, target, lhs, arguments); @@ -264,7 +258,7 @@ void string_instrumentationt::do_sprintf( const exprt &lhs, const exprt::operandst &arguments) { - if(arguments.size()<2) + if(arguments.size() < 2) { throw invalid_source_file_exceptiont( "sprintf expected to have two or more arguments", @@ -300,7 +294,7 @@ void string_instrumentationt::do_snprintf( const exprt &lhs, const exprt::operandst &arguments) { - if(arguments.size()<3) + if(arguments.size() < 3) { throw invalid_source_file_exceptiont( "snprintf expected to have three or more arguments", @@ -337,7 +331,7 @@ void string_instrumentationt::do_fscanf( const exprt &lhs, const exprt::operandst &arguments) { - if(arguments.size()<2) + if(arguments.size() < 2) { throw invalid_source_file_exceptiont( "fscanf expected to have two or more arguments", @@ -368,7 +362,7 @@ void string_instrumentationt::do_format_string_read( std::size_t argument_start_inx, const std::string &function_name) { - const exprt &format_arg=arguments[format_string_inx]; + const exprt &format_arg = arguments[format_string_inx]; if( format_arg.id() == ID_address_of && @@ -381,22 +375,22 @@ void string_instrumentationt::do_format_string_read( to_index_expr(to_address_of_expr(format_arg).object()).array()) .value())); - std::size_t args=0; + std::size_t args = 0; for(const auto &token : token_list) { - if(token.type==format_tokent::token_typet::STRING) + if(token.type == format_tokent::token_typet::STRING) { - const exprt &arg=arguments[argument_start_inx+args]; + const exprt &arg = arguments[argument_start_inx + args]; - if(arg.id()!=ID_string_constant) // we don't need to check constants + if(arg.id() != ID_string_constant) // we don't need to check constants { exprt temp(arg); if(arg.type().id() != ID_pointer) { index_exprt index(temp, from_integer(0, c_index_type())); - temp=address_of_exprt(index); + temp = address_of_exprt(index); } source_locationt annotated_location = target->source_location(); @@ -409,14 +403,16 @@ void string_instrumentationt::do_format_string_read( } } - if(token.type!=format_tokent::token_typet::TEXT && - token.type!=format_tokent::token_typet::UNKNOWN) args++; + if( + token.type != format_tokent::token_typet::TEXT && + token.type != format_tokent::token_typet::UNKNOWN) + args++; - if(find( - token.flags.begin(), - token.flags.end(), - format_tokent::flag_typet::ASTERISK)!= - token.flags.end()) + if( + find( + token.flags.begin(), + token.flags.end(), + format_tokent::flag_typet::ASTERISK) != token.flags.end()) args++; // just eat the additional argument } } @@ -429,9 +425,9 @@ void string_instrumentationt::do_format_string_read( dest.add(goto_programt::make_assertion( is_zero_string(arguments[1]), annotated_location)); - for(std::size_t i=2; isource_location(); @@ -462,7 +458,7 @@ void string_instrumentationt::do_format_string_write( std::size_t argument_start_inx, const std::string &function_name) { - const exprt &format_arg=arguments[format_string_inx]; + const exprt &format_arg = arguments[format_string_inx]; if( format_arg.id() == ID_address_of && @@ -475,96 +471,94 @@ void string_instrumentationt::do_format_string_write( to_index_expr(to_address_of_expr(format_arg).object()).array()) .value())); - std::size_t args=0; + std::size_t args = 0; for(const auto &token : token_list) { - if(find( - token.flags.begin(), - token.flags.end(), - format_tokent::flag_typet::ASTERISK)!= - token.flags.end()) + if( + find( + token.flags.begin(), + token.flags.end(), + format_tokent::flag_typet::ASTERISK) != token.flags.end()) continue; // asterisk means `ignore this' switch(token.type) { - case format_tokent::token_typet::STRING: + case format_tokent::token_typet::STRING: + { + const exprt &argument = arguments[argument_start_inx + args]; + const typet &arg_type = argument.type(); + + exprt condition; + + if(token.field_width != 0) { - const exprt &argument=arguments[argument_start_inx+args]; - const typet &arg_type = argument.type(); + exprt fwidth = from_integer(token.field_width, unsigned_int_type()); + exprt one = from_integer(1, unsigned_int_type()); + const plus_exprt fw_1(fwidth, one); // +1 for 0-char - exprt condition; + exprt fw_lt_bs; - if(token.field_width!=0) - { - exprt fwidth=from_integer(token.field_width, unsigned_int_type()); - exprt one=from_integer(1, unsigned_int_type()); - const plus_exprt fw_1(fwidth, one); // +1 for 0-char - - exprt fw_lt_bs; - - if(arg_type.id()==ID_pointer) - fw_lt_bs= - binary_relation_exprt(fw_1, ID_le, buffer_size(argument)); - else - { - const index_exprt index( - argument, from_integer(0, unsigned_int_type())); - address_of_exprt aof(index); - fw_lt_bs=binary_relation_exprt(fw_1, ID_le, buffer_size(aof)); - } - - condition = fw_lt_bs; - } + if(arg_type.id() == ID_pointer) + fw_lt_bs = + binary_relation_exprt(fw_1, ID_le, buffer_size(argument)); else { - // this is a possible overflow. - condition = false_exprt(); + const index_exprt index( + argument, from_integer(0, unsigned_int_type())); + address_of_exprt aof(index); + fw_lt_bs = binary_relation_exprt(fw_1, ID_le, buffer_size(aof)); } - source_locationt annotated_location = target->source_location(); - annotated_location.set_property_class("string"); - std::string comment("format string buffer overflow in "); - comment += function_name; - annotated_location.set_comment(comment); - dest.add( - goto_programt::make_assertion(condition, annotated_location)); - - // now kill the contents - invalidate_buffer( - dest, target, argument, arg_type, token.field_width); - - args++; - break; + condition = fw_lt_bs; } - case format_tokent::token_typet::TEXT: - case format_tokent::token_typet::UNKNOWN: + else { - // nothing - break; + // this is a possible overflow. + condition = false_exprt(); } - case format_tokent::token_typet::POINTER: - case format_tokent::token_typet::CHAR: - case format_tokent::token_typet::FLOAT: - case format_tokent::token_typet::INT: - { - const exprt &argument=arguments[argument_start_inx+args]; - const dereference_exprt lhs{argument}; - side_effect_expr_nondett rhs(lhs.type(), target->source_location()); + source_locationt annotated_location = target->source_location(); + annotated_location.set_property_class("string"); + std::string comment("format string buffer overflow in "); + comment += function_name; + annotated_location.set_comment(comment); + dest.add(goto_programt::make_assertion(condition, annotated_location)); - dest.add(goto_programt::make_assignment( - lhs, rhs, target->source_location())); + // now kill the contents + invalidate_buffer(dest, target, argument, arg_type, token.field_width); - args++; - break; - } + args++; + break; + } + case format_tokent::token_typet::TEXT: + case format_tokent::token_typet::UNKNOWN: + { + // nothing + break; + } + case format_tokent::token_typet::POINTER: + case format_tokent::token_typet::CHAR: + case format_tokent::token_typet::FLOAT: + case format_tokent::token_typet::INT: + { + const exprt &argument = arguments[argument_start_inx + args]; + const dereference_exprt lhs{argument}; + + side_effect_expr_nondett rhs(lhs.type(), target->source_location()); + + dest.add( + goto_programt::make_assignment(lhs, rhs, target->source_location())); + + args++; + break; + } } } } else // non-const format string { - for(std::size_t i=argument_start_inx; isource_location()); @@ -637,7 +631,7 @@ void string_instrumentationt::do_strrchr( const exprt &lhs, const exprt::operandst &arguments) { - if(arguments.size()!=2) + if(arguments.size() != 2) { throw invalid_source_file_exceptiont( "strrchr expected to have two arguments", target->source_location()); @@ -660,7 +654,7 @@ void string_instrumentationt::do_strstr( const exprt &lhs, const exprt::operandst &arguments) { - if(arguments.size()!=2) + if(arguments.size() != 2) { throw invalid_source_file_exceptiont( "strstr expected to have two arguments", target->source_location()); @@ -691,7 +685,7 @@ void string_instrumentationt::do_strtok( const exprt &lhs, const exprt::operandst &arguments) { - if(arguments.size()!=2) + if(arguments.size() != 2) { throw invalid_source_file_exceptiont( "strtok expected to have two arguments", target->source_location()); @@ -728,32 +722,32 @@ void string_instrumentationt::do_strerror( return; } - irep_idt identifier_buf="__strerror_buffer"; - irep_idt identifier_size="__strerror_buffer_size"; + irep_idt identifier_buf = "__strerror_buffer"; + irep_idt identifier_size = "__strerror_buffer_size"; - if(symbol_table.symbols.find(identifier_buf)==symbol_table.symbols.end()) + if(symbol_table.symbols.find(identifier_buf) == symbol_table.symbols.end()) { symbolt new_symbol_size{identifier_size, size_type(), ID_C}; new_symbol_size.base_name = identifier_size; - new_symbol_size.pretty_name=new_symbol_size.base_name; - new_symbol_size.is_state_var=true; - new_symbol_size.is_lvalue=true; - new_symbol_size.is_static_lifetime=true; + new_symbol_size.pretty_name = new_symbol_size.base_name; + new_symbol_size.is_state_var = true; + new_symbol_size.is_lvalue = true; + new_symbol_size.is_static_lifetime = true; array_typet type(char_type(), new_symbol_size.symbol_expr()); symbolt new_symbol_buf{identifier_buf, type, ID_C}; - new_symbol_buf.is_state_var=true; - new_symbol_buf.is_lvalue=true; - new_symbol_buf.is_static_lifetime=true; + new_symbol_buf.is_state_var = true; + new_symbol_buf.is_lvalue = true; + new_symbol_buf.is_static_lifetime = true; new_symbol_buf.base_name = identifier_buf; - new_symbol_buf.pretty_name=new_symbol_buf.base_name; + new_symbol_buf.pretty_name = new_symbol_buf.base_name; symbol_table.insert(std::move(new_symbol_buf)); symbol_table.insert(std::move(new_symbol_size)); } - const symbolt &symbol_size=ns.lookup(identifier_size); - const symbolt &symbol_buf=ns.lookup(identifier_buf); + const symbolt &symbol_size = ns.lookup(identifier_size); + const symbolt &symbol_buf = ns.lookup(identifier_buf); goto_programt tmp; @@ -786,7 +780,7 @@ void string_instrumentationt::do_strerror( // assign address { - exprt rhs=ptr; + exprt rhs = ptr; make_type(rhs, lhs.type()); tmp.add(goto_programt::make_assignment( code_assignt(lhs, rhs), it->source_location())); @@ -803,21 +797,21 @@ void string_instrumentationt::invalidate_buffer( const typet &buf_type, const mp_integer &limit) { - irep_idt cntr_id="string_instrumentation::$counter"; + irep_idt cntr_id = "string_instrumentation::$counter"; - if(symbol_table.symbols.find(cntr_id)==symbol_table.symbols.end()) + if(symbol_table.symbols.find(cntr_id) == symbol_table.symbols.end()) { symbolt new_symbol{cntr_id, size_type(), ID_C}; - new_symbol.base_name="$counter"; - new_symbol.pretty_name=new_symbol.base_name; - new_symbol.is_state_var=true; - new_symbol.is_lvalue=true; - new_symbol.is_static_lifetime=true; + new_symbol.base_name = "$counter"; + new_symbol.pretty_name = new_symbol.base_name; + new_symbol.is_state_var = true; + new_symbol.is_lvalue = true; + new_symbol.is_static_lifetime = true; symbol_table.insert(std::move(new_symbol)); } - const symbolt &cntr_sym=ns.lookup(cntr_id); + const symbolt &cntr_sym = ns.lookup(cntr_id); // create a loop that runs over the buffer // and invalidates every element @@ -829,20 +823,20 @@ void string_instrumentationt::invalidate_buffer( exprt bufp; - if(buf_type.id()==ID_pointer) - bufp=buffer; + if(buf_type.id() == ID_pointer) + bufp = buffer; else { index_exprt index( buffer, from_integer(0, c_index_type()), to_type_with_subtype(buf_type).subtype()); - bufp=address_of_exprt(index); + bufp = address_of_exprt(index); } exprt condition; - if(limit==0) + if(limit == 0) condition = binary_relation_exprt(cntr_sym.symbol_expr(), ID_ge, buffer_size(bufp)); else diff --git a/src/ansi-c/goto-conversion/string_instrumentation.h b/src/ansi-c/goto-conversion/string_instrumentation.h index 646f803e3c87..fd57d0306d64 100644 --- a/src/ansi-c/goto-conversion/string_instrumentation.h +++ b/src/ansi-c/goto-conversion/string_instrumentation.h @@ -25,7 +25,7 @@ void string_instrumentation(symbol_table_baset &, goto_functionst &); void string_instrumentation(goto_modelt &); exprt is_zero_string(const exprt &what, bool write = false); -exprt zero_string_length(const exprt &what, bool write=false); +exprt zero_string_length(const exprt &what, bool write = false); exprt buffer_size(const exprt &what); #endif // CPROVER_GOTO_PROGRAMS_STRING_INSTRUMENTATION_H diff --git a/src/ansi-c/printf_formatter.h b/src/ansi-c/printf_formatter.h index ab8dda2d9f53..45968da45ba5 100644 --- a/src/ansi-c/printf_formatter.h +++ b/src/ansi-c/printf_formatter.h @@ -19,16 +19,12 @@ Author: Daniel Kroening, kroening@kroening.com class printf_formattert { public: - void operator()( - const std::string &format, - const std::list &_operands); + void operator()(const std::string &format, const std::list &_operands); void print(std::ostream &out); std::string as_string(); - explicit printf_formattert(const namespacet &_ns): - ns(_ns), - format_pos(0) + explicit printf_formattert(const namespacet &_ns) : ns(_ns), format_pos(0) { } @@ -38,9 +34,14 @@ class printf_formattert std::list operands; std::list::const_iterator next_operand; unsigned format_pos; - bool eol() const { return format_pos>=format.size(); } + bool eol() const + { + return format_pos >= format.size(); + } - class eol_exceptiont { }; + class eol_exceptiont + { + }; char next() { diff --git a/unit/ansi-c/allocate_objects.cpp b/unit/ansi-c/allocate_objects.cpp index 8f4a97f6d09b..3f33bede78e0 100644 --- a/unit/ansi-c/allocate_objects.cpp +++ b/unit/ansi-c/allocate_objects.cpp @@ -6,11 +6,10 @@ Author: Diffblue Ltd \*******************************************************************/ -#include - #include #include +#include #include TEST_CASE(