From 62fbfe8e2f41fc1cd182c181752b856b06f5029d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 27 Apr 2023 11:24:15 +0000 Subject: [PATCH 1/3] analyses/loop_analysis.h: fix includes Direct use of this header file made apparent that it didn't include what actually is required to use it: the declaration of goto_modelt. --- src/analyses/loop_analysis.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/loop_analysis.h b/src/analyses/loop_analysis.h index a8a2d683925..358879e1f13 100644 --- a/src/analyses/loop_analysis.h +++ b/src/analyses/loop_analysis.h @@ -13,7 +13,7 @@ Author: Diffblue Ltd #ifndef CPROVER_ANALYSES_LOOP_ANALYSIS_H #define CPROVER_ANALYSES_LOOP_ANALYSIS_H -#include +#include template class loop_analysist; From b96bbeb33777f06d1d11f34546815908563eb372 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 27 Apr 2023 11:26:27 +0000 Subject: [PATCH 2/3] build_loop_nesting_graph: remove unused logging parameter There is no actual logging done. --- .../contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp | 4 +--- .../contracts/dynamic-frames/dfcc_loop_nesting_graph.h | 4 ++-- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp index d01fb222b4d..9cfd79f13e0 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp @@ -13,7 +13,6 @@ Date: March 2023 #include "dfcc_loop_nesting_graph.h" #include -#include dfcc_loop_nesting_graph_nodet::dfcc_loop_nesting_graph_nodet( const goto_programt::targett &head, @@ -24,8 +23,7 @@ dfcc_loop_nesting_graph_nodet::dfcc_loop_nesting_graph_nodet( } /// \pre Loop normal form properties must hold. -dfcc_loop_nesting_grapht -build_loop_nesting_graph(goto_programt &goto_program, messaget &log) +dfcc_loop_nesting_grapht build_loop_nesting_graph(goto_programt &goto_program) { natural_loops_mutablet natural_loops(goto_program); dfcc_loop_nesting_grapht loop_nesting_graph; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.h index 6ecd70b5355..e554f727a31 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.h @@ -47,6 +47,6 @@ typedef grapht dfcc_loop_nesting_grapht; /// loops in the given \p goto_program. /// A loop is considered nested in an outer loop if its head and its latch are /// both found in the instructions of the outer loop. -dfcc_loop_nesting_grapht -build_loop_nesting_graph(goto_programt &goto_program, messaget &log); +dfcc_loop_nesting_grapht build_loop_nesting_graph(goto_programt &goto_program); + #endif From fe428ad613b91623a9967df29e912edf21835c01 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 27 Apr 2023 11:26:58 +0000 Subject: [PATCH 3/3] dfcc_loop_nesting_grapht: cleanup loop includes Directly refer to the classes rather than going through a series of (member) typedefs and one header that is rather unrelated. --- .../contracts/dynamic-frames/dfcc_cfg_info.cpp | 5 ++--- .../contracts/dynamic-frames/dfcc_cfg_info.h | 3 +-- .../contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp | 4 ++-- .../contracts/dynamic-frames/dfcc_loop_nesting_graph.h | 6 +++--- 4 files changed, 8 insertions(+), 10 deletions(-) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp index 5c942541b4f..67857f71548 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp @@ -522,16 +522,15 @@ dfcc_cfg_infot::dfcc_cfg_infot( : function_id(function_id), goto_function(goto_function), top_level_write_set(top_level_write_set), - log(message_handler), ns(symbol_table) { dfcc_loop_nesting_grapht loop_nesting_graph; goto_programt &goto_program = goto_function.body; - messaget log(message_handler); if(loop_contract_mode != dfcc_loop_contract_modet::NONE) { + messaget log(message_handler); dfcc_check_loop_normal_form(goto_program, log); - loop_nesting_graph = build_loop_nesting_graph(goto_program, log); + loop_nesting_graph = build_loop_nesting_graph(goto_program); const auto head = check_inner_loops_have_contracts(loop_nesting_graph); if(head.has_value()) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h index 2149fc8a49d..3c36c55d9d2 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h @@ -17,7 +17,6 @@ Date: March 2023 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CFG_INFO_H #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CFG_INFO_H -#include #include #include #include @@ -33,6 +32,7 @@ Date: March 2023 class dfcc_utilst; class dfcc_libraryt; class goto_functiont; +class message_handlert; /// \brief Describes a single loop for the purpose of DFCC loop contract /// instrumentation. @@ -297,7 +297,6 @@ class dfcc_cfg_infot const irep_idt &function_id; goto_functiont &goto_function; const exprt &top_level_write_set; - messaget log; const namespacet ns; /// True iff \p id is in the valid range for a loop id or is equal to diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp index 9cfd79f13e0..269cb06f5f6 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp @@ -12,12 +12,12 @@ Date: March 2023 #include "dfcc_loop_nesting_graph.h" -#include +#include dfcc_loop_nesting_graph_nodet::dfcc_loop_nesting_graph_nodet( const goto_programt::targett &head, const goto_programt::targett &latch, - const loopt &instructions) + const loop_templatet &instructions) : head(head), latch(latch), instructions(instructions) { } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.h index e554f727a31..a2391af5328 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.h @@ -18,7 +18,7 @@ Date: March 2023 #include -#include +#include class messaget; @@ -29,7 +29,7 @@ struct dfcc_loop_nesting_graph_nodet : public graph_nodet dfcc_loop_nesting_graph_nodet( const goto_programt::targett &head, const goto_programt::targett &latch, - const loopt &instructions); + const loop_templatet &instructions); /// Loop head instruction goto_programt::targett head; @@ -38,7 +38,7 @@ struct dfcc_loop_nesting_graph_nodet : public graph_nodet goto_programt::targett latch; /// Set of loop instructions - loopt instructions; + loop_templatet instructions; }; typedef grapht dfcc_loop_nesting_grapht;