diff options
author | Andres Notzli <andres.noetzli@gmail.com> | 2017-03-27 11:40:45 +0200 |
---|---|---|
committer | Andres Notzli <andres.noetzli@gmail.com> | 2017-03-27 12:58:22 +0200 |
commit | f5954a66ac3255fe140049e47a7b56a6fab459b3 (patch) | |
tree | 8424cfc0c54d292d4a3de93c019e4982705ac48b /src/theory | |
parent | 0be62eeea95eaf27913e792c17dd79afb96b16cb (diff) |
Remove throw qualifiers in type enumerators
This addresses Coverity issues:
- 1172154
- 1172156
- 1172157
- 1172158
- 1172159
- 1379612
- 1379612
- 1421430
- 1172166
- 1172144
- 1362709
- 1362696
- 1172145
- 1172147
- 1172148
- 1379610
- 1362772
- 1362676
- 1362704
- 1362749
- 1362876
- 1362843
- 1362837
- 1362881
- 1172223
- 1172155
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arrays/type_enumerator.h | 6 | ||||
-rw-r--r-- | src/theory/booleans/type_enumerator.h | 2 | ||||
-rw-r--r-- | src/theory/builtin/type_enumerator.h | 4 | ||||
-rw-r--r-- | src/theory/bv/type_enumerator.h | 4 | ||||
-rw-r--r-- | src/theory/datatypes/type_enumerator.h | 10 | ||||
-rw-r--r-- | src/theory/strings/type_enumerator.h | 4 | ||||
-rw-r--r-- | src/theory/type_enumerator.h | 4 |
7 files changed, 17 insertions, 17 deletions
diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h index 0208fe52d..25a8ca3f2 100644 --- a/src/theory/arrays/type_enumerator.h +++ b/src/theory/arrays/type_enumerator.h @@ -41,7 +41,7 @@ class ArrayEnumerator : public TypeEnumeratorBase<ArrayEnumerator> { public: - ArrayEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) : + ArrayEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) : TypeEnumeratorBase<ArrayEnumerator>(type), d_tep(tep), d_index(type.getArrayIndexType(), tep), @@ -87,7 +87,7 @@ public: } } - Node operator*() throw(NoMoreValuesException) { + Node operator*() { if (d_finished) { throw NoMoreValuesException(getType()); } @@ -101,7 +101,7 @@ public: return n; } - ArrayEnumerator& operator++() throw() { + ArrayEnumerator& operator++() { Trace("array-type-enum") << "operator++ called, **this = " << **this << std::endl; if (d_finished) { diff --git a/src/theory/booleans/type_enumerator.h b/src/theory/booleans/type_enumerator.h index 3949d15d5..e91f47317 100644 --- a/src/theory/booleans/type_enumerator.h +++ b/src/theory/booleans/type_enumerator.h @@ -39,7 +39,7 @@ public: type.getConst<TypeConstant>() == BOOLEAN_TYPE); } - Node operator*() throw(NoMoreValuesException) { + Node operator*() { switch(d_value) { case FALSE: return NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h index 3840bb3b1..6ee540004 100644 --- a/src/theory/builtin/type_enumerator.h +++ b/src/theory/builtin/type_enumerator.h @@ -35,7 +35,7 @@ class UninterpretedSortEnumerator : public TypeEnumeratorBase<UninterpretedSortE Integer d_fixed_bound; public: - UninterpretedSortEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) : + UninterpretedSortEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) : TypeEnumeratorBase<UninterpretedSortEnumerator>(type), d_count(0) { Assert(type.getKind() == kind::SORT_TYPE); @@ -53,7 +53,7 @@ public: } } - Node operator*() throw(NoMoreValuesException) { + Node operator*() { if(isFinished()) { throw NoMoreValuesException(getType()); } diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h index 39f1e87f6..3c984def8 100644 --- a/src/theory/bv/type_enumerator.h +++ b/src/theory/bv/type_enumerator.h @@ -35,13 +35,13 @@ class BitVectorEnumerator : public TypeEnumeratorBase<BitVectorEnumerator> { public: - BitVectorEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw(AssertionException) : + BitVectorEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) : TypeEnumeratorBase<BitVectorEnumerator>(type), d_size(type.getBitVectorSize()), d_bits(0) { } - Node operator*() throw(NoMoreValuesException) { + Node operator*() { if(d_bits != d_bits.modByPow2(d_size)) { throw NoMoreValuesException(getType()); } diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 83c938299..5889090aa 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -81,7 +81,7 @@ class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> { void init(); public: - DatatypesEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw() : + DatatypesEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) : TypeEnumeratorBase<DatatypesEnumerator>(type), d_tep(tep), d_datatype(DatatypeType(type.toType()).getDatatype()), @@ -89,7 +89,7 @@ public: d_child_enum = false; init(); } - DatatypesEnumerator(TypeNode type, bool childEnum, TypeEnumeratorProperties * tep = NULL) throw() : + DatatypesEnumerator(TypeNode type, bool childEnum, TypeEnumeratorProperties * tep = NULL) : TypeEnumeratorBase<DatatypesEnumerator>(type), d_tep(tep), d_datatype(DatatypeType(type.toType()).getDatatype()), @@ -97,7 +97,7 @@ public: d_child_enum = childEnum; init(); } - DatatypesEnumerator(const DatatypesEnumerator& de) throw() : + DatatypesEnumerator(const DatatypesEnumerator& de) : TypeEnumeratorBase<DatatypesEnumerator>(de.getType()), d_tep(de.d_tep), d_datatype(de.d_datatype), @@ -130,7 +130,7 @@ public: virtual ~DatatypesEnumerator() throw() { } - Node operator*() throw(NoMoreValuesException) { + Node operator*() { Debug("dt-enum-debug") << ": get term " << this << std::endl; if(d_ctor < d_has_debruijn + d_datatype.getNumConstructors()) { return getCurrentTerm( d_ctor ); @@ -139,7 +139,7 @@ public: } } - DatatypesEnumerator& operator++() throw() { + DatatypesEnumerator& operator++() { Debug("dt-enum-debug") << ": increment " << this << std::endl; unsigned prevSize = d_size_limit; while(d_ctor < d_has_debruijn+d_datatype.getNumConstructors()) { diff --git a/src/theory/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h index 1fe3d79f6..22dc903ab 100644 --- a/src/theory/strings/type_enumerator.h +++ b/src/theory/strings/type_enumerator.h @@ -50,7 +50,7 @@ public: Node operator*() throw() { return d_curr; } - StringEnumerator& operator++() throw() { + StringEnumerator& operator++() { bool changed = false; do{ for(unsigned i=0; i<d_data.size(); ++i) { @@ -99,7 +99,7 @@ public: return d_curr; } - StringEnumeratorLength& operator++() throw() { + StringEnumeratorLength& operator++() { bool changed = false; for(unsigned i=0; i<d_data.size(); ++i) { if( d_data[i] + 1 < d_cardinality ) { diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h index bcd7e695f..258bf6a3a 100644 --- a/src/theory/type_enumerator.h +++ b/src/theory/type_enumerator.h @@ -49,10 +49,10 @@ public: virtual bool isFinished() throw() = 0; /** Get the current constant of this type (throws if no such constant exists) */ - virtual Node operator*() throw(NoMoreValuesException) = 0; + virtual Node operator*() = 0; /** Increment the pointer to the next available constant */ - virtual TypeEnumeratorInterface& operator++() throw() = 0; + virtual TypeEnumeratorInterface& operator++() = 0; /** Clone this enumerator */ virtual TypeEnumeratorInterface* clone() const = 0; |