Skip to content

Commit 73635f0

Browse files
author
Daniel Kroening
authored
Merge pull request #447 from tautschnig/no-gen_zero
Remove gen_zero/gen_one
2 parents 46e0b9f + 31ce11f commit 73635f0

File tree

130 files changed

+521
-578
lines changed

Some content is hidden

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

130 files changed

+521
-578
lines changed

‎regression/cbmc-java/Makefile

+8-2
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,16 @@
11
default: tests.log
22

33
test:
4-
@../test.pl -c ../../../src/cbmc/cbmc
4+
@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
5+
../failed-tests-printer.pl ; \
6+
exit 1 ; \
7+
fi
58

69
tests.log: ../test.pl
7-
@../test.pl -c ../../../src/cbmc/cbmc
10+
@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
11+
../failed-tests-printer.pl ; \
12+
exit 1 ; \
13+
fi
814

915
show:
1016
@for dir in *; do \

‎src/aa-path-symex/path_symex.cpp

+2-3
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
1111
#include <util/simplify_expr.h>
1212
#include <util/byte_operators.h>
1313
#include <util/pointer_offset_size.h>
14-
#include <util/expr_util.h>
1514
#include <util/base_type.h>
1615

1716
#include <ansi-c/c_types.h>
@@ -353,7 +352,7 @@ void path_symext::symex_malloc(
353352
rhs.type()=pointer_typet(value_symbol.type.subtype());
354353
index_exprt index_expr(value_symbol.type.subtype());
355354
index_expr.array()=value_symbol.symbol_expr();
356-
index_expr.index()=gen_zero(index_type());
355+
index_expr.index()=from_integer(0, index_type());
357356
rhs.op0()=index_expr;
358357
}
359358
else
@@ -486,7 +485,7 @@ void path_symext::assign_rec(
486485
else if(compound_type.id()==ID_union)
487486
{
488487
// rewrite into byte_extract, and do again
489-
exprt offset=gen_zero(index_type());
488+
exprt offset=from_integer(0, index_type());
490489

491490
byte_extract_exprt
492491
new_lhs(byte_update_id(), struct_op, offset, ssa_rhs.type());

‎src/aa-path-symex/path_symex_state.cpp

-1
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@ Author: Daniel Kroening, [email protected]
99

1010
#include <util/simplify_expr.h>
1111
#include <util/arith_tools.h>
12-
#include <util/expr_util.h>
1312
#include <util/decision_procedure.h>
1413

1514
#include <ansi-c/c_types.h>

‎src/analyses/ai.cpp

-1
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include <util/std_expr.h>
1313
#include <util/std_code.h>
14-
#include <util/expr_util.h>
1514

1615
#include "is_threaded.h"
1716

‎src/analyses/flow_insensitive_analysis.cpp

-1
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include <util/std_expr.h>
1313
#include <util/std_code.h>
14-
#include <util/expr_util.h>
1514

1615
#include "flow_insensitive_analysis.h"
1716

‎src/analyses/goto_check.cpp

+20-13
Original file line numberDiff line numberDiff line change
@@ -188,7 +188,7 @@ void goto_checkt::div_by_zero_check(
188188

189189
// add divison by zero subgoal
190190

191-
exprt zero=gen_zero(expr.op1().type());
191+
exprt zero=from_integer(0, expr.op1().type());
192192

193193
if(zero.is_nil())
194194
throw "no zero of argument type of operator "+expr.id_string();
@@ -233,7 +233,7 @@ void goto_checkt::undefined_shift_check(
233233
if(distance_type.id()==ID_signedbv)
234234
{
235235
binary_relation_exprt inequality(
236-
expr.distance(), ID_ge, gen_zero(distance_type));
236+
expr.distance(), ID_ge, from_integer(0, distance_type));
237237

238238
add_guarded_claim(
239239
inequality,
@@ -289,7 +289,7 @@ void goto_checkt::mod_by_zero_check(
289289

290290
// add divison by zero subgoal
291291

292-
exprt zero=gen_zero(expr.op1().type());
292+
exprt zero=from_integer(0, expr.op1().type());
293293

294294
if(zero.is_nil())
295295
throw "no zero of argument type of operator "+expr.id_string();
@@ -802,8 +802,8 @@ void goto_checkt::nan_check(
802802
// 0/0 = NaN and x/inf = NaN
803803
// (note that x/0 = +-inf for x!=0 and x!=inf)
804804
exprt zero_div_zero=and_exprt(
805-
ieee_float_equal_exprt(expr.op0(), gen_zero(expr.op0().type())),
806-
ieee_float_equal_exprt(expr.op1(), gen_zero(expr.op1().type())));
805+
ieee_float_equal_exprt(expr.op0(), from_integer(0, expr.op0().type())),
806+
ieee_float_equal_exprt(expr.op1(), from_integer(0, expr.op1().type())));
807807

808808
exprt div_inf=unary_exprt(ID_isinf, expr.op1(), bool_typet());
809809

@@ -819,10 +819,10 @@ void goto_checkt::nan_check(
819819
// Inf * 0 is NaN
820820
exprt inf_times_zero=and_exprt(
821821
unary_exprt(ID_isinf, expr.op0(), bool_typet()),
822-
ieee_float_equal_exprt(expr.op1(), gen_zero(expr.op1().type())));
822+
ieee_float_equal_exprt(expr.op1(), from_integer(0, expr.op1().type())));
823823

824824
exprt zero_times_inf=and_exprt(
825-
ieee_float_equal_exprt(expr.op1(), gen_zero(expr.op1().type())),
825+
ieee_float_equal_exprt(expr.op1(), from_integer(0, expr.op1().type())),
826826
unary_exprt(ID_isinf, expr.op0(), bool_typet()));
827827

828828
isnan=or_exprt(inf_times_zero, zero_times_inf);
@@ -972,7 +972,8 @@ void goto_checkt::pointer_validity_check(
972972
return;
973973

974974
const exprt &pointer=expr.op0();
975-
const typet &pointer_type=to_pointer_type(ns.follow(pointer.type()));
975+
const pointer_typet &pointer_type=
976+
to_pointer_type(ns.follow(pointer.type()));
976977

977978
assert(base_type_eq(pointer_type.subtype(), expr.type(), ns));
978979

@@ -986,7 +987,7 @@ void goto_checkt::pointer_validity_check(
986987
{
987988
if(flags.is_unknown() || flags.is_null())
988989
{
989-
notequal_exprt not_eq_null(pointer, gen_zero(pointer.type()));
990+
notequal_exprt not_eq_null(pointer, null_pointer_exprt(pointer_type));
990991

991992
add_guarded_claim(
992993
not_eq_null,
@@ -1175,7 +1176,7 @@ void goto_checkt::bounds_check(
11751176
effective_offset=plus_exprt(p_offset, effective_offset);
11761177
}
11771178

1178-
exprt zero=gen_zero(ode.offset().type());
1179+
exprt zero=from_integer(0, ode.offset().type());
11791180
assert(zero.is_not_nil());
11801181

11811182
// the final offset must not be negative
@@ -1612,7 +1613,9 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
16121613

16131614
if(flags.is_unknown() || flags.is_null())
16141615
{
1615-
notequal_exprt not_eq_null(pointer, gen_zero(pointer.type()));
1616+
notequal_exprt not_eq_null(
1617+
pointer,
1618+
null_pointer_exprt(to_pointer_type(pointer.type())));
16161619

16171620
add_guarded_claim(
16181621
not_eq_null,
@@ -1651,7 +1654,9 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
16511654

16521655
if(pointer.type().subtype().get(ID_identifier)!="java::java.lang.AssertionError")
16531656
{
1654-
notequal_exprt not_eq_null(pointer, gen_zero(pointer.type()));
1657+
notequal_exprt not_eq_null(
1658+
pointer,
1659+
null_pointer_exprt(to_pointer_type(pointer.type())));
16551660

16561661
add_guarded_claim(
16571662
not_eq_null,
@@ -1718,7 +1723,9 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
17181723
source_locationt source_location;
17191724
source_location.set_function(i.function);
17201725

1721-
equal_exprt eq(leak_expr, gen_zero(ns.follow(leak.type)));
1726+
equal_exprt eq(
1727+
leak_expr,
1728+
null_pointer_exprt(to_pointer_type(leak.type)));
17221729
add_guarded_claim(
17231730
eq,
17241731
"dynamically allocated memory never freed",

‎src/analyses/invariant_propagation.cpp

-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,6 @@ Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

9-
#include <util/expr_util.h>
109
#include <util/simplify_expr.h>
1110
#include <util/base_type.h>
1211
#include <util/symbol_table.h>

‎src/analyses/invariant_set.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@ Author: Daniel Kroening, [email protected]
1010

1111
#include <util/symbol_table.h>
1212
#include <util/namespace.h>
13-
#include <util/expr_util.h>
1413
#include <util/arith_tools.h>
1514
#include <util/std_expr.h>
1615
#include <util/simplify_expr.h>
@@ -992,7 +991,7 @@ void invariant_sett::nnf(exprt &expr, bool negate)
992991
{
993992
equal_exprt tmp;
994993
tmp.lhs()=expr.op0();
995-
tmp.rhs()=gen_zero(expr.op0().type());
994+
tmp.rhs()=from_integer(0, expr.op0().type());
996995
nnf(tmp, !negate);
997996
expr.swap(tmp);
998997
}

‎src/analyses/local_may_alias.cpp

+3-2
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
99
#include <iterator>
1010
#include <algorithm>
1111

12+
#include <util/arith_tools.h>
1213
#include <util/std_expr.h>
1314
#include <util/std_code.h>
1415
#include <util/expr_util.h>
@@ -272,7 +273,7 @@ void local_may_aliast::get_rec(
272273
if(index_expr.array().id()==ID_symbol)
273274
{
274275
index_exprt tmp1=index_expr;
275-
tmp1.index()=gen_zero(index_type());
276+
tmp1.index()=from_integer(0, index_type());
276277
address_of_exprt tmp2(tmp1);
277278
unsigned object_nr=objects.number(tmp2);
278279
dest.insert(object_nr);
@@ -284,7 +285,7 @@ void local_may_aliast::get_rec(
284285
else if(index_expr.array().id()==ID_string_constant)
285286
{
286287
index_exprt tmp1=index_expr;
287-
tmp1.index()=gen_zero(index_type());
288+
tmp1.index()=from_integer(0, index_type());
288289
address_of_exprt tmp2(tmp1);
289290
unsigned object_nr=objects.number(tmp2);
290291
dest.insert(object_nr);

‎src/analyses/static_analysis.cpp

-1
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include <util/std_expr.h>
1313
#include <util/std_code.h>
14-
#include <util/expr_util.h>
1514

1615
#include "is_threaded.h"
1716

‎src/ansi-c/ansi_c_entry_point.cpp

+15-12
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@ Author: Daniel Kroening, [email protected]
1010
#include <cstdlib>
1111

1212
#include <util/namespace.h>
13-
#include <util/expr_util.h>
1413
#include <util/std_expr.h>
1514
#include <util/arith_tools.h>
1615
#include <util/std_code.h>
@@ -90,7 +89,7 @@ exprt::operandst build_function_environment(
9089

9190
// record as an input
9291
input.op0()=address_of_exprt(
93-
index_exprt(string_constantt(base_name), gen_zero(index_type())));
92+
index_exprt(string_constantt(base_name), from_integer(0, index_type())));
9493
input.op1()=symbol_expr;
9594
input.add_source_location()=p.source_location();
9695

@@ -131,9 +130,11 @@ void record_function_outputs(
131130

132131
const symbolt &return_symbol=symbol_table.lookup("return'");
133132

134-
output.op0()=address_of_exprt(
135-
index_exprt(string_constantt(return_symbol.base_name),
136-
gen_zero(index_type())));
133+
output.op0()=
134+
address_of_exprt(
135+
index_exprt(
136+
string_constantt(return_symbol.base_name),
137+
from_integer(0, index_type())));
137138

138139
output.op1()=return_symbol.symbol_expr();
139140
output.add_source_location()=function.location;
@@ -158,9 +159,11 @@ void record_function_outputs(
158159
codet output(ID_output);
159160
output.operands().resize(2);
160161

161-
output.op0()=address_of_exprt(
162-
index_exprt(string_constantt(symbol.base_name),
163-
gen_zero(index_type())));
162+
output.op0()=
163+
address_of_exprt(
164+
index_exprt(
165+
string_constantt(symbol.base_name),
166+
from_integer(0, index_type())));
164167
output.op1()=symbol.symbol_expr();
165168
output.add_source_location()=p.source_location();
166169

@@ -350,7 +353,7 @@ bool ansi_c_entry_point(
350353
codet input(ID_input);
351354
input.operands().resize(2);
352355
input.op0()=address_of_exprt(
353-
index_exprt(string_constantt("argc"), gen_zero(index_type())));
356+
index_exprt(string_constantt("argc"), from_integer(0, index_type())));
354357
input.op1()=argc_symbol.symbol_expr();
355358
init_code.move_to_operands(input);
356359
}
@@ -392,7 +395,7 @@ bool ansi_c_entry_point(
392395
zero_string.type().subtype()=char_type();
393396
zero_string.type().set(ID_size, "infinity");
394397
exprt index(ID_index, char_type());
395-
index.copy_to_operands(zero_string, gen_zero(uint_type()));
398+
index.copy_to_operands(zero_string, from_integer(0, uint_type()));
396399
exprt address_of("address_of", pointer_typet());
397400
address_of.type().subtype()=char_type();
398401
address_of.copy_to_operands(index);
@@ -470,7 +473,7 @@ bool ansi_c_entry_point(
470473
exprt index_expr(ID_index, arg1.type().subtype());
471474
index_expr.copy_to_operands(
472475
argv_symbol.symbol_expr(),
473-
gen_zero(index_type()));
476+
from_integer(0, index_type()));
474477

475478
// disable bounds check on that one
476479
index_expr.set("bounds_check", false);
@@ -489,7 +492,7 @@ bool ansi_c_entry_point(
489492

490493
exprt index_expr(ID_index, arg2.type().subtype());
491494
index_expr.copy_to_operands(
492-
envp_symbol.symbol_expr(), gen_zero(index_type()));
495+
envp_symbol.symbol_expr(), from_integer(0, index_type()));
493496

494497
op2=exprt(ID_address_of, arg2.type());
495498
op2.move_to_operands(index_expr);

‎src/ansi-c/ansi_c_language.cpp

-1
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@ Author: Daniel Kroening, [email protected]
1010
#include <sstream>
1111
#include <fstream>
1212

13-
#include <util/expr_util.h>
1413
#include <util/config.h>
1514
#include <util/get_base_name.h>
1615

‎src/ansi-c/c_typecast.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
1010

1111
#include <cassert>
1212

13+
#include <util/arith_tools.h>
1314
#include <util/config.h>
1415
#include <util/expr_util.h>
1516
#include <util/std_expr.h>
@@ -853,7 +854,7 @@ void c_typecastt::do_typecast(exprt &expr, const typet &dest_type)
853854
{
854855
index_exprt index;
855856
index.array()=expr;
856-
index.index()=gen_zero(index_type());
857+
index.index()=from_integer(0, index_type());
857858
index.type()=src_type.subtype();
858859
expr=address_of_exprt(index);
859860
if(ns.follow(expr.type())!=ns.follow(dest_type))

‎src/ansi-c/c_typecheck_argc_argv.cpp

-1
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@ Author: Daniel Kroening, [email protected]
77
\*******************************************************************/
88

99
#include <util/arith_tools.h>
10-
#include <util/expr_util.h>
1110

1211
#include "c_typecheck_base.h"
1312

‎src/ansi-c/c_typecheck_expr.cpp

+4-5
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
1111
#include <util/arith_tools.h>
1212
#include <util/config.h>
1313
#include <util/std_types.h>
14-
#include <util/expr_util.h>
1514
#include <util/prefix.h>
1615
#include <util/cprover_prefix.h>
1716
#include <util/simplify_expr.h>
@@ -100,7 +99,7 @@ void c_typecheck_baset::add_rounding_mode(exprt &expr)
10099
else
101100
assert(false);
102101

103-
expr.op2()=gen_zero(unsigned_int_type());
102+
expr.op2()=from_integer(0, unsigned_int_type());
104103
}
105104
}
106105
}
@@ -604,7 +603,7 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr)
604603

605604
exprt &member=static_cast<exprt &>(expr.add(ID_designator));
606605

607-
exprt result=gen_zero(size_type());
606+
exprt result=from_integer(0, size_type());
608607

609608
forall_operands(m_it, member)
610609
{
@@ -1286,7 +1285,7 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
12861285
{
12871286
index_exprt index;
12881287
index.array()=op;
1289-
index.index()=gen_zero(index_type());
1288+
index.index()=from_integer(0, index_type());
12901289
index.type()=op_type.subtype();
12911290
op=address_of_exprt(index);
12921291
}
@@ -2031,7 +2030,7 @@ void c_typecheck_baset::typecheck_expr_dereference(exprt &expr)
20312030
// *a is the same as a[0]
20322031
expr.id(ID_index);
20332032
expr.type()=op_type.subtype();
2034-
expr.copy_to_operands(gen_zero(index_type()));
2033+
expr.copy_to_operands(from_integer(0, index_type()));
20352034
assert(expr.operands().size()==2);
20362035
}
20372036
else if(op_type.id()==ID_pointer)

0 commit comments

Comments
 (0)