Skip to content

Commit 26fb850

Browse files
reukreuk
committed
Replace macros with exception types
1 parent 822df45 commit 26fb850

13 files changed

+66
-36
lines changed

‎src/analyses/invariant_set.cpp‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
1313

1414
#include <iostream>
1515

16+
#include <util/base_exceptions.h>
1617
#include <util/symbol_table.h>
1718
#include <util/namespace.h>
1819
#include <util/arith_tools.h>
@@ -315,8 +316,8 @@ void invariant_sett::output(
315316
return;
316317
}
317318

318-
INVARIANT(
319-
object_store!=nullptr, nullptr_exceptiont("Object store is null"));
319+
INVARIANT_STRUCTURED(
320+
object_store!=nullptr, nullptr_exceptiont, "Object store is null");
320321

321322
for(unsigned i=0; i<eq_set.size(); i++)
322323
if(eq_set.is_root(i) &&

‎src/analyses/invariant_set.h‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com
2222

2323
#include "interval_template.h"
2424

25-
#define nullptr_exceptiont(str) str
26-
2725
class inv_object_storet
2826
{
2927
public:

‎src/analyses/reaching_definitions.cpp‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -51,9 +51,10 @@ void rd_range_domaint::transform(
5151
{
5252
reaching_definitions_analysist *rd=
5353
dynamic_cast<reaching_definitions_analysist*>(&ai);
54-
INVARIANT(
54+
INVARIANT_STRUCTURED(
5555
rd!=nullptr,
56-
bad_cast_exceptiont("ai has type reaching_definitions_analysist"));
56+
bad_cast_exceptiont,
57+
"ai has type reaching_definitions_analysist");
5758

5859
assert(bv_container);
5960

@@ -300,9 +301,10 @@ void rd_range_domaint::transform_assign(
300301
const symbolt *symbol_ptr;
301302
if(ns.lookup(identifier, symbol_ptr))
302303
continue;
303-
INVARIANT(
304+
INVARIANT_STRUCTURED(
304305
symbol_ptr!=nullptr,
305-
nullptr_exceptiont("Symbol is in symbol table"));
306+
nullptr_exceptiont,
307+
"Symbol is in symbol table");
306308

307309
const range_domaint &ranges=rw_set.get_ranges(it);
308310

‎src/analyses/reaching_definitions.h‎

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ Date: February 2013
1616
#ifndef CPROVER_ANALYSES_REACHING_DEFINITIONS_H
1717
#define CPROVER_ANALYSES_REACHING_DEFINITIONS_H
1818

19+
#include <util/base_exceptions.h>
1920
#include <util/threeval.h>
2021

2122
#include "ai.h"
@@ -26,9 +27,6 @@ class is_threadedt;
2627
class dirtyt;
2728
class reaching_definitions_analysist;
2829

29-
#define bad_cast_exceptiont(str) str
30-
#define nullptr_exceptiont(str) str
31-
3230
// requirement: V has a member "identifier" of type irep_idt
3331
template<typename V>
3432
class sparse_bitvector_analysist
@@ -262,9 +260,10 @@ class reaching_definitions_analysist:
262260
statet &s=concurrency_aware_ait<rd_range_domaint>::get_state(l);
263261

264262
rd_range_domaint *rd_state=dynamic_cast<rd_range_domaint*>(&s);
265-
INVARIANT(
263+
INVARIANT_STRUCTURED(
266264
rd_state!=nullptr,
267-
bad_cast_exceptiont("rd_state has type rd_range_domaint"));
265+
bad_cast_exceptiont,
266+
"rd_state has type rd_range_domaint");
268267

269268
rd_state->set_bitvector_container(*this);
270269

‎src/cpp/cpp_instantiate_template.cpp‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
1212
#include "cpp_typecheck.h"
1313

1414
#include <util/arith_tools.h>
15+
#include <util/base_exceptions.h>
1516
#include <util/simplify_expr.h>
1617

1718
#include <util/c_types.h>
@@ -130,8 +131,8 @@ const symbolt &cpp_typecheckt::class_template_symbol(
130131
cpp_scopet *template_scope=
131132
static_cast<cpp_scopet *>(cpp_scopes.id_map[template_symbol.name]);
132133

133-
INVARIANT(
134-
template_scope!=nullptr, nullptr_exceptiont("template_scope is null"));
134+
INVARIANT_STRUCTURED(
135+
template_scope!=nullptr, nullptr_exceptiont, "template_scope is null");
135136

136137
irep_idt identifier=
137138
id2string(template_scope->prefix)+
@@ -285,8 +286,8 @@ const symbolt &cpp_typecheckt::instantiate_template(
285286
throw 0;
286287
}
287288

288-
INVARIANT(
289-
template_scope!=nullptr, nullptr_exceptiont("template_scope is null"));
289+
INVARIANT_STRUCTURED(
290+
template_scope!=nullptr, nullptr_exceptiont, "template_scope is null");
290291

291292
// produce new declaration
292293
cpp_declarationt new_decl=to_cpp_declaration(template_symbol.type);

‎src/cpp/cpp_typecheck.h‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,8 +30,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
3030
#include "cpp_template_type.h"
3131
#include "cpp_util.h"
3232

33-
#define nullptr_exceptiont(str) str
34-
3533
bool cpp_typecheck(
3634
cpp_parse_treet &cpp_parse_tree,
3735
symbol_tablet &symbol_table,

‎src/cpp/cpp_typecheck_template.cpp‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
1111

1212
#include "cpp_typecheck.h"
1313

14+
#include <util/base_exceptions.h>
1415
#include <util/simplify_expr.h>
1516

1617
#include "cpp_type2name.h"
@@ -910,8 +911,8 @@ cpp_template_args_tct cpp_typecheckt::typecheck_template_args(
910911
// these need to be typechecked in the scope of the template,
911912
// not in the current scope!
912913
cpp_idt *template_scope=cpp_scopes.id_map[template_symbol.name];
913-
INVARIANT(
914-
template_scope!=nullptr, nullptr_exceptiont("template_scope is null"));
914+
INVARIANT_STRUCTURED(
915+
template_scope!=nullptr, nullptr_exceptiont, "template_scope is null");
915916
cpp_scopes.go_to(*template_scope);
916917
}
917918

@@ -961,9 +962,10 @@ cpp_template_args_tct cpp_typecheckt::typecheck_template_args(
961962
{
962963
cpp_save_scopet cpp_saved_scope(cpp_scopes);
963964
cpp_idt *template_scope=cpp_scopes.id_map[template_symbol.name];
964-
INVARIANT(
965+
INVARIANT_STRUCTURED(
965966
template_scope!=nullptr,
966-
nullptr_exceptiont("template_scope is null"));
967+
nullptr_exceptiont,
968+
"template_scope is null");
967969
cpp_scopes.go_to(*template_scope);
968970
typecheck_type(type);
969971
}

‎src/goto-symex/goto_symex_state.cpp‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
1515
#include <cassert>
1616
#include <iostream>
1717

18+
#include <util/base_exceptions.h>
1819
#include <util/std_expr.h>
1920
#include <util/prefix.h>
2021

@@ -541,7 +542,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
541542
return false;
542543

543544
// is it a shared object?
544-
INVARIANT(dirty!=nullptr, nullptr_exceptiont("dirty is null"));
545+
INVARIANT_STRUCTURED(dirty!=nullptr, nullptr_exceptiont, "dirty is null");
545546
const irep_idt &obj_identifier=expr.get_object_name();
546547
if(obj_identifier=="goto_symex::\\guard" ||
547548
(!ns.lookup(obj_identifier).is_shared() &&
@@ -666,7 +667,8 @@ bool goto_symex_statet::l2_thread_read_encoding(
666667
expr=ssa_l1;
667668

668669
// and record that
669-
INVARIANT(symex_target!=nullptr, nullptr_exceptiont("symex_target is null"));
670+
INVARIANT_STRUCTURED(
671+
symex_target!=nullptr, nullptr_exceptiont, "symex_target is null");
670672
symex_target->shared_read(
671673
guard.as_expr(),
672674
expr,
@@ -685,7 +687,7 @@ bool goto_symex_statet::l2_thread_write_encoding(
685687
return false;
686688

687689
// is it a shared object?
688-
INVARIANT(dirty!=nullptr, nullptr_exceptiont("dirty is null"));
690+
INVARIANT_STRUCTURED(dirty!=nullptr, nullptr_exceptiont, "dirty is null");
689691
const irep_idt &obj_identifier=expr.get_object_name();
690692
if(obj_identifier=="goto_symex::\\guard" ||
691693
(!ns.lookup(obj_identifier).is_shared() &&

‎src/goto-symex/goto_symex_state.h‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -26,8 +26,6 @@ Author: Daniel Kroening, kroening@kroening.com
2626

2727
class dirtyt;
2828

29-
#define nullptr_exceptiont(str) str
30-
3129
// central data structure: state
3230
class goto_symex_statet
3331
{

‎src/path-symex/path_symex_history.h‎

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -15,14 +15,13 @@ Author: Daniel Kroening, kroening@kroening.com
1515
#include <cassert>
1616
#include <limits>
1717

18+
#include <util/base_exceptions.h>
1819
#include <util/std_expr.h>
1920

2021
#include "loc_ref.h"
2122

2223
class path_symex_stept;
2324

24-
#define nullptr_exceptiont(str) str
25-
2625
// This is a reference to a path_symex_stept,
2726
// and is really cheap to copy. These references are stable,
2827
// even though the underlying vector is not.
@@ -48,7 +47,8 @@ class path_symex_step_reft
4847

4948
path_symex_historyt &get_history() const
5049
{
51-
INVARIANT(history!=nullptr, nullptr_exceptiont("history is null"));
50+
INVARIANT_STRUCTURED(
51+
history!=nullptr, nullptr_exceptiont, "history is null");
5252
return *history;
5353
}
5454

@@ -156,7 +156,8 @@ class path_symex_historyt
156156

157157
inline void path_symex_step_reft::generate_successor()
158158
{
159-
INVARIANT(history!=nullptr, nullptr_exceptiont("history is null"));
159+
INVARIANT_STRUCTURED(
160+
history!=nullptr, nullptr_exceptiont, "history is null");
160161
path_symex_step_reft old=*this;
161162
index=history->step_container.size();
162163
history->step_container.push_back(path_symex_stept());
@@ -171,7 +172,8 @@ inline path_symex_step_reft &path_symex_step_reft::operator--()
171172

172173
inline path_symex_stept &path_symex_step_reft::get() const
173174
{
174-
INVARIANT(history!=nullptr, nullptr_exceptiont("history is null"));
175+
INVARIANT_STRUCTURED(
176+
history!=nullptr, nullptr_exceptiont, "history is null");
175177
assert(!is_nil());
176178
return history->step_container[index];
177179
}

0 commit comments

Comments
 (0)