summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2018-05-24 13:01:33 -0700
committerGitHub <noreply@github.com>2018-05-24 13:01:33 -0700
commit83b4e2ba719ddc410c125a7ef7ff49f39dc2a599 (patch)
tree329f0a3f91e9ba44368a9f435bd2c2b17f75c1e9
parentd12c7561624de9a2ae6cf10a7fa2bd9c97b2bc5e (diff)
Fix compiler warnings (#1959)
-rw-r--r--src/expr/expr_template.h4
-rw-r--r--src/theory/fp/kinds2
-rw-r--r--src/theory/fp/theory_fp.h4
-rw-r--r--src/theory/fp/theory_fp_rewriter.cpp2
-rw-r--r--src/theory/type_enumerator_template.cpp2
5 files changed, 7 insertions, 7 deletions
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 3a27fca25..f8601af15 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -43,7 +43,7 @@ ${includes}
// compiler directs the user to the template file instead of the
// generated one. We don't want the user to modify the generated one,
// since it'll get overwritten on a later build.
-#line 44 "${template}"
+#line 47 "${template}"
namespace CVC4 {
@@ -609,7 +609,7 @@ private:
${getConst_instantiations}
-#line 549 "${template}"
+#line 613 "${template}"
inline size_t ExprHashFunction::operator()(CVC4::Expr e) const {
return (size_t) e.getId();
diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds
index b1170b42c..49ed92dee 100644
--- a/src/theory/fp/kinds
+++ b/src/theory/fp/kinds
@@ -8,7 +8,7 @@ theory THEORY_FP ::CVC4::theory::fp::TheoryFp "theory/fp/theory_fp.h"
typechecker "theory/fp/theory_fp_type_rules.h"
rewriter ::CVC4::theory::fp::TheoryFpRewriter "theory/fp/theory_fp_rewriter.h"
-properties check propagate
+properties check
# Theory content goes here.
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 6234ab8ad..832fc6442 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -43,11 +43,11 @@ class TheoryFp : public Theory {
void preRegisterTerm(TNode node) override;
void addSharedTerm(TNode node) override;
- Node ppRewrite(TNode node);
+ Node ppRewrite(TNode node) override;
void check(Effort) override;
- bool needsCheckLastEffort() { return true; }
+ bool needsCheckLastEffort() override { return true; }
Node getModelValue(TNode var) override;
bool collectModelInfo(TheoryModel* m) override;
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index f502ad547..496066ebc 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -862,12 +862,12 @@ namespace constantFold {
{
Assert(node.getKind() == kind::ROUNDINGMODE_BITBLAST);
- RoundingMode arg0(node[0].getConst<RoundingMode>());
BitVector value;
#ifdef CVC4_USE_SYMFPU
/* \todo fix the numbering of rounding modes so this doesn't need
* to call symfpu at all and remove the dependency on fp_converter.h #1915 */
+ RoundingMode arg0(node[0].getConst<RoundingMode>());
switch (arg0)
{
case roundNearestTiesToEven:
diff --git a/src/theory/type_enumerator_template.cpp b/src/theory/type_enumerator_template.cpp
index 91ae3e1d6..3daf449fb 100644
--- a/src/theory/type_enumerator_template.cpp
+++ b/src/theory/type_enumerator_template.cpp
@@ -45,7 +45,7 @@ ${mk_type_enumerator_type_constant_cases}
}
Unreachable();
${mk_type_enumerator_cases}
-#line 47 "${template}"
+#line 49 "${template}"
default:
{
stringstream ss;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback