From: Tim King <taking@cs.nyu.edu>
Date: Wed, 7 Apr 2010 22:14:10 +0000 (+0000)
Subject: This update contains more black-box tests as part of the attributes code review.... 
X-Git-Tag: cvc5-1.0.0~9123
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=de2b6c4ee9c2ecad88bddd0a60f10e94d6f8c71f;p=cvc5.git

This update contains more black-box tests as part of the attributes code review. I have confirmed by eyeball that every executable line of attributes.h is now getting hit in coverage testing. This can only be eyeballed at the moment because of templates. (There is 1 function that is not being touched, something included from NodeTemplate: _ZNK4CVC44expr4attr16AttributeManager12getAttributeINS0_9AttributeINS_6theory15RewriteCacheTagENS_12NodeTemplateILb0EEENS1_19NullCleanupStrategyELb0EEEEENT_10value_typeEPNS0_9NodeValueERKSB_)
---

diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index e87c8d708..92aacf509 100644
--- a/test/unit/expr/attribute_black.h
+++ b/test/unit/expr/attribute_black.h
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /** attribute_black.h
- ** Original author: dejan
+ ** Original author: taking
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters, cconway
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -10,7 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** Black box testing of CVC4::Node.
+ ** Black box testing of CVC4::Attribute.
  **/
 
 #include <cxxtest/TestSuite.h>
@@ -82,6 +82,190 @@ public:
     delete node;
   }
 
