From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 1 Oct 2010 22:25:01 +0000 (+0000)
Subject: re-add no-deprecated to C sources; update some file-level documentation; first look... 
X-Git-Tag: cvc5-1.0.0~8837
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=02c2038dca9ce3e09cac66ed3bd6f8e2832ff74b;p=cvc5.git

re-add no-deprecated to C sources; update some file-level documentation; first look at cdvector for code review
---

diff --git a/configure.ac b/configure.ac
index 249122d25..d2033ac1f 100644
--- a/configure.ac
+++ b/configure.ac
@@ -705,7 +705,7 @@ AC_DEFINE_UNQUOTED(CVC4_RELEASE_STRING, ["${CVC4_RELEASE_STRING}"], [Full releas
 
 CPPFLAGS="${CPPFLAGS:+$CPPFLAGS }$CVC4CPPFLAGS"
 CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated"
-CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -fexceptions"
+CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
 LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
 
 AC_SUBST(FLAG_VISIBILITY_HIDDEN)
diff --git a/src/context/cdvector.h b/src/context/cdvector.h
index cf88e2ce6..0076d509f 100644
--- a/src/context/cdvector.h
+++ b/src/context/cdvector.h
@@ -1,4 +1,21 @@
-
+/*********************                                                        */
+/*! \file cdvector.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** 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
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
 
 #include "cvc4_private.h"
 
@@ -14,35 +31,26 @@ namespace CVC4 {
 namespace context {
 
 template <class T>
-struct UpdatableElement{
+struct UpdatableElement {
 public:
   T d_data;
   int d_contextLevelOfLastUpdate;
 
   UpdatableElement(const T& data) :
     d_data(data),
-    d_contextLevelOfLastUpdate(0){
+    d_contextLevelOfLastUpdate(0) {
   }
-
-  // UpdatableElement() :
-  //   d_data(),
-  //   d_contextLevelOfLastUpdate(0){
-  // }
-};
+};/* struct UpdatableElement<T> */
 
 template <class T>
-struct HistoryElement{
+struct HistoryElement {
 public:
   UpdatableElement<T> d_cached;
   unsigned d_index;
   HistoryElement(const UpdatableElement<T>& cache, unsigned index) :
-    d_cached(cache), d_index(index)
-  {}
-
-  // HistoryElement() :
-  //   d_cached(), d_index(0)
-  // {}
-};
+    d_cached(cache), d_index(index) {
+  }
+};/* struct HistoryElement<T> */
 
 
 /**
@@ -65,7 +73,6 @@ private:
 
   CDO<unsigned> d_historySize;
 
-
 private:
   void restoreConsistency() {
     Assert(d_history.size() >= d_historySize.get());
@@ -76,12 +83,12 @@ private:
     }
   }
 
-  bool isConsistent() const{
+  bool isConsistent() const {
     return d_history.size() == d_historySize.get();
   }
 
   void makeConsistent() {
-    if(!isConsistent()){
+    if(!isConsistent()) {
       restoreConsistency();
     }
     Assert(isConsistent());
@@ -92,7 +99,7 @@ public:
     d_context(c),
     d_current(callDestructor),
     d_history(callDestructor),
-    d_historySize(c,0){
+    d_historySize(c, 0) {
   }
 
   unsigned size() const {
@@ -117,7 +124,7 @@ public:
   /**
    * Access to the ith item in the list.
    */
-  const T& operator[](unsigned i){
+  const T& operator[](unsigned i) {
     return get(i);
   }
 
@@ -127,11 +134,11 @@ public:
     return d_current[i].d_data;
   }
 
-  void set(unsigned index, const T& data){
+  void set(unsigned index, const T& data) {
     Assert(index < size(), "index out of bounds in CDVector::set()");
     makeConsistent();
 
-    if(d_current[index].d_contextLevelOfLastUpdate == d_context->getLevel() ){
+    if(d_current[index].d_contextLevelOfLastUpdate == d_context->getLevel()) {
       d_current[index].d_data = data;
     }else{
       d_history.push_back(HistoryElement<T>(d_current[index], index));
@@ -142,7 +149,7 @@ public:
     }
   }
 
-};/* class CDVector */
+};/* class CDVector<T> */
 
 }/* CVC4::context namespace */
 }/* CVC4 namespace */
diff --git a/src/context/context.cpp b/src/context/context.cpp
index 5d8e88db0..9b40e9780 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: barrett
- ** Minor contributors (to current version): 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
diff --git a/test/unit/context/cdvector_black.h b/test/unit/context/cdvector_black.h
index 8deac3fb3..3e9a7b87b 100644
--- a/test/unit/context/cdvector_black.h
+++ b/test/unit/context/cdvector_black.h
@@ -1,3 +1,21 @@
+/*********************                                                        */
+/*! \file cdvector_black.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** 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
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
 
 #include <cxxtest/TestSuite.h>