Skip to content

Commit 76d202a

Browse files
author
Daniel Kroening
committed
use goto_function.h when only goto_functiont is used
1 parent b9cd297 commit 76d202a

File tree

6 files changed

+10
-8
lines changed

6 files changed

+10
-8
lines changed

src/analyses/local_cfg.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected]
1414

1515
#include <util/numbering.h>
1616

17-
#include <goto-programs/goto_functions.h>
17+
#include <goto-programs/goto_program.h>
1818

1919
class local_cfgt
2020
{

src/analyses/locals.h

+1-3
Original file line numberDiff line numberDiff line change
@@ -14,13 +14,11 @@ Date: March 2013
1414
#ifndef CPROVER_ANALYSES_LOCALS_H
1515
#define CPROVER_ANALYSES_LOCALS_H
1616

17-
#include <goto-programs/goto_functions.h>
17+
#include <goto-programs/goto_function.h>
1818

1919
class localst
2020
{
2121
public:
22-
typedef goto_functionst::goto_functiont goto_functiont;
23-
2422
explicit localst(const goto_functiont &goto_function)
2523
{
2624
build(goto_function);

src/goto-instrument/alignment_checks.cpp

+4
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,11 @@ Module: Alignment Checks
1212
#include "alignment_checks.h"
1313

1414
#include <util/config.h>
15+
#include <util/namespace.h>
1516
#include <util/pointer_offset_size.h>
17+
#include <util/std_types.h>
18+
19+
#include <ostream>
1620

1721
void print_struct_alignment_problems(
1822
const symbol_tablet &symbol_table,

src/goto-instrument/alignment_checks.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ Module: Alignment Checks
1414

1515
#include <iosfwd>
1616

17-
#include <goto-programs/goto_functions.h>
17+
#include <util/symbol_table.h>
1818

1919
void print_struct_alignment_problems(
2020
const symbol_tablet &symbol_table,

src/goto-programs/generate_function_bodies.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ Author: Diffblue Ltd.
1212
#include <memory>
1313
#include <regex>
1414

15-
#include <goto-programs/goto_functions.h>
15+
#include <goto-programs/goto_function.h>
1616
#include <goto-programs/goto_model.h>
1717
#include <util/cmdline.h>
1818
#include <util/message.h>

src/goto-symex/goto_symex_state.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ Author: Daniel Kroening, [email protected]
2424
#include <util/make_unique.h>
2525

2626
#include <pointer-analysis/value_set.h>
27-
#include <goto-programs/goto_functions.h>
27+
#include <goto-programs/goto_function.h>
2828

2929
#include "symex_target_equation.h"
3030

@@ -365,7 +365,7 @@ class goto_symex_statet final
365365
bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns);
366366

367367
void populate_dirty_for_function(
368-
const irep_idt &id, const goto_functionst::goto_functiont &);
368+
const irep_idt &id, const goto_functiont &);
369369

370370
void switch_to_thread(unsigned t);
371371
bool record_events;

0 commit comments

Comments
 (0)