diff --git a/CODING_STANDARD.md b/CODING_STANDARD.md index c5d67173e14..c218cdf859b 100644 --- a/CODING_STANDARD.md +++ b/CODING_STANDARD.md @@ -19,7 +19,10 @@ Formatting is enforced using clang-format. For more information about this, see - Nested function calls do not need to be broken up into separate lines even if the outer function call does. - If a method is bigger than 50 lines, break it into parts. -- Put matching `{ }` into the same column. +- Put matching `{ }` into the same column, except for initializer lists and + lambdas, where you should place `{` directly after the closing `)`. This is + to comply with clang-format, which doesn't support aligned curly braces in + these cases. - Spaces around binary operators (`=`, `+`, `==` ...) - Space after comma (parameter lists, argument lists, ...) - Space after colon inside `for` diff --git a/scripts/cpplint.py b/scripts/cpplint.py index bb08391f4d9..d01baeb2fcf 100755 --- a/scripts/cpplint.py +++ b/scripts/cpplint.py @@ -3972,14 +3972,6 @@ def CheckBracesSpacing(filename, clean_lines, linenum, nesting_state, error): error(filename, linenum, 'whitespace/braces', 5, 'Missing space before {') - # Make sure '} else {' has spaces. - # if Search(r'}else', line): - # error(filename, linenum, 'whitespace/braces', 5, - # 'Missing space before else') - if (Search(r'^.*[^\s].*}$', line) or Search(r'^.*[^\s].*{$', line)) and not(Search(r'{[^}]*}', line)): - error(filename, linenum, 'whitespace/braces', 5, - 'Put braces on a separate next line') - # You shouldn't have a space before a semicolon at the end of the line. # There's a special case for "for" since the style guide allows space before # the semicolon there. diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 2bca47c7723..453679bc639 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -1823,10 +1823,8 @@ void goto_convertt::generate_ifthenelse( // Note this depends on the fact that `instructions` is a std::list // and so goto-program-destructive-append preserves iterator validity. if(is_guarded_goto) - guarded_gotos.push_back({ // NOLINT(whitespace/braces) - tmp_v.instructions.begin(), - tmp_w.instructions.begin(), - guard}); + guarded_gotos.push_back( + {tmp_v.instructions.begin(), tmp_w.instructions.begin(), guard}); dest.destructive_append(tmp_v); dest.destructive_append(tmp_w); diff --git a/src/goto-programs/lazy_goto_model.h b/src/goto-programs/lazy_goto_model.h index 78b078cadc2..417115024ce 100644 --- a/src/goto-programs/lazy_goto_model.h +++ b/src/goto-programs/lazy_goto_model.h @@ -53,11 +53,11 @@ class lazy_goto_modelt : public abstract_goto_modelt message_handlert &message_handler) { return lazy_goto_modelt( - [&handler, &options] - (goto_model_functiont &fun, const abstract_goto_modelt &model) { // NOLINT(*) + [&handler, + &options](goto_model_functiont &fun, const abstract_goto_modelt &model) { handler.process_goto_function(fun, model, options); }, - [&handler, &options] (goto_modelt &goto_model) -> bool { // NOLINT(*) + [&handler, &options](goto_modelt &goto_model) -> bool { return handler.process_goto_functions(goto_model, options); }, message_handler); diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 8c33d25541d..ed1d391690d 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -166,8 +166,8 @@ void goto_symext::symex_threaded_step( static goto_symext::get_goto_functiont get_function_from_goto_functions( const goto_functionst &goto_functions) { - return [&goto_functions](const irep_idt &key) -> - const goto_functionst::goto_functiont & { // NOLINT(*) + return [&goto_functions]( + const irep_idt &key) -> const goto_functionst::goto_functiont & { return goto_functions.function_map.at(key); }; } diff --git a/src/java_bytecode/expr2java.h b/src/java_bytecode/expr2java.h index 2adb417eb03..1df94bdc9ce 100644 --- a/src/java_bytecode/expr2java.h +++ b/src/java_bytecode/expr2java.h @@ -66,7 +66,7 @@ std::string floating_point_to_java_string(float_type value) return class_name + ".POSITIVE_INFINITY"; if(std::isinf(value) && value <= 0.) return class_name + ".NEGATIVE_INFINITY"; - const std::string decimal = [&]() -> std::string { // NOLINT + const std::string decimal = [&]() -> std::string { // Using ostringstream instead of to_string to get string without // trailing zeros std::ostringstream raw_stream; @@ -76,7 +76,7 @@ std::string floating_point_to_java_string(float_type value) return raw_decimal + ".0"; return raw_decimal; }(); - const bool is_lossless = [&] { // NOLINT + const bool is_lossless = [&] { if(value == std::numeric_limits::min()) return true; try @@ -88,7 +88,7 @@ std::string floating_point_to_java_string(float_type value) return false; } }(); - const std::string lossless = [&]() -> std::string { // NOLINT + const std::string lossless = [&]() -> std::string { if(is_lossless) return decimal; std::ostringstream stream; diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index cdc75bad6dd..9b221d4298c 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -895,10 +895,8 @@ static void gather_symbol_live_ranges( if(e.id()==ID_symbol) { const auto &symexpr=to_symbol_expr(e); - auto findit= - result.insert({ // NOLINT(whitespace/braces) - symexpr.get_identifier(), - java_bytecode_convert_methodt::variablet()}); + auto findit = result.insert( + {symexpr.get_identifier(), java_bytecode_convert_methodt::variablet()}); auto &var=findit.first->second; if(findit.second) { diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index 7c09b07b2fe..bd2e6a95be4 100644 --- a/src/java_bytecode/java_bytecode_instrument.cpp +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -75,7 +75,7 @@ class java_bytecode_instrumentt:public messaget optionalt instrument_expr(const exprt &expr); }; -const std::vector exception_needed_classes = { // NOLINT +const std::vector exception_needed_classes = { "java.lang.ArithmeticException", "java.lang.ArrayIndexOutOfBoundsException", "java.lang.ClassCastException", diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index a139b75c613..0de42e59ebc 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -157,7 +157,7 @@ bool java_bytecode_languaget::parse( { string_preprocess.initialize_known_type_table(); - auto get_string_base_classes = [this](const irep_idt &id) { // NOLINT (*) + auto get_string_base_classes = [this](const irep_idt &id) { return string_preprocess.get_string_type_base_classes(id); }; diff --git a/src/java_bytecode/remove_exceptions.cpp b/src/java_bytecode/remove_exceptions.cpp index 618c1a8cda1..9b6801128c2 100644 --- a/src/java_bytecode/remove_exceptions.cpp +++ b/src/java_bytecode/remove_exceptions.cpp @@ -572,7 +572,7 @@ void remove_exceptions( std::map> exceptions_map; uncaught_exceptions(goto_functions, ns, exceptions_map); remove_exceptionst::function_may_throwt function_may_throw = - [&exceptions_map](const irep_idt &id) { // NOLINT(whitespace/braces) + [&exceptions_map](const irep_idt &id) { return !exceptions_map[id].empty(); }; remove_exceptionst remove_exceptions( diff --git a/src/java_bytecode/remove_instanceof.cpp b/src/java_bytecode/remove_instanceof.cpp index 37cb8cc3094..cb93fcbbb98 100644 --- a/src/java_bytecode/remove_instanceof.cpp +++ b/src/java_bytecode/remove_instanceof.cpp @@ -90,9 +90,7 @@ std::size_t remove_instanceoft::lower_instanceof( // Sort alphabetically to make order of generated disjuncts // independent of class loading order std::sort( - children.begin(), - children.end(), - [](const irep_idt &a, const irep_idt &b) { // NOLINT + children.begin(), children.end(), [](const irep_idt &a, const irep_idt &b) { return a.compare(b) < 0; }); diff --git a/src/java_bytecode/replace_java_nondet.cpp b/src/java_bytecode/replace_java_nondet.cpp index 264de82328b..6d0e23210c1 100644 --- a/src/java_bytecode/replace_java_nondet.cpp +++ b/src/java_bytecode/replace_java_nondet.cpp @@ -249,9 +249,7 @@ static goto_programt::targett check_and_replace_target( "goto_program missing END_FUNCTION instruction"); std::for_each( - target, - after_matching_assignment, - [](goto_programt::instructiont &instr) { // NOLINT (*) + target, after_matching_assignment, [](goto_programt::instructiont &instr) { instr.make_skip(); }); diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 0a80a382b94..4a371001851 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -493,13 +493,13 @@ int jbmc_parse_optionst::doit() std::function configure_bmc = nullptr; if(options.get_bool_option("java-unwind-enum-static")) { - configure_bmc = []( - bmct &bmc, const symbol_tablet &symbol_table) { // NOLINT (*) - bmc.add_loop_unwind_handler([&symbol_table]( - const irep_idt &function_id, - unsigned loop_number, - unsigned unwind, - unsigned &max_unwind) { // NOLINT (*) + configure_bmc = [](bmct &bmc, const symbol_tablet &symbol_table) { + bmc.add_loop_unwind_handler( + [&symbol_table]( + const irep_idt &function_id, + unsigned loop_number, + unsigned unwind, + unsigned &max_unwind) { return java_enum_static_init_unwind_handler( function_id, loop_number, @@ -564,7 +564,7 @@ int jbmc_parse_optionst::doit() // executes. If --paths is active, these dump routines run after every // paths iteration. Its return value indicates that if we ran any dump // function, then we should skip the actual solver phase. - auto callback_after_symex = [this, &lazy_goto_model]() { // NOLINT (*) + auto callback_after_symex = [this, &lazy_goto_model]() { return show_loaded_functions(lazy_goto_model); }; @@ -729,11 +729,10 @@ void jbmc_parse_optionst::process_goto_function( remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF); } - auto function_is_stub = - [&symbol_table, &model](const irep_idt &id) { // NOLINT(*) - return symbol_table.lookup_ref(id).value.is_nil() && - !model.can_produce_function(id); - }; + auto function_is_stub = [&symbol_table, &model](const irep_idt &id) { + return symbol_table.lookup_ref(id).value.is_nil() && + !model.can_produce_function(id); + }; remove_returns(function, function_is_stub); diff --git a/src/jsil/jsil_types.cpp b/src/jsil/jsil_types.cpp index 12a76787149..ac2ff75c487 100644 --- a/src/jsil/jsil_types.cpp +++ b/src/jsil/jsil_types.cpp @@ -15,54 +15,38 @@ Author: Daiva Naudziuniene, daivan@amazon.com typet jsil_any_type() { - return jsil_union_typet({ // NOLINT(whitespace/braces) - jsil_empty_type(), - jsil_reference_type(), - jsil_value_type() - }); + return jsil_union_typet( + {jsil_empty_type(), jsil_reference_type(), jsil_value_type()}); } typet jsil_value_or_empty_type() { - return jsil_union_typet({ // NOLINT(whitespace/braces) - jsil_value_type(), - jsil_empty_type() - }); + return jsil_union_typet({jsil_value_type(), jsil_empty_type()}); } typet jsil_value_or_reference_type() { - return jsil_union_typet({ // NOLINT(whitespace/braces) - jsil_value_type(), - jsil_reference_type() - }); + return jsil_union_typet({jsil_value_type(), jsil_reference_type()}); } typet jsil_value_type() { - return jsil_union_typet({ // NOLINT(whitespace/braces) - jsil_undefined_type(), - jsil_null_type(), - jsil_prim_type(), - jsil_object_type() - }); + return jsil_union_typet( + {jsil_undefined_type(), + jsil_null_type(), + jsil_prim_type(), + jsil_object_type()}); } typet jsil_prim_type() { - return jsil_union_typet({ // NOLINT(whitespace/braces) - floatbv_typet(), - string_typet(), - bool_typet() - }); + return jsil_union_typet({floatbv_typet(), string_typet(), bool_typet()}); } typet jsil_reference_type() { - return jsil_union_typet({ // NOLINT(whitespace/braces) - jsil_member_reference_type(), - jsil_variable_reference_type() - }); + return jsil_union_typet( + {jsil_member_reference_type(), jsil_variable_reference_type()}); } typet jsil_member_reference_type() @@ -77,10 +61,8 @@ typet jsil_variable_reference_type() typet jsil_object_type() { - return jsil_union_typet({ // NOLINT(whitespace/braces) - jsil_user_object_type(), - jsil_builtin_object_type() - }); + return jsil_union_typet( + {jsil_user_object_type(), jsil_builtin_object_type()}); } typet jsil_user_object_type() diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp index 154e027a5ef..effcef775e6 100644 --- a/src/solvers/refinement/string_constraint_generator_transformation.cpp +++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp @@ -128,7 +128,7 @@ exprt string_constraint_generatort::add_axioms_for_substring( lemmas.push_back(equal_exprt(res.length(), minus_exprt(end1, start1))); // Axiom 2. - constraints.push_back([&] { // NOLINT + constraints.push_back([&] { const symbol_exprt idx = fresh_univ_index("QA_index_substring", index_type); return string_constraintt( idx, res.length(), equal_exprt(res[idx], str[plus_exprt(start1, idx)])); @@ -197,7 +197,7 @@ exprt string_constraint_generatort::add_axioms_for_trim( constraints.push_back(a6); // Axiom 7. - constraints.push_back([&] { // NOLINT + constraints.push_back([&] { const symbol_exprt n2 = fresh_univ_index("QA_index_trim2", index_type); const minus_exprt bound(minus_exprt(str.length(), idx), res.length()); const binary_relation_exprt eqn2( @@ -473,7 +473,7 @@ exprt string_constraint_generatort::add_axioms_for_replace( char_array_of_pointer(f.arguments()[1], f.arguments()[0]); if( const auto maybe_chars = - to_char_pair(f.arguments()[3], f.arguments()[4], [this](const exprt &e) { // NOLINT + to_char_pair(f.arguments()[3], f.arguments()[4], [this](const exprt &e) { return get_string_expr(e); })) { diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index c2685dc6202..e42e1ff776a 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -692,7 +692,7 @@ decision_proceduret::resultt string_refinementt::dec_solve() constraints.begin(), constraints.end(), std::back_inserter(axioms.universal), - [&](string_constraintt constraint) { // NOLINT + [&](string_constraintt constraint) { symbol_resolve.replace_expr(constraint); DATA_INVARIANT( is_valid_string_constraint(error(), ns, constraint), @@ -707,14 +707,14 @@ decision_proceduret::resultt string_refinementt::dec_solve() not_contains_constraints.begin(), not_contains_constraints.end(), std::back_inserter(axioms.not_contains), - [&](string_not_contains_constraintt axiom) { // NOLINT + [&](string_not_contains_constraintt axiom) { symbol_resolve.replace_expr(axiom); return axiom; }); for(const auto &nc_axiom : axioms.not_contains) { - const auto &witness_type = [&] { // NOLINT + const auto &witness_type = [&] { const auto &rtype = to_array_type(nc_axiom.s0().type()); const typet &index_type = rtype.size().type(); return array_typet(index_type, infinity_exprt(index_type)); @@ -1920,7 +1920,7 @@ static void update_index_set( static optionalt find_index(const exprt &expr, const exprt &str, const symbol_exprt &qvar) { - auto index_str_containing_qvar = [&](const exprt &e) { // NOLINT + auto index_str_containing_qvar = [&](const exprt &e) { if(auto index_expr = expr_try_dynamic_cast(e)) { const auto &arr = index_expr->array(); diff --git a/src/util/graph.h b/src/util/graph.h index 45530f09ef6..16af29ea634 100644 --- a/src/util/graph.h +++ b/src/util/graph.h @@ -486,7 +486,7 @@ void get_reachable( { auto n = stack.back(); stack.pop_back(); - for_each_successor(n, [&](const nodet &node) { // NOLINT + for_each_successor(n, [&](const nodet &node) { if(set.insert(node).second) stack.push_back(node); }); @@ -749,8 +749,8 @@ void output_dot_generic( &for_each_succ, const std::function node_to_string) { - for_each_node([&](const node_index_type &i) { // NOLINT - for_each_succ(i, [&](const node_index_type &n) { // NOLINT + for_each_node([&](const node_index_type &i) { + for_each_succ(i, [&](const node_index_type &n) { out << node_to_string(i) << " -> " << node_to_string(n) << '\n'; }); }); @@ -784,14 +784,13 @@ template void grapht::output_dot(std::ostream &out) const { const auto for_each_node = - [&](const std::function &f) { // NOLINT + [&](const std::function &f) { for(node_indext i = 0; i < nodes.size(); ++i) f(i); }; const auto for_each_succ = [&]( - const node_indext &i, - const std::function &f) { // NOLINT + const node_indext &i, const std::function &f) { for_each_successor(i, f); }; diff --git a/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp b/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp index 1341c158176..16fb06aec81 100644 --- a/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp +++ b/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp @@ -19,13 +19,10 @@ /// \return true if a suitable symbol_exprt is found static bool contains_symbol_reference(const exprt &expr, const irep_idt &id) { - return - std::any_of( - expr.depth_begin(), - expr.depth_end(), - [id](const exprt &e) { // NOLINT (*) - return e.id() == ID_symbol && to_symbol_expr(e).get_identifier() == id; - }); + return std::any_of( + expr.depth_begin(), expr.depth_end(), [id](const exprt &e) { + return e.id() == ID_symbol && to_symbol_expr(e).get_identifier() == id; + }); } SCENARIO( diff --git a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp index 3556cc26915..aaf797f7388 100644 --- a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp +++ b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp @@ -206,7 +206,7 @@ SCENARIO("instantiate_not_contains", constraints.begin(), constraints.end(), axioms, - [&](const std::string &accu, string_constraintt sc) { // NOLINT + [&](const std::string &accu, string_constraintt sc) { simplify(sc, ns); std::string s; java_lang->from_expr(sc, s, ns); @@ -218,8 +218,7 @@ SCENARIO("instantiate_not_contains", nc_contraints.begin(), nc_contraints.end(), axioms, - [&]( - const std::string &accu, string_not_contains_constraintt sc) { // NOLINT + [&](const std::string &accu, string_not_contains_constraintt sc) { simplify(sc, ns); generator.witness[sc] = generator.fresh_symbol("w", t.witness_type()); nc_axioms.push_back(sc); @@ -233,7 +232,7 @@ SCENARIO("instantiate_not_contains", lemmas.begin(), lemmas.end(), axioms, - [&](const std::string &accu, exprt axiom) { // NOLINT + [&](const std::string &accu, exprt axiom) { simplify(axiom, ns); std::string s; java_lang->from_expr(axiom, s, ns); diff --git a/unit/solvers/refinement/string_refinement/dependency_graph.cpp b/unit/solvers/refinement/string_refinement/dependency_graph.cpp index 3a0b6e16b62..de6bd2d69e6 100644 --- a/unit/solvers/refinement/string_refinement/dependency_graph.cpp +++ b/unit/solvers/refinement/string_refinement/dependency_graph.cpp @@ -142,8 +142,7 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]") const auto &node = dependencies.get_node(char_array3); std::size_t nb_dependencies = 0; dependencies.for_each_dependency( - node, - [&](const string_dependenciest::builtin_function_nodet &n) { // NOLINT + node, [&](const string_dependenciest::builtin_function_nodet &n) { nb_dependencies++; THEN("primitive0 depends on string1 and string2") { @@ -161,8 +160,7 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]") const auto &node = dependencies.get_node(char_array5); std::size_t nb_dependencies = 0; dependencies.for_each_dependency( - node, - [&](const string_dependenciest::builtin_function_nodet &n) { // NOLINT + node, [&](const string_dependenciest::builtin_function_nodet &n) { nb_dependencies++; THEN("primitive1 depends on string3 and string4") {