Skip to content

Commit f23ac19

Browse files
Move bmc_util to goto_checker module
1 parent 3892c55 commit f23ac19

File tree

6 files changed

+8
-6
lines changed

6 files changed

+8
-6
lines changed

src/cbmc/all_properties.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected]
1414
#include <algorithm>
1515
#include <chrono>
1616

17-
#include <cbmc/bmc_util.h>
17+
#include <goto-checker/bmc_util.h>
1818

1919
#include <util/xml.h>
2020
#include <util/json.h>

src/cbmc/bmc.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,9 +24,9 @@ Author: Daniel Kroening, [email protected]
2424

2525
#include <linking/static_lifetime_init.h>
2626

27+
#include <goto-checker/bmc_util.h>
2728
#include <goto-checker/solver_factory.h>
2829

29-
#include "bmc_util.h"
3030
#include "counterexample_beautification.h"
3131
#include "fault_localization.h"
3232

src/cbmc/bmc_cover.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected]
1414
#include <chrono>
1515
#include <iomanip>
1616

17-
#include <cbmc/bmc_util.h>
17+
#include <goto-checker/bmc_util.h>
1818

1919
#include <util/xml.h>
2020
#include <util/xml_expr.h>

src/cbmc/fault_localization.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,8 @@ Author: Peter Schrammel
2626
#include <goto-symex/build_goto_trace.h>
2727
#include <goto-programs/xml_goto_trace.h>
2828

29-
#include "bmc_util.h"
29+
#include <goto-checker/bmc_util.h>
30+
3031
#include "counterexample_beautification.h"
3132

3233
void fault_localizationt::freeze_guards()
File renamed without changes.

src/cbmc/bmc_util.h renamed to src/goto-checker/bmc_util.h

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ Author: Daniel Kroening, Peter Schrammel
99
/// \file
1010
/// Bounded Model Checking Utilities
1111

12-
#ifndef CPROVER_CBMC_BMC_UTIL_H
13-
#define CPROVER_CBMC_BMC_UTIL_H
12+
#ifndef CPROVER_GOTO_CHECKER_BMC_UTIL_H
13+
#define CPROVER_GOTO_CHECKER_BMC_UTIL_H
1414

1515
#include <goto-programs/safety_checker.h>
1616

@@ -70,3 +70,4 @@ void slice(
7070
const optionst &,
7171
ui_message_handlert &);
7272

73+
#endif // CPROVER_GOTO_CHECKER_BMC_UTIL_H

0 commit comments

Comments
 (0)