Skip to content

Commit 73b4357

Browse files
author
Daniel Kroening
authored
Merge pull request #1339 from diffblue/initialize_goto_model
New API for getting goto models
2 parents 4febd10 + 7d30cde commit 73b4357

File tree

134 files changed

+1053
-1311
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

134 files changed

+1053
-1311
lines changed

‎src/analyses/call_graph.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -18,9 +18,9 @@ call_grapht::call_grapht()
1818
{
1919
}
2020

21-
call_grapht::call_grapht(const goto_functionst &goto_functions)
21+
call_grapht::call_grapht(const goto_modelt &goto_model)
2222
{
23-
forall_goto_functions(f_it, goto_functions)
23+
forall_goto_functions(f_it, goto_model.goto_functions)
2424
{
2525
const goto_programt &body=f_it->second.body;
2626
add(f_it->first, body);

‎src/analyses/call_graph.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -15,13 +15,13 @@ Author: Daniel Kroening, [email protected]
1515
#include <iosfwd>
1616
#include <map>
1717

18-
#include <goto-programs/goto_functions.h>
18+
#include <goto-programs/goto_model.h>
1919

2020
class call_grapht
2121
{
2222
public:
2323
call_grapht();
24-
explicit call_grapht(const goto_functionst &);
24+
explicit call_grapht(const goto_modelt &);
2525

2626
void output_dot(std::ostream &out) const;
2727
void output(std::ostream &out) const;

‎src/analyses/constant_propagator.h

+4-4
Original file line numberDiff line numberDiff line change
@@ -110,11 +110,11 @@ class constant_propagator_ait:public ait<constant_propagator_domaint>
110110
{
111111
public:
112112
constant_propagator_ait(
113-
goto_functionst &goto_functions,
114-
const namespacet &ns)
113+
goto_modelt &goto_model)
115114
{
116-
operator()(goto_functions, ns);
117-
replace(goto_functions, ns);
115+
const namespacet ns(goto_model.symbol_table);
116+
operator()(goto_model.goto_functions, ns);
117+
replace(goto_model.goto_functions, ns);
118118
}
119119

120120
constant_propagator_ait(

‎src/analyses/custom_bitvector_analysis.cpp

+4-3
Original file line numberDiff line numberDiff line change
@@ -682,14 +682,13 @@ void custom_bitvector_analysist::instrument(goto_functionst &)
682682
}
683683

684684
void custom_bitvector_analysist::check(
685-
const namespacet &ns,
686-
const goto_functionst &goto_functions,
685+
const goto_modelt &goto_model,
687686
bool use_xml,
688687
std::ostream &out)
689688
{
690689
unsigned pass=0, fail=0, unknown=0;
691690

692-
forall_goto_functions(f_it, goto_functions)
691+
forall_goto_functions(f_it, goto_model.goto_functions)
693692
{
694693
if(!f_it->second.body.has_assertion())
695694
continue;
@@ -715,6 +714,7 @@ void custom_bitvector_analysist::check(
715714
continue;
716715

717716
exprt tmp=eval(i_it->guard, i_it);
717+
const namespacet ns(goto_model.symbol_table);
718718
result=simplify_expr(tmp, ns);
719719

720720
description=i_it->source_location.get_comment();
@@ -744,6 +744,7 @@ void custom_bitvector_analysist::check(
744744
if(!description.empty())
745745
out << ", " << description;
746746
out << ": ";
747+
const namespacet ns(goto_model.symbol_table);
747748
out << from_expr(ns, f_it->first, result);
748749
out << '\n';
749750
}

‎src/analyses/custom_bitvector_analysis.h

+1-2
Original file line numberDiff line numberDiff line change
@@ -128,8 +128,7 @@ class custom_bitvector_analysist:public ait<custom_bitvector_domaint>
128128
public:
129129
void instrument(goto_functionst &);
130130
void check(
131-
const namespacet &,
132-
const goto_functionst &,
131+
const goto_modelt &,
133132
bool xml, std::ostream &);
134133

135134
exprt eval(const exprt &src, locationt loc)

‎src/analyses/escape_analysis.cpp

+4-3
Original file line numberDiff line numberDiff line change
@@ -436,10 +436,11 @@ void escape_analysist::insert_cleanup(
436436
}
437437

438438
void escape_analysist::instrument(
439-
goto_functionst &goto_functions,
440-
const namespacet &ns)
439+
goto_modelt &goto_model)
441440
{
442-
Forall_goto_functions(f_it, goto_functions)
441+
const namespacet ns(goto_model.symbol_table);
442+
443+
Forall_goto_functions(f_it, goto_model.goto_functions)
443444
{
444445
Forall_goto_program_instructions(i_it, f_it->second.body)
445446
{

‎src/analyses/escape_analysis.h

+1-3
Original file line numberDiff line numberDiff line change
@@ -95,9 +95,7 @@ class escape_domaint:public ai_domain_baset
9595
class escape_analysist:public ait<escape_domaint>
9696
{
9797
public:
98-
void instrument(
99-
goto_functionst &,
100-
const namespacet &);
98+
void instrument(goto_modelt &);
10199

102100
protected:
103101
virtual void initialize(const goto_functionst &_goto_functions)

‎src/analyses/goto_rw.h

+4-4
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ Date: April 2010
1919

2020
#include <util/guard.h>
2121

22-
#include <goto-programs/goto_program.h>
22+
#include <goto-programs/goto_model.h>
2323

2424
#define forall_rw_range_set_r_objects(it, rw_set) \
2525
for(rw_range_sett::objectst::const_iterator it=(rw_set).get_r_set().begin(); \
@@ -30,15 +30,15 @@ Date: April 2010
3030
it!=(rw_set).get_w_set().end(); ++it)
3131

3232
class rw_range_sett;
33-
class goto_functionst;
33+
class goto_modelt;
3434

3535
void goto_rw(goto_programt::const_targett target,
3636
rw_range_sett &rw_set);
3737

38-
void goto_rw(const goto_programt &goto_program,
38+
void goto_rw(const goto_programt &,
3939
rw_range_sett &rw_set);
4040

41-
void goto_rw(const goto_functionst &goto_functions,
41+
void goto_rw(const goto_functionst &,
4242
const irep_idt &function,
4343
rw_range_sett &rw_set);
4444

‎src/analyses/interval_analysis.cpp

+4-5
Original file line numberDiff line numberDiff line change
@@ -76,14 +76,13 @@ void instrument_intervals(
7676
}
7777
}
7878

79-
void interval_analysis(
80-
const namespacet &ns,
81-
goto_functionst &goto_functions)
79+
void interval_analysis(goto_modelt &goto_model)
8280
{
8381
ait<interval_domaint> interval_analysis;
8482

85-
interval_analysis(goto_functions, ns);
83+
const namespacet ns(goto_model.symbol_table);
84+
interval_analysis(goto_model.goto_functions, ns);
8685

87-
Forall_goto_functions(f_it, goto_functions)
86+
Forall_goto_functions(f_it, goto_model.goto_functions)
8887
instrument_intervals(interval_analysis, f_it->second);
8988
}

‎src/analyses/interval_analysis.h

+2-5
Original file line numberDiff line numberDiff line change
@@ -12,11 +12,8 @@ Author: Daniel Kroening, [email protected]
1212
#ifndef CPROVER_ANALYSES_INTERVAL_ANALYSIS_H
1313
#define CPROVER_ANALYSES_INTERVAL_ANALYSIS_H
1414

15-
#include <util/namespace.h>
16-
#include <goto-programs/goto_functions.h>
15+
class goto_modelt;
1716

18-
void interval_analysis(
19-
const namespacet &ns,
20-
goto_functionst &goto_functions);
17+
void interval_analysis(goto_modelt &);
2118

2219
#endif // CPROVER_ANALYSES_INTERVAL_ANALYSIS_H

‎src/analyses/is_threaded.h

+7-1
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ Date: October 2012
1616

1717
#include <set>
1818

19-
#include <goto-programs/goto_functions.h>
19+
#include <goto-programs/goto_model.h>
2020

2121
class is_threadedt
2222
{
@@ -27,6 +27,12 @@ class is_threadedt
2727
compute(goto_functions);
2828
}
2929

30+
explicit is_threadedt(
31+
const goto_modelt &goto_model)
32+
{
33+
compute(goto_model.goto_functions);
34+
}
35+
3036
bool operator()(const goto_programt::const_targett t) const
3137
{
3238
return is_threaded_set.find(t)!=is_threaded_set.end();

‎src/analyses/natural_loops.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,9 @@ Author: Georg Weissenbacher, [email protected]
1313

1414
#include <iostream>
1515

16-
void show_natural_loops(const goto_functionst &goto_functions)
16+
void show_natural_loops(const goto_modelt &goto_model)
1717
{
18-
forall_goto_functions(it, goto_functions)
18+
forall_goto_functions(it, goto_model.goto_functions)
1919
{
2020
std::cout << "*** " << it->first << '\n';
2121

‎src/analyses/natural_loops.h

+2-3
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,7 @@ Author: Georg Weissenbacher, [email protected]
1616
#include <iosfwd>
1717
#include <set>
1818

19-
#include <goto-programs/goto_program.h>
20-
#include <goto-programs/goto_functions.h>
19+
#include <goto-programs/goto_model.h>
2120

2221
#include "cfg_dominators.h"
2322

@@ -70,7 +69,7 @@ class natural_loopst:
7069
typedef natural_loops_templatet<goto_programt, goto_programt::targett>
7170
natural_loops_mutablet;
7271

73-
void show_natural_loops(const goto_functionst &goto_functions);
72+
void show_natural_loops(const goto_modelt &);
7473

7574
/// Finds all back-edges and computes the natural loops
7675
#ifdef DEBUG

‎src/cbmc/bmc.h

+4-3
Original file line numberDiff line numberDiff line change
@@ -16,14 +16,15 @@ Author: Daniel Kroening, [email protected]
1616
#include <map>
1717

1818
#include <util/options.h>
19+
#include <util/ui_message.h>
1920

2021
#include <solvers/prop/prop.h>
2122
#include <solvers/prop/prop_conv.h>
2223
#include <solvers/sat/cnf.h>
2324
#include <solvers/sat/satcheck.h>
2425
#include <solvers/smt1/smt1_dec.h>
2526
#include <solvers/smt2/smt2_dec.h>
26-
#include <langapi/language_ui.h>
27+
2728
#include <goto-symex/symex_target_equation.h>
2829
#include <goto-programs/safety_checker.h>
2930

@@ -56,7 +57,7 @@ class bmct:public safety_checkert
5657
// additional stuff
5758
expr_listt bmc_constraints;
5859

59-
void set_ui(language_uit::uit _ui) { ui=_ui; }
60+
void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
6061

6162
// the safety_checkert interface
6263
virtual resultt operator()(
@@ -74,7 +75,7 @@ class bmct:public safety_checkert
7475
prop_convt &prop_conv;
7576

7677
// use gui format
77-
language_uit::uit ui;
78+
ui_message_handlert::uit ui;
7879

7980
virtual decision_proceduret::resultt
8081
run_decision_procedure(prop_convt &prop_conv);

0 commit comments

Comments
 (0)