Skip to content

Commit 5c65731

Browse files
tautschnigtautschnig
authored
Merge pull request diffblue#1612 from reuk/reuk/more-iterator-fixes
Iterator comparison and memory bug fixes
2 parents 48ee475 + d423c65 commit 5c65731

Some content is hidden

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

45 files changed

+174
-70
lines changed

‎.travis.yml

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,9 @@ jobs:
6565
before_install:
6666
- mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
6767
# env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
68-
env: COMPILER="ccache g++-5"
68+
env:
69+
- COMPILER="ccache g++-5"
70+
- EXTRA_CXXFLAGS="-D_GLIBCXX_DEBUG"
6971

7072
# OS X using g++
7173
- stage: Test different OS/CXX/Flags

‎regression/cbmc-cover/built-ins7/test.desc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--cover mcdc --unwind 5
44
^EXIT=0$
@@ -7,3 +7,6 @@ main.c
77
--
88
^warning: ignoring
99
^\[.*<builtin-library-
10+
--
11+
Knownbug added because this test triggers an invariant in cover.cpp
12+
See #1622 for details

‎regression/cbmc-cover/mcdc1/test.desc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--cover mcdc
44
^EXIT=0$
@@ -12,3 +12,6 @@ main.c
1212
^\*\* .* of .* covered \(100.0%\)$
1313
--
1414
^warning: ignoring
15+
--
16+
Knownbug added because this test triggers an invariant in cover.cpp
17+
See #1622 for details

‎regression/cbmc-cover/mcdc10/test.desc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--cover mcdc
44
^EXIT=0$
@@ -10,3 +10,6 @@ main.c
1010
^\*\* .* of .* covered \(100.0%\)$
1111
--
1212
^warning: ignoring
13+
--
14+
Knownbug added because this test triggers an invariant in cover.cpp
15+
See #1622 for details

‎regression/cbmc-cover/mcdc11/test.desc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--cover mcdc
44
^EXIT=0$
@@ -12,3 +12,6 @@ main.c
1212
^\*\* .* of .* covered \(100.0%\)$
1313
--
1414
^warning: ignoring
15+
--
16+
Knownbug added because this test triggers an invariant in cover.cpp
17+
See #1622 for details

‎regression/cbmc-cover/mcdc12/test.desc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--cover mcdc
44
^EXIT=0$
@@ -15,3 +15,6 @@ main.c
1515
^\*\* .* of .* covered \(100.0%\)$
1616
--
1717
^warning: ignoring
18+
--
19+
Knownbug added because this test triggers an invariant in cover.cpp
20+
See #1622 for details

‎regression/cbmc-cover/mcdc13/test.desc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--cover mcdc
44
^EXIT=0$
@@ -10,3 +10,6 @@ main.c
1010
^\*\* .* of .* covered \(100.0%\)$
1111
--
1212
^warning: ignoring
13+
--
14+
Knownbug added because this test triggers an invariant in cover.cpp
15+
See #1622 for details

‎regression/cbmc-cover/mcdc14/test.desc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--cover mcdc
44
^EXIT=0$
@@ -8,3 +8,6 @@ main.c
88
^\*\* .* of .* covered \(100.0%\)$
99
--
1010
^warning: ignoring
11+
--
12+
Knownbug added because this test triggers an invariant in cover.cpp
13+
See #1622 for details

‎regression/cbmc-cover/mcdc2/test.desc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--cover mcdc
44
^EXIT=0$
@@ -10,3 +10,6 @@ main.c
1010
^\*\* .* of .* covered \(100.0%\)$
1111
--
1212
^warning: ignoring
13+
--
14+
Knownbug added because this test triggers an invariant in cover.cpp
15+
See #1622 for details

‎regression/cbmc-cover/mcdc3/test.desc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--cover mcdc
44
^EXIT=0$
@@ -9,3 +9,6 @@ main.c
99
^\*\* .* of .* covered \(100.0%\)$
1010
--
1111
^warning: ignoring
12+
--
13+
Knownbug added because this test triggers an invariant in cover.cpp
14+
See #1622 for details

‎regression/cbmc-cover/mcdc4/test.desc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--cover mcdc
44
^EXIT=0$
@@ -11,3 +11,6 @@ main.c
1111
^\*\* .* of .* covered \(100.0%\)$
1212
--
1313
^warning: ignoring
14+
--
15+
Knownbug added because this test triggers an invariant in cover.cpp
16+
See #1622 for details

‎regression/cbmc-cover/mcdc5/test.desc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--cover mcdc
44
^EXIT=0$
@@ -11,3 +11,6 @@ main.c
1111
^\*\* .* of .* covered \(100.0%\)$
1212
--
1313
^warning: ignoring
14+
--
15+
Knownbug added because this test triggers an invariant in cover.cpp
16+
See #1622 for details

‎regression/cbmc-cover/mcdc6/test.desc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--cover mcdc
44
^EXIT=0$
@@ -8,3 +8,6 @@ main.c
88
^\*\* .* of .* covered \(100.0%\)$
99
--
1010
^warning: ignoring
11+
--
12+
Knownbug added because this test triggers an invariant in cover.cpp
13+
See #1622 for details

‎regression/cbmc-cover/mcdc7/test.desc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--cover mcdc
44
^EXIT=0$
@@ -10,3 +10,6 @@ main.c
1010
^\*\* .* of .* covered \(100.0%\)$
1111
--
1212
^warning: ignoring
13+
--
14+
Knownbug added because this test triggers an invariant in cover.cpp
15+
See #1622 for details

‎regression/cbmc-cover/mcdc8/test.desc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--cover mcdc
44
^EXIT=0$
@@ -10,3 +10,6 @@ main.c
1010
^\*\* .* of .* covered \(100.0%\)$
1111
--
1212
^warning: ignoring
13+
--
14+
Knownbug added because this test triggers an invariant in cover.cpp
15+
See #1622 for details

‎regression/cbmc-cover/mcdc9/test.desc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--cover mcdc
44
^EXIT=0$
@@ -11,3 +11,6 @@ main.c
1111
^\*\* .* of .* covered \(100.0%\)$
1212
--
1313
^warning: ignoring
14+
--
15+
Knownbug added because this test triggers an invariant in cover.cpp
16+
See #1622 for details

‎src/analyses/ai.cpp

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -365,7 +365,8 @@ bool ai_baset::visit(
365365
// initialize state, if necessary
366366
get_state(to_l);
367367

368-
new_values.transform(l, to_l, *this, ns);
368+
new_values.transform(
369+
l, to_l, *this, ns, ai_domain_baset::edge_typet::FUNCTION_LOCAL);
369370

370371
if(merge(new_values, l, to_l))
371372
have_new_values=true;
@@ -398,7 +399,8 @@ bool ai_baset::do_function_call(
398399
{
399400
// if we don't have a body, we just do an edige call -> return
400401
std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
401-
tmp_state->transform(l_call, l_return, *this, ns);
402+
tmp_state->transform(
403+
l_call, l_return, *this, ns, ai_domain_baset::edge_typet::FUNCTION_LOCAL);
402404

403405
return merge(*tmp_state, l_call, l_return);
404406
}
@@ -415,7 +417,8 @@ bool ai_baset::do_function_call(
415417

416418
// do the edge from the call site to the beginning of the function
417419
std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
418-
tmp_state->transform(l_call, l_begin, *this, ns);
420+
tmp_state->transform(
421+
l_call, l_begin, *this, ns, ai_domain_baset::edge_typet::CALL);
419422

420423
bool new_data=false;
421424

@@ -442,7 +445,8 @@ bool ai_baset::do_function_call(
442445
return false; // function exit point not reachable
443446

444447
std::unique_ptr<statet> tmp_state(make_temporary_state(end_state));
445-
tmp_state->transform(l_end, l_return, *this, ns);
448+
tmp_state->transform(
449+
l_end, l_return, *this, ns, ai_domain_baset::edge_typet::RETURN);
446450

447451
// Propagate those
448452
return merge(*tmp_state, l_end, l_return);

‎src/analyses/ai.h

Lines changed: 12 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,13 @@ class ai_baset;
3131
class ai_domain_baset
3232
{
3333
public:
34+
enum class edge_typet
35+
{
36+
FUNCTION_LOCAL,
37+
CALL,
38+
RETURN,
39+
};
40+
3441
// The constructor is expected to produce 'false'
3542
// or 'bottom'
3643
ai_domain_baset()
@@ -53,7 +60,8 @@ class ai_domain_baset
5360
locationt from,
5461
locationt to,
5562
ai_baset &ai,
56-
const namespacet &ns)=0;
63+
const namespacet &ns,
64+
edge_typet edge_type) = 0;
5765

5866
virtual void output(
5967
std::ostream &out,
@@ -401,7 +409,9 @@ class ait:public ai_baset
401409
}
402410

403411
protected:
404-
typedef std::unordered_map<locationt, domainT, const_target_hash> state_mapt;
412+
typedef std::
413+
unordered_map<locationt, domainT, const_target_hash, pointee_address_equalt>
414+
state_mapt;
405415
state_mapt state_map;
406416

407417
// this one creates states, if need be

‎src/analyses/constant_propagator.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,8 @@ void constant_propagator_domaint::transform(
4545
locationt from,
4646
locationt to,
4747
ai_baset &ai,
48-
const namespacet &ns)
48+
const namespacet &ns,
49+
ai_domain_baset::edge_typet edge_type)
4950
{
5051
#ifdef DEBUG
5152
std::cout << "Transform from/to:\n";
@@ -129,7 +130,7 @@ void constant_propagator_domaint::transform(
129130
const symbol_exprt &symbol_expr=to_symbol_expr(function);
130131
const irep_idt id=symbol_expr.get_identifier();
131132

132-
if(to==next)
133+
if(edge_type == ai_domain_baset::edge_typet::FUNCTION_LOCAL)
133134
{
134135
if(id==CPROVER_PREFIX "set_must" ||
135136
id==CPROVER_PREFIX "get_must" ||

‎src/analyses/constant_propagator.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,8 @@ class constant_propagator_domaint:public ai_domain_baset
2525
locationt from,
2626
locationt to,
2727
ai_baset &ai_base,
28-
const namespacet &ns) final override;
28+
const namespacet &ns,
29+
ai_domain_baset::edge_typet edge_type) final override;
2930

3031
virtual void output(
3132
std::ostream &out,

‎src/analyses/custom_bitvector_analysis.cpp

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -269,7 +269,8 @@ void custom_bitvector_domaint::transform(
269269
locationt from,
270270
locationt to,
271271
ai_baset &ai,
272-
const namespacet &ns)
272+
const namespacet &ns,
273+
ai_domain_baset::edge_typet edge_type)
273274
{
274275
// upcast of ai
275276
custom_bitvector_analysist &cba=
@@ -395,11 +396,8 @@ void custom_bitvector_domaint::transform(
395396
}
396397
else
397398
{
398-
goto_programt::const_targett next=from;
399-
++next;
400-
401399
// only if there is an actual call, i.e., we have a body
402-
if(next!=to)
400+
if(edge_type != ai_domain_baset::edge_typet::FUNCTION_LOCAL)
403401
{
404402
const code_typet &code_type=
405403
to_code_type(ns.lookup(identifier).type);

‎src/analyses/custom_bitvector_analysis.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,8 @@ class custom_bitvector_domaint:public ai_domain_baset
2727
locationt from,
2828
locationt to,
2929
ai_baset &ai,
30-
const namespacet &ns) final override;
30+
const namespacet &ns,
31+
ai_domain_baset::edge_typet edge_type) final override;
3132

3233
void output(
3334
std::ostream &out,

‎src/analyses/dependence_graph.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -187,18 +187,18 @@ void dep_graph_domaint::transform(
187187
goto_programt::const_targett from,
188188
goto_programt::const_targett to,
189189
ai_baset &ai,
190-
const namespacet &ns)
190+
const namespacet &ns,
191+
ai_domain_baset::edge_typet edge_type)
191192
{
192193
dependence_grapht *dep_graph=dynamic_cast<dependence_grapht*>(&ai);
193194
assert(dep_graph!=nullptr);
194195

195196
// propagate control dependencies across function calls
196197
if(from->is_function_call())
197198
{
198-
goto_programt::const_targett next=from;
199-
++next;
199+
const goto_programt::const_targett next = std::next(from);
200200

201-
if(next==to)
201+
if(edge_type == ai_domain_baset::edge_typet::FUNCTION_LOCAL)
202202
{
203203
control_dependencies(from, to, *dep_graph);
204204
}

‎src/analyses/dependence_graph.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -83,7 +83,8 @@ class dep_graph_domaint:public ai_domain_baset
8383
goto_programt::const_targett from,
8484
goto_programt::const_targett to,
8585
ai_baset &ai,
86-
const namespacet &ns) final override;
86+
const namespacet &ns,
87+
ai_domain_baset::edge_typet edge_type) final override;
8788

8889
void output(
8990
std::ostream &out,

‎src/analyses/escape_analysis.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -165,7 +165,8 @@ void escape_domaint::transform(
165165
locationt from,
166166
locationt to,
167167
ai_baset &ai,
168-
const namespacet &ns)
168+
const namespacet &ns,
169+
ai_domain_baset::edge_typet /*edge_type*/)
169170
{
170171
if(has_values.is_false())
171172
return;

‎src/analyses/escape_analysis.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,8 @@ class escape_domaint:public ai_domain_baset
3232
locationt from,
3333
locationt to,
3434
ai_baset &ai,
35-
const namespacet &ns) final override;
35+
const namespacet &ns,
36+
ai_domain_baset::edge_typet edge_type) final override;
3637

3738
void output(
3839
std::ostream &out,

0 commit comments

Comments
 (0)