+  struct PrimitiveIntAttributeId {};
+  struct CDPrimitiveIntAttributeId {};
+
+  typedef expr::Attribute<PrimitiveIntAttributeId,uint64_t> PrimitiveIntAttribute;
+  typedef expr::CDAttribute<CDPrimitiveIntAttributeId,uint64_t> CDPrimitiveIntAttribute;
+  void testInts(){
+    Type* booleanType = d_nodeManager->booleanType();
+    Node* node = new Node(d_nodeManager->mkVar(booleanType));
+    const uint64_t val = 63489;
+    uint64_t data0;
+    uint64_t data1;
+
+    PrimitiveIntAttribute attr;
+    TS_ASSERT(!node->getAttribute(attr, data0));
+    node->setAttribute(attr, val);
+    TS_ASSERT(node->getAttribute(attr, data1));
+    TS_ASSERT_EQUALS(data1, val);
+
+    uint64_t data2;
+    uint64_t data3;
+    CDPrimitiveIntAttribute cdattr;
+    TS_ASSERT(!node->getAttribute(cdattr, data2));
+    node->setAttribute(cdattr, val);
+    TS_ASSERT(node->getAttribute(cdattr, data3));
+    TS_ASSERT_EQUALS(data3, val);
+    delete node;
+  }
+
+  struct TNodeAttributeId {};
+  struct CDTNodeAttributeId {};
+
+  typedef expr::Attribute<TNodeAttributeId, TNode> TNodeAttribute;
+  typedef expr::CDAttribute<CDTNodeAttributeId, TNode> CDTNodeAttribute;
+  void testTNodes(){
+    Type* booleanType = d_nodeManager->booleanType();
+    Node* node = new Node(d_nodeManager->mkVar(booleanType));
+
+    Node val(d_nodeManager->mkVar(booleanType));
+    TNode data0;
+    TNode data1;
+
+    TNodeAttribute attr;
+    TS_ASSERT(!node->getAttribute(attr, data0));
+    node->setAttribute(attr, val);
+    TS_ASSERT(node->getAttribute(attr, data1));
+    TS_ASSERT_EQUALS(data1, val);
+
+    TNode data2;
+    TNode data3;
+    CDTNodeAttribute cdattr;
+    TS_ASSERT(!node->getAttribute(cdattr, data2));
+    node->setAttribute(cdattr, val);
+    TS_ASSERT(node->getAttribute(cdattr, data3));
+    TS_ASSERT_EQUALS(data3, val);
+    delete node;
+  }
+
+  class Foo {
+    int blah;
+  public:
+    Foo(int b) : blah(b) {}
+  };
+
+  struct PtrAttributeId {};
+  struct CDPtrAttributeId {};
+
+  typedef expr::Attribute<PtrAttributeId, Foo*> PtrAttribute;
+  typedef expr::CDAttribute<CDPtrAttributeId, Foo*> CDPtrAttribute;
+  void testPtrs(){
+    Type* booleanType = d_nodeManager->booleanType();
+    Node* node = new Node(d_nodeManager->mkVar(booleanType));
+
+    Foo* val = new Foo(63489);
+    Foo* data0;
+    Foo* data1;
+
+    PtrAttribute attr;
+    TS_ASSERT(!node->getAttribute(attr, data0));
+    node->setAttribute(attr, val);
+    TS_ASSERT(node->getAttribute(attr, data1));
+    TS_ASSERT_EQUALS(data1, val);
+
+    Foo* data2;
+    Foo* data3;
+    CDPtrAttribute cdattr;
+    TS_ASSERT(!node->getAttribute(cdattr, data2));
+    node->setAttribute(cdattr, val);
+    TS_ASSERT(node->getAttribute(cdattr, data3));
+    TS_ASSERT_EQUALS(data3, val);
+    delete node;
+    delete val;
+  }
+
+
+  struct ConstPtrAttributeId {};
+  struct CDConstPtrAttributeId {};
+
+  typedef expr::Attribute<ConstPtrAttributeId, const Foo*> ConstPtrAttribute;
+  typedef expr::CDAttribute<CDConstPtrAttributeId, const Foo*> CDConstPtrAttribute;
+  void testConstPtrs(){
+    Type* booleanType = d_nodeManager->booleanType();
+    Node* node = new Node(d_nodeManager->mkVar(booleanType));
+
+    const Foo* val = new Foo(63489);
+    const Foo* data0;
+    const Foo* data1;
+
+    ConstPtrAttribute attr;
+    TS_ASSERT(!node->getAttribute(attr, data0));
+    node->setAttribute(attr, val);
+    TS_ASSERT(node->getAttribute(attr, data1));
+    TS_ASSERT_EQUALS(data1, val);
+
+    const Foo* data2;
+    const Foo* data3;
+    CDConstPtrAttribute cdattr;
+    TS_ASSERT(!node->getAttribute(cdattr, data2));
+    node->setAttribute(cdattr, val);
+    TS_ASSERT(node->getAttribute(cdattr, data3));
+    TS_ASSERT_EQUALS(data3, val);
+    delete node;
+    delete val;
+  }
+
+  struct StringAttributeId {};
+  struct CDStringAttributeId {};
+
+  typedef expr::Attribute<StringAttributeId, std::string> StringAttribute;
+  typedef expr::CDAttribute<CDStringAttributeId, std::string> CDStringAttribute;
+  void testStrings(){
+    Type* booleanType = d_nodeManager->booleanType();
+    Node* node = new Node(d_nodeManager->mkVar(booleanType));
+
+    std::string val("63489");
+    std::string data0;
+    std::string data1;
+
+    StringAttribute attr;
+    TS_ASSERT(!node->getAttribute(attr, data0));
+    node->setAttribute(attr, val);
+    TS_ASSERT(node->getAttribute(attr, data1));
+    TS_ASSERT_EQUALS(data1, val);
+
+    std::string data2;
+    std::string data3;
+    CDStringAttribute cdattr;
+    TS_ASSERT(!node->getAttribute(cdattr, data2));
+    node->setAttribute(cdattr, val);
+    TS_ASSERT(node->getAttribute(cdattr, data3));
+    TS_ASSERT_EQUALS(data3, val);
+    delete node;
+  }
+
+  struct BoolAttributeId {};
+  struct CDBoolAttributeId {};
+
+  typedef expr::Attribute<BoolAttributeId, bool> BoolAttribute;
+  typedef expr::CDAttribute<CDBoolAttributeId, bool> CDBoolAttribute;
+  void testBools(){
+    Type* booleanType = d_nodeManager->booleanType();
+    Node* node = new Node(d_nodeManager->mkVar(booleanType));
+
+    bool val = true;
+    bool data0;
+    bool data1;
+
+    BoolAttribute attr;
+    TS_ASSERT(node->getAttribute(attr, data0));
+    TS_ASSERT_EQUALS(false, data0);
+    node->setAttribute(attr, val);
+    TS_ASSERT(node->getAttribute(attr, data1));
+    TS_ASSERT_EQUALS(data1, val);
+
+    bool data2;
+    bool data3;
+    CDBoolAttribute cdattr;
+    TS_ASSERT(node->getAttribute(cdattr, data2));
+    TS_ASSERT_EQUALS(false, data2);
+    node->setAttribute(cdattr, val);
+    TS_ASSERT(node->getAttribute(cdattr, data3));
+    TS_ASSERT_EQUALS(data3, val);
+    delete node;
+  }
+
 };
 
 int AttributeBlack::MyData::count = 0;