From b0f7476fca372ce71f4cfbb89cd0d767ca86ca5d Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 28 Apr 2018 15:50:58 +0100 Subject: [PATCH 1/2] remove do_unwind_module hook --- src/cbmc/bmc.cpp | 8 -------- src/cbmc/bmc.h | 1 - 2 files changed, 9 deletions(-) diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 205e738d392..e236091631a 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -35,11 +35,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "counterexample_beautification.h" #include "fault_localization.h" -void bmct::do_unwind_module() -{ - // this is a hook for hw-cbmc -} - /// Hook used by CEGIS to selectively freeze variables /// in the SAT solver after the SSA formula is added to the solver. /// Freezing variables is necessary to make use of incremental @@ -118,9 +113,6 @@ void bmct::output_graphml(resultt result) void bmct::do_conversion() { - // convert HDL (hook for hw-cbmc) - do_unwind_module(); - status() << "converting SSA" << eom; // convert SSA diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 0f394199fe0..7401a641155 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -191,7 +191,6 @@ class bmct:public safety_checkert // unwinding virtual void setup_unwind(); - virtual void do_unwind_module(); void do_conversion(); virtual void freeze_program_variables(); From f6a92cc414fe8c9aed491ecf0b8ced31bde2a7f0 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 28 Apr 2018 17:01:38 +0100 Subject: [PATCH 2/2] remove bmc_constraints --- src/cbmc/bmc.cpp | 8 -------- src/cbmc/bmc.h | 3 --- 2 files changed, 11 deletions(-) diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index e236091631a..34edbb516a6 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -118,14 +118,6 @@ void bmct::do_conversion() // convert SSA equation.convert(prop_conv); - // the 'extra constraints' - if(!bmc_constraints.empty()) - { - status() << "converting constraints" << eom; - - for(const auto &constraint : bmc_constraints) - prop_conv.set_to_true(constraint); - } // hook for cegis to freeze synthesis program vars freeze_program_variables(); } diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 7401a641155..32ec40b29a2 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -100,9 +100,6 @@ class bmct:public safety_checkert safety_checkert::resultt execute(abstract_goto_modelt &); virtual ~bmct() { } - // additional stuff - std::list bmc_constraints; - void set_ui(ui_message_handlert::uit _ui) { ui=_ui; } // the safety_checkert interface