diff --git a/jbmc/src/jbmc/Makefile b/jbmc/src/jbmc/Makefile index 57eb5ad31e7..0e85a394f16 100644 --- a/jbmc/src/jbmc/Makefile +++ b/jbmc/src/jbmc/Makefile @@ -43,8 +43,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \ ../$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \ ../$(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \ ../$(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \ - ../$(CPROVER_DIR)/src/cbmc/symex_bmc$(OBJEXT) \ - ../$(CPROVER_DIR)/src/cbmc/symex_coverage$(OBJEXT) \ # Empty last line INCLUDES= -I .. -I ../$(CPROVER_DIR)/src diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index d1e009b831c..531a3cb8fe7 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -89,8 +89,6 @@ BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/cbmc_parse_options$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \ - $(CPROVER_DIR)/src/cbmc/symex_bmc$(OBJEXT) \ - $(CPROVER_DIR)/src/cbmc/symex_coverage$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/xml_interface$(OBJEXT) \ $(CPROVER_DIR)/src/jsil/expr2jsil$(OBJEXT) \ $(CPROVER_DIR)/src/jsil/jsil_convert$(OBJEXT) \ diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index 4dec22ee526..4ce2be97bab 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -6,8 +6,6 @@ SRC = all_properties.cpp \ cbmc_parse_options.cpp \ counterexample_beautification.cpp \ fault_localization.cpp \ - symex_bmc.cpp \ - symex_coverage.cpp \ xml_interface.cpp \ # Empty last line diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 1f230a34ed5..063d2fc6078 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -20,6 +20,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include #include @@ -29,7 +31,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "symex_bmc.h" class cbmc_solverst; diff --git a/src/goto-checker/Makefile b/src/goto-checker/Makefile index b6d2d98a003..7f37d465d4c 100644 --- a/src/goto-checker/Makefile +++ b/src/goto-checker/Makefile @@ -1,5 +1,7 @@ SRC = bmc_util.cpp \ solver_factory.cpp \ + symex_coverage.cpp \ + symex_bmc.cpp \ # Empty last line INCLUDES= -I .. diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index 5a617d2b56b..b947e092a32 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -14,8 +14,6 @@ Author: Daniel Kroening, Peter Schrammel #include #include -#include - #include #include #include @@ -33,6 +31,8 @@ Author: Daniel Kroening, Peter Schrammel #include #include +#include "symex_bmc.h" + void build_error_trace( goto_tracet &goto_trace, const namespacet &ns, diff --git a/src/cbmc/symex_bmc.cpp b/src/goto-checker/symex_bmc.cpp similarity index 74% rename from src/cbmc/symex_bmc.cpp rename to src/goto-checker/symex_bmc.cpp index e0aeaabd3f8..e905aa0bf2e 100644 --- a/src/cbmc/symex_bmc.cpp +++ b/src/goto-checker/symex_bmc.cpp @@ -15,8 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include +#include symex_bmct::symex_bmct( message_handlert &mh, @@ -35,28 +35,28 @@ void symex_bmct::symex_step( const get_goto_functiont &get_goto_function, statet &state) { - const source_locationt &source_location=state.source.pc->source_location; + const source_locationt &source_location = state.source.pc->source_location; - if(!source_location.is_nil() && last_source_location!=source_location) + if(!source_location.is_nil() && last_source_location != source_location) { - log.debug() << "BMC at " << source_location.as_string() - << " (depth " << state.depth << ')' << log.eom; + log.debug() << "BMC at " << source_location.as_string() << " (depth " + << state.depth << ')' << log.eom; - last_source_location=source_location; + last_source_location = source_location; } - const goto_programt::const_targett cur_pc=state.source.pc; - const guardt cur_guard=state.guard; + const goto_programt::const_targett cur_pc = state.source.pc; + const guardt cur_guard = state.guard; - if(!state.guard.is_false() && - state.source.pc->is_assume() && - simplify_expr(state.source.pc->guard, ns).is_false()) + if( + !state.guard.is_false() && state.source.pc->is_assume() && + simplify_expr(state.source.pc->guard, ns).is_false()) { log.statistics() << "aborting path on assume(false) at " << state.source.pc->source_location << " thread " << state.source.thread_nr; - const irep_idt &c=state.source.pc->source_location.get_comment(); + const irep_idt &c = state.source.pc->source_location.get_comment(); if(!c.empty()) log.statistics() << ": " << c; @@ -77,9 +77,9 @@ void symex_bmct::symex_step( // taken an impossible transition); thus we synthesize a // transition from the goto instruction to its target to make // sure the goto is considered covered - if(cur_pc->is_goto() && - cur_pc->get_target()!=state.source.pc && - cur_pc->guard.is_true()) + if( + cur_pc->is_goto() && cur_pc->get_target() != state.source.pc && + cur_pc->guard.is_true()) symex_coverage.covered(cur_pc, cur_pc->get_target()); else if(!state.guard.is_false()) symex_coverage.covered(cur_pc, state.source.pc); @@ -90,18 +90,18 @@ void symex_bmct::merge_goto( const statet::goto_statet &goto_state, statet &state) { - const goto_programt::const_targett prev_pc=goto_state.source.pc; - const guardt prev_guard=goto_state.guard; + const goto_programt::const_targett prev_pc = goto_state.source.pc; + const guardt prev_guard = goto_state.guard; goto_symext::merge_goto(goto_state, state); PRECONDITION(prev_pc->is_goto()); - if(record_coverage && - // could the branch possibly be taken? - !prev_guard.is_false() && - !state.guard.is_false() && - // branches only, no single-successor goto - !prev_pc->guard.is_true()) + if( + record_coverage && + // could the branch possibly be taken? + !prev_guard.is_false() && !state.guard.is_false() && + // branches only, no single-successor goto + !prev_pc->guard.is_true()) symex_coverage.covered(prev_pc, state.source.pc); } @@ -110,10 +110,10 @@ bool symex_bmct::should_stop_unwind( const goto_symex_statet::call_stackt &context, unsigned unwind) { - const irep_idt id=goto_programt::loop_id(*source.pc); + const irep_idt id = goto_programt::loop_id(*source.pc); tvt abort_unwind_decision; - unsigned this_loop_limit=std::numeric_limits::max(); + unsigned this_loop_limit = std::numeric_limits::max(); for(auto handler : loop_unwind_handlers) { @@ -127,7 +127,7 @@ bool symex_bmct::should_stop_unwind( // / --unwind options to decide: if(abort_unwind_decision.is_unknown()) { - auto limit=unwindset.get_limit(id, source.thread_nr); + auto limit = unwindset.get_limit(id, source.thread_nr); if(!limit.has_value()) abort_unwind_decision = tvt(false); @@ -142,7 +142,7 @@ bool symex_bmct::should_stop_unwind( log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " loop " << id << " iteration " << unwind; - if(this_loop_limit!=std::numeric_limits::max()) + if(this_loop_limit != std::numeric_limits::max()) log.statistics() << " (" << this_loop_limit << " max)"; log.statistics() << " " << source.pc->source_location << " thread " @@ -157,7 +157,7 @@ bool symex_bmct::get_unwind_recursion( unsigned unwind) { tvt abort_unwind_decision; - unsigned this_loop_limit=std::numeric_limits::max(); + unsigned this_loop_limit = std::numeric_limits::max(); for(auto handler : recursion_unwind_handlers) { @@ -170,7 +170,7 @@ bool symex_bmct::get_unwind_recursion( // / --unwind options to decide: if(abort_unwind_decision.is_unknown()) { - auto limit=unwindset.get_limit(id, thread_nr); + auto limit = unwindset.get_limit(id, thread_nr); if(!limit.has_value()) abort_unwind_decision = tvt(false); @@ -182,14 +182,14 @@ bool symex_bmct::get_unwind_recursion( abort_unwind_decision.is_known(), "unwind decision should be taken by now"); bool abort = abort_unwind_decision.is_true(); - if(unwind>0 || abort) + if(unwind > 0 || abort) { - const symbolt &symbol=ns.lookup(id); + const symbolt &symbol = ns.lookup(id); log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " recursion " << symbol.display_name() << " iteration " << unwind; - if(this_loop_limit!=std::numeric_limits::max()) + if(this_loop_limit != std::numeric_limits::max()) log.statistics() << " (" << this_loop_limit << " max)"; log.statistics() << log.eom; diff --git a/src/cbmc/symex_bmc.h b/src/goto-checker/symex_bmc.h similarity index 93% rename from src/cbmc/symex_bmc.h rename to src/goto-checker/symex_bmc.h index 97e8c7aeade..8f56e5193d0 100644 --- a/src/cbmc/symex_bmc.h +++ b/src/goto-checker/symex_bmc.h @@ -9,20 +9,20 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Bounded Model Checking for ANSI-C -#ifndef CPROVER_CBMC_SYMEX_BMC_H -#define CPROVER_CBMC_SYMEX_BMC_H +#ifndef CPROVER_GOTO_CHECKER_SYMEX_BMC_H +#define CPROVER_GOTO_CHECKER_SYMEX_BMC_H #include #include -#include #include +#include #include #include "symex_coverage.h" -class symex_bmct: public goto_symext +class symex_bmct : public goto_symext { public: symex_bmct( @@ -41,9 +41,8 @@ class symex_bmct: public goto_symext /// information for the user (e.g. "unwinding iteration N, max M"), and is not /// enforced. They return true to halt unwinding, false to authorise /// unwinding, or Unknown to indicate they have no opinion. - typedef - std::function + typedef std::function< + tvt(const goto_symex_statet::call_stackt &, unsigned, unsigned, unsigned &)> loop_unwind_handlert; /// Recursion unwind handlers take the function ID, the unwind count so far, @@ -115,4 +114,4 @@ class symex_bmct: public goto_symext symex_coveraget symex_coverage; }; -#endif // CPROVER_CBMC_SYMEX_BMC_H +#endif // CPROVER_GOTO_CHECKER_SYMEX_BMC_H diff --git a/src/cbmc/symex_coverage.cpp b/src/goto-checker/symex_coverage.cpp similarity index 61% rename from src/cbmc/symex_coverage.cpp rename to src/goto-checker/symex_coverage.cpp index f5e2c0aec3b..e6f632b743f 100644 --- a/src/cbmc/symex_coverage.cpp +++ b/src/goto-checker/symex_coverage.cpp @@ -31,12 +31,12 @@ Date: March 2016 class coverage_recordt { public: - explicit coverage_recordt(const std::string &node_id): - xml(node_id), - lines_covered(0), - lines_total(0), - branches_covered(0), - branches_total(0) + explicit coverage_recordt(const std::string &node_id) + : xml(node_id), + lines_covered(0), + lines_total(0), + branches_covered(0), + branches_total(0) { } @@ -47,7 +47,7 @@ class coverage_recordt std::size_t branches_total; }; -class goto_program_coverage_recordt:public coverage_recordt +class goto_program_coverage_recordt : public coverage_recordt { public: goto_program_coverage_recordt( @@ -65,8 +65,7 @@ class goto_program_coverage_recordt:public coverage_recordt struct coverage_conditiont { - coverage_conditiont(): - false_taken(false), true_taken(false) + coverage_conditiont() : false_taken(false), true_taken(false) { } @@ -76,42 +75,38 @@ class goto_program_coverage_recordt:public coverage_recordt struct coverage_linet { - coverage_linet(): - hits(0) + coverage_linet() : hits(0) { } unsigned hits; - std::map - conditions; + std::map conditions; }; - typedef std::map - coverage_lines_mapt; + typedef std::map coverage_lines_mapt; void compute_coverage_lines( const goto_programt &goto_program, + const irep_idt &file_name, const symex_coveraget::coveraget &coverage, coverage_lines_mapt &dest); }; -static std::string rate( - std::size_t covered, - std::size_t total, - bool per_cent=false) +static std::string +rate(std::size_t covered, std::size_t total, bool per_cent = false) { std::ostringstream oss; #if 1 float fraction; - if(total==0) - fraction=1.0; + if(total == 0) + fraction = 1.0; else - fraction=static_cast(covered)/static_cast(total); + fraction = static_cast(covered) / static_cast(total); if(per_cent) - oss << fraction*100.0 << '%'; + oss << fraction * 100.0 << '%'; else oss << fraction; #else @@ -121,41 +116,37 @@ static std::string rate( return oss.str(); } -static std::string rate_detailed( - std::size_t covered, - std::size_t total, - bool per_cent=false) +static std::string +rate_detailed(std::size_t covered, std::size_t total, bool per_cent = false) { std::ostringstream oss; - oss << rate(covered, total, per_cent) - << " (" << covered << '/' << total << ')'; + oss << rate(covered, total, per_cent) << " (" << covered << '/' << total + << ')'; return oss.str(); } goto_program_coverage_recordt::goto_program_coverage_recordt( const namespacet &ns, goto_functionst::function_mapt::const_iterator gf_it, - const symex_coveraget::coveraget &coverage): - coverage_recordt("method") + const symex_coveraget::coveraget &coverage) + : coverage_recordt("method") { PRECONDITION(gf_it->second.body_available()); // identify the file name, inlined functions aren't properly // accounted for - goto_programt::const_targett end_function= + goto_programt::const_targett end_function = --gf_it->second.body.instructions.end(); DATA_INVARIANT( end_function->is_end_function(), "last instruction in a function body is end function"); - file_name=end_function->source_location.get_file(); + file_name = end_function->source_location.get_file(); DATA_INVARIANT(!file_name.empty(), "should have a valid source location"); // compute the maximum coverage of individual source-code lines coverage_lines_mapt coverage_lines_map; compute_coverage_lines( - gf_it->second.body, - coverage, - coverage_lines_map); + gf_it->second.body, file_name, coverage, coverage_lines_map); // // @@ -171,21 +162,18 @@ goto_program_coverage_recordt::goto_program_coverage_recordt( // xml.set_attribute("name", id2string(gf_it->first)); - code_typet sig_type= + code_typet sig_type = original_return_type(ns.get_symbol_table(), gf_it->first); - xml.set_attribute("signature", - from_type(ns, gf_it->first, sig_type)); + xml.set_attribute("signature", from_type(ns, gf_it->first, sig_type)); - xml.set_attribute("line-rate", - rate_detailed(lines_covered, lines_total)); - xml.set_attribute("branch-rate", - rate(branches_covered, branches_total)); + xml.set_attribute("line-rate", rate_detailed(lines_covered, lines_total)); + xml.set_attribute("branch-rate", rate(branches_covered, branches_total)); - xmlt &lines=xml.new_element("lines"); + xmlt &lines = xml.new_element("lines"); for(const auto &cov_line : coverage_lines_map) { - xmlt &line=lines.new_element("line"); + xmlt &line = lines.new_element("line"); line.set_attribute("number", std::to_string(cov_line.first)); line.set_attribute("hits", std::to_string(cov_line.second.hits)); @@ -195,45 +183,45 @@ goto_program_coverage_recordt::goto_program_coverage_recordt( { line.set_attribute("branch", "true"); - xmlt &conditions=line.new_element("conditions"); + xmlt &conditions = line.new_element("conditions"); - std::size_t number=0, total_taken=0; + std::size_t number = 0, total_taken = 0; for(const auto &c : cov_line.second.conditions) { // - xmlt &condition=conditions.new_element("condition"); + xmlt &condition = conditions.new_element("condition"); condition.set_attribute("number", std::to_string(number++)); condition.set_attribute("type", "jump"); - unsigned taken=c.second.false_taken+c.second.true_taken; - total_taken+=taken; + unsigned taken = c.second.false_taken + c.second.true_taken; + total_taken += taken; condition.set_attribute("coverage", rate(taken, 2, true)); } line.set_attribute( - "condition-coverage", - rate_detailed(total_taken, number*2, true)); + "condition-coverage", rate_detailed(total_taken, number * 2, true)); } } } void goto_program_coverage_recordt::compute_coverage_lines( - const goto_programt &goto_program, - const symex_coveraget::coveraget &coverage, - coverage_lines_mapt &dest) + const goto_programt &goto_program, + const irep_idt &file_name, + const symex_coveraget::coveraget &coverage, + coverage_lines_mapt &dest) { forall_goto_program_instructions(it, goto_program) { - if(it->source_location.is_nil() || - it->source_location.get_file()!=file_name || - it->is_dead() || - it->is_end_function()) + if( + it->source_location.is_nil() || + it->source_location.get_file() != file_name || it->is_dead() || + it->is_end_function()) continue; - const bool is_branch=it->is_goto() && !it->guard.is_constant(); + const bool is_branch = it->is_goto() && !it->guard.is_constant(); - unsigned l= + unsigned l = safe_string2unsigned(id2string(it->source_location.get_line())); - std::pair entry= + std::pair entry = dest.insert(std::make_pair(l, coverage_linet())); if(entry.second) @@ -243,17 +231,16 @@ void goto_program_coverage_recordt::compute_coverage_lines( // a branching instruction if(is_branch) { - branches_total+=2; - if(!entry.first->second.conditions.insert( - {it, coverage_conditiont()}).second) + branches_total += 2; + if(!entry.first->second.conditions.insert({it, coverage_conditiont()}) + .second) UNREACHABLE; } - symex_coveraget::coveraget::const_iterator c_entry= - coverage.find(it); - if(c_entry!=coverage.end()) + symex_coveraget::coveraget::const_iterator c_entry = coverage.find(it); + if(c_entry != coverage.end()) { - if(!(c_entry->second.size()==1 || is_branch)) + if(!(c_entry->second.size() == 1 || is_branch)) { std::cerr << it->location_number << '\n'; for(const auto &cov : c_entry->second) @@ -269,24 +256,24 @@ void goto_program_coverage_recordt::compute_coverage_lines( cov.second.num_executions > 0, "coverage entries can only exist with at least one execution"); - if(entry.first->second.hits==0) + if(entry.first->second.hits == 0) ++lines_covered; - if(cov.second.num_executions>entry.first->second.hits) - entry.first->second.hits=cov.second.num_executions; + if(cov.second.num_executions > entry.first->second.hits) + entry.first->second.hits = cov.second.num_executions; if(is_branch) { - auto cond_entry=entry.first->second.conditions.find(it); + auto cond_entry = entry.first->second.conditions.find(it); INVARIANT( cond_entry != entry.first->second.conditions.end(), "branch should have condition"); - if(it->get_target()==cov.second.succ) + if(it->get_target() == cov.second.succ) { if(!cond_entry->second.false_taken) { - cond_entry->second.false_taken=true; + cond_entry->second.false_taken = true; ++branches_covered; } } @@ -294,7 +281,7 @@ void goto_program_coverage_recordt::compute_coverage_lines( { if(!cond_entry->second.true_taken) { - cond_entry->second.true_taken=true; + cond_entry->second.true_taken = true; ++branches_covered; } } @@ -313,17 +300,17 @@ void symex_coveraget::compute_overall_coverage( forall_goto_functions(gf_it, goto_functions) { - if(!gf_it->second.body_available() || - gf_it->first==goto_functions.entry_point() || - gf_it->first == INITIALIZE_FUNCTION) + if( + !gf_it->second.body_available() || + gf_it->first == goto_functions.entry_point() || + gf_it->first == INITIALIZE_FUNCTION) continue; goto_program_coverage_recordt func_cov(ns, gf_it, coverage); - std::pair entry= - file_records.insert(std::make_pair(func_cov.get_file(), - coverage_recordt("class"))); - coverage_recordt &file_record=entry.first->second; + std::pair entry = file_records.insert( + std::make_pair(func_cov.get_file(), coverage_recordt("class"))); + coverage_recordt &file_record = entry.first->second; if(entry.second) { @@ -335,48 +322,46 @@ void symex_coveraget::compute_overall_coverage( file_record.xml.elements.front().new_element(func_cov.xml); // copy any lines - for(xmlt::elementst::const_iterator - it=func_cov.xml.elements.front().elements.begin(); - it!=func_cov.xml.elements.front().elements.end(); + for(xmlt::elementst::const_iterator it = + func_cov.xml.elements.front().elements.begin(); + it != func_cov.xml.elements.front().elements.end(); ++it) file_record.xml.elements.back().new_element(*it); // merge line/branch info - file_record.lines_covered+=func_cov.lines_covered; - file_record.lines_total+=func_cov.lines_total; - file_record.branches_covered+=func_cov.branches_covered; - file_record.branches_total+=func_cov.branches_total; + file_record.lines_covered += func_cov.lines_covered; + file_record.lines_total += func_cov.lines_total; + file_record.branches_covered += func_cov.branches_covered; + file_record.branches_total += func_cov.branches_total; } - xmlt &classes=dest.xml.new_element("classes"); + xmlt &classes = dest.xml.new_element("classes"); // - for(file_recordst::const_iterator it=file_records.begin(); - it!=file_records.end(); + for(file_recordst::const_iterator it = file_records.begin(); + it != file_records.end(); ++it) { if(source_locationt::is_built_in(id2string(it->first))) continue; - const coverage_recordt &f_cov=it->second; + const coverage_recordt &f_cov = it->second; - xmlt &class_xml=classes.new_element(f_cov.xml); + xmlt &class_xml = classes.new_element(f_cov.xml); class_xml.set_attribute("name", id2string(it->first)); class_xml.set_attribute("filename", id2string(it->first)); - class_xml.set_attribute("line-rate", - rate(f_cov.lines_covered, - f_cov.lines_total)); - class_xml.set_attribute("branch-rate", - rate(f_cov.branches_covered, - f_cov.branches_total)); + class_xml.set_attribute( + "line-rate", rate(f_cov.lines_covered, f_cov.lines_total)); + class_xml.set_attribute( + "branch-rate", rate(f_cov.branches_covered, f_cov.branches_total)); class_xml.set_attribute("complexity", "0.0"); // merge line/branch info - dest.lines_covered+=f_cov.lines_covered; - dest.lines_total+=f_cov.lines_total; - dest.branches_covered+=f_cov.branches_covered; - dest.branches_total+=f_cov.branches_total; + dest.lines_covered += f_cov.lines_covered; + dest.lines_total += f_cov.lines_total; + dest.branches_covered += f_cov.branches_covered; + dest.branches_total += f_cov.branches_total; } } @@ -387,9 +372,9 @@ void symex_coveraget::build_cobertura( coverage_recordt overall_cov("package"); compute_overall_coverage(goto_functions, overall_cov); - std::string overall_line_rate_str= + std::string overall_line_rate_str = rate(overall_cov.lines_covered, overall_cov.lines_total); - std::string overall_branch_rate_str= + std::string overall_branch_rate_str = rate(overall_cov.branches_covered, overall_cov.branches_total); auto now = std::chrono::system_clock::now(); @@ -402,23 +387,22 @@ void symex_coveraget::build_cobertura( // version="2.1.1" timestamp="0"> xml_coverage.set_attribute("line-rate", overall_line_rate_str); xml_coverage.set_attribute("branch-rate", overall_branch_rate_str); - xml_coverage.set_attribute("lines-covered", - std::to_string(overall_cov.lines_covered)); - xml_coverage.set_attribute("lines-valid", - std::to_string(overall_cov.lines_total)); - xml_coverage.set_attribute("branches-covered", - std::to_string(overall_cov.branches_covered)); - xml_coverage.set_attribute("branches-valid", - std::to_string(overall_cov.branches_total)); + xml_coverage.set_attribute( + "lines-covered", std::to_string(overall_cov.lines_covered)); + xml_coverage.set_attribute( + "lines-valid", std::to_string(overall_cov.lines_total)); + xml_coverage.set_attribute( + "branches-covered", std::to_string(overall_cov.branches_covered)); + xml_coverage.set_attribute( + "branches-valid", std::to_string(overall_cov.branches_total)); xml_coverage.set_attribute("complexity", "0.0"); xml_coverage.set_attribute("version", "2.1.1"); - xml_coverage.set_attribute("timestamp", - std::to_string(tt)); + xml_coverage.set_attribute("timestamp", std::to_string(tt)); - xmlt &packages=xml_coverage.new_element("packages"); + xmlt &packages = xml_coverage.new_element("packages"); // - xmlt &package=packages.new_element(overall_cov.xml); + xmlt &package = packages.new_element(overall_cov.xml); package.set_attribute("name", ""); package.set_attribute("line-rate", overall_line_rate_str); package.set_attribute("branch-rate", overall_branch_rate_str); @@ -446,7 +430,7 @@ bool symex_coveraget::generate_report( { PRECONDITION(!path.empty()); - if(path=="-") + if(path == "-") return output_report(goto_functions, std::cout); else { @@ -454,4 +438,3 @@ bool symex_coveraget::generate_report( return output_report(goto_functions, out); } } - diff --git a/src/cbmc/symex_coverage.h b/src/goto-checker/symex_coverage.h similarity index 79% rename from src/cbmc/symex_coverage.h rename to src/goto-checker/symex_coverage.h index 6eac2cf4ef7..1ad851c172d 100644 --- a/src/cbmc/symex_coverage.h +++ b/src/goto-checker/symex_coverage.h @@ -28,15 +28,14 @@ class xmlt; class symex_coveraget { public: - explicit symex_coveraget(const namespacet &_ns):ns(_ns) + explicit symex_coveraget(const namespacet &_ns) : ns(_ns) { } - void covered( - goto_programt::const_targett from, - goto_programt::const_targett to) + void + covered(goto_programt::const_targett from, goto_programt::const_targett to) { - std::pair entry= + std::pair entry = coverage[from].insert({to, coverage_infot(from, to, 1)}); if(!entry.second) @@ -55,9 +54,8 @@ class symex_coveraget coverage_infot( goto_programt::const_targett _from, goto_programt::const_targett _to, - unsigned _num_executions): - location(_from), num_executions(_num_executions), - succ(_to) + unsigned _num_executions) + : location(_from), num_executions(_num_executions), succ(_to) { } @@ -68,13 +66,11 @@ class symex_coveraget typedef std::map coverage_innert; - typedef std::map - coveraget; + typedef std::map coveraget; coveraget coverage; - bool output_report( - const goto_functionst &goto_functions, - std::ostream &os) const; + bool + output_report(const goto_functionst &goto_functions, std::ostream &os) const; void build_cobertura( const goto_functionst &goto_functions, diff --git a/unit/Makefile b/unit/Makefile index 488597b4a3d..739e2dc4210 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -93,8 +93,6 @@ BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \ ../src/cbmc/cbmc_parse_options$(OBJEXT) \ ../src/cbmc/counterexample_beautification$(OBJEXT) \ ../src/cbmc/fault_localization$(OBJEXT) \ - ../src/cbmc/symex_bmc$(OBJEXT) \ - ../src/cbmc/symex_coverage$(OBJEXT) \ ../src/cbmc/xml_interface$(OBJEXT) \ ../src/goto-instrument/cover$(OBJEXT) \ ../src/goto-instrument/cover_basic_blocks$(OBJEXT) \