From baa57412a7e7a0dbc40c2ad26d31e9dcf5110d6a Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Fri, 10 Feb 2017 12:51:25 +0000 Subject: [PATCH 1/7] Use ai function output in goto-instrument. --- .../goto_instrument_parse_options.cpp | 23 ++----------------- 1 file changed, 2 insertions(+), 21 deletions(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 9c30bae5612..0ee4c125bb5 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -506,16 +506,7 @@ int goto_instrument_parse_optionst::doit() reaching_definitions_analysist rd_analysis(ns); rd_analysis(goto_functions, ns); - forall_goto_functions(f_it, goto_functions) - { - if(f_it->second.body_available()) - { - std::cout << "////\n"; - std::cout << "//// Function: " << f_it->first << '\n'; - std::cout << "////\n\n"; - rd_analysis.output(ns, f_it->second.body, std::cout); - } - } + rd_analysis.output(ns, goto_functions, std::cout); return 0; } @@ -528,17 +519,7 @@ int goto_instrument_parse_optionst::doit() dependence_grapht dependence_graph(ns); dependence_graph(goto_functions, ns); - forall_goto_functions(f_it, goto_functions) - { - if(f_it->second.body_available()) - { - std::cout << "////\n"; - std::cout << "//// Function: " << f_it->first << '\n'; - std::cout << "////\n\n"; - dependence_graph.output(ns, f_it->second.body, std::cout); - } - } - + dependence_graph.output(ns, goto_functions, std::cout); dependence_graph.output_dot(std::cout); return 0; From 026f2de21c8658ed0d5b52ecac760aa48df98bdb Mon Sep 17 00:00:00 2001 From: martin Date: Mon, 22 May 2017 20:18:48 +0100 Subject: [PATCH 2/7] Add output_json to the dependence_graph abstract domain. --- src/analyses/dependence_graph.cpp | 43 +++++++++++++++++++++++++++++++ src/analyses/dependence_graph.h | 4 +++ 2 files changed, 47 insertions(+) diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index 9c8d70a884f..c24cf04ab8c 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -11,6 +11,9 @@ Date: August 2013 #include +#include +#include + #include "goto_rw.h" #include "dependence_graph.h" @@ -347,6 +350,46 @@ void dep_graph_domaint::output( /*******************************************************************\ +Function: dep_graph_domaint::output_json + + Inputs: The abstract interpreter and the namespace. + + Outputs: The domain, formatted as a JSON object. + + Purpose: Outputs the current value of the domain. + +\*******************************************************************/ + +jsont dep_graph_domaint::output_json( + const ai_baset &ai, + const namespacet &ns) const +{ + json_arrayt graph; + + for(const auto &cd : control_deps) + { + json_objectt &link=graph.push_back().make_object(); + link["locationNumber"]= + json_numbert(std::to_string(cd->location_number)); + link["sourceLocation"]=json(cd->source_location); + link["type"]=json_stringt("control"); + } + + for(const auto &dd : data_deps) + { + json_objectt &link=graph.push_back().make_object(); + link["locationNumber"]= + json_numbert(std::to_string(dd->location_number)); + link["sourceLocation"]=json(dd->source_location); + json_stringt(dd->source_location.as_string()); + link["type"]=json_stringt("data"); + } + + return graph; +} + +/*******************************************************************\ + Function: dependence_grapht::add_dep Inputs: diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h index fae7c7adbd4..8c94c1dde4c 100644 --- a/src/analyses/dependence_graph.h +++ b/src/analyses/dependence_graph.h @@ -87,6 +87,10 @@ class dep_graph_domaint:public ai_domain_baset const ai_baset &ai, const namespacet &ns) const final; + jsont output_json( + const ai_baset &ai, + const namespacet &ns) const override; + void make_top() final { assert(node_id!=std::numeric_limits::max()); From 4b6e59e934d33259da2f87c95c28b435fd8592dc Mon Sep 17 00:00:00 2001 From: martin Date: Mon, 22 May 2017 20:25:06 +0100 Subject: [PATCH 3/7] Improve annotation of dependence graph declarations. --- src/analyses/dependence_graph.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h index 8c94c1dde4c..1294a40295e 100644 --- a/src/analyses/dependence_graph.h +++ b/src/analyses/dependence_graph.h @@ -91,7 +91,7 @@ class dep_graph_domaint:public ai_domain_baset const ai_baset &ai, const namespacet &ns) const override; - void make_top() final + void make_top() final override { assert(node_id!=std::numeric_limits::max()); From ffd6e552a5fc02bc4ab916425ed617f4e5fa2161 Mon Sep 17 00:00:00 2001 From: martin Date: Mon, 22 May 2017 20:20:54 +0100 Subject: [PATCH 4/7] Add utility function for remove_unreachable. --- src/goto-programs/remove_unreachable.cpp | 6 ++++++ src/goto-programs/remove_unreachable.h | 1 + 2 files changed, 7 insertions(+) diff --git a/src/goto-programs/remove_unreachable.cpp b/src/goto-programs/remove_unreachable.cpp index 14f92e97be1..ac6df4261a8 100644 --- a/src/goto-programs/remove_unreachable.cpp +++ b/src/goto-programs/remove_unreachable.cpp @@ -55,3 +55,9 @@ void remove_unreachable(goto_programt &goto_program) it->make_skip(); } } + +void remove_unreachable(goto_functionst &goto_functions) +{ + Forall_goto_functions(f_it, goto_functions) + remove_unreachable(f_it->second.body); +} diff --git a/src/goto-programs/remove_unreachable.h b/src/goto-programs/remove_unreachable.h index 694cd8c0af8..4fd423641f1 100644 --- a/src/goto-programs/remove_unreachable.h +++ b/src/goto-programs/remove_unreachable.h @@ -12,5 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_functions.h" void remove_unreachable(goto_programt &goto_program); +void remove_unreachable(goto_functionst &goto_functions); #endif // CPROVER_GOTO_PROGRAMS_REMOVE_UNREACHABLE_H From ff65162072008afe5cdbaa9cb40e6fbf9fada9ae Mon Sep 17 00:00:00 2001 From: martin Date: Tue, 23 May 2017 00:01:04 +0100 Subject: [PATCH 5/7] Fix formatting of comments in interval domain. --- src/analyses/interval_domain.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index 1faf8c52364..7ac597bb6ca 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -157,8 +157,8 @@ bool interval_domaint::merge( for(int_mapt::iterator it=int_map.begin(); it!=int_map.end(); ) // no it++ { - //search for the variable that needs to be merged - //containers have different size and variable order + // search for the variable that needs to be merged + // containers have different size and variable order const int_mapt::const_iterator b_it=b.int_map.find(it->first); if(b_it==b.int_map.end()) { From 3b0266de1575f993d85b1a52955676cb09bed02a Mon Sep 17 00:00:00 2001 From: martin Date: Mon, 22 May 2017 23:59:59 +0100 Subject: [PATCH 6/7] White space fix up in test case. --- .../constant_propagation_10/constant_propagation_10.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c b/regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c index 169f7965b9d..f0dea39a424 100644 --- a/regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c +++ b/regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c @@ -4,7 +4,7 @@ int main() signed int i; signed int j; i = 0; - if(!(i >= 2)) + if(!(i >= 2)) { j = j + 1; i = i + 1; From 784f2edc9c44724be9ecf36699450a14e1e70ffb Mon Sep 17 00:00:00 2001 From: martin Date: Tue, 23 May 2017 10:38:32 +0100 Subject: [PATCH 7/7] Add make clean to clear the regression test results. --- regression/Makefile | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/regression/Makefile b/regression/Makefile index 296f583cc5e..71e3494e073 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -12,3 +12,10 @@ DIRS = ansi-c \ test: $(foreach var,$(DIRS), $(MAKE) -C $(var) test || exit 1;) + +clean: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + $(MAKE) -C "$$dir" clean; \ + fi; \ + done;