avoid -I util

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@2384 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

src/goto-instrument/Makefile

@@ -26,7 +26,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../util/util$(LIBEXT) \
       ../solvers/solvers$(LIBEXT)
 
-INCLUDES= -I .. -I ../util
+INCLUDES= -I ..
 
 LIBS =
 

src/goto-instrument/accelerate/accelerate.h

@@ -1,9 +1,9 @@
+#include <util/namespace.h>
+
 #include <analyses/natural_loops.h>
 
 #include <goto-programs/goto_functions.h>
 
-#include <namespace.h>
-
 #include "path.h"
 
 class acceleratet {

src/goto-instrument/accelerate/finite_calculus.cpp

@@ -2,12 +2,12 @@
  * Routines for doing finite calculus.
  */
 
+#include <cassert>
+
+#include <util/replace_expr.h>
+
 #include "finite_calculus.h"
 
-#include <replace_expr.h>
-
-#include <assert.h>
-
 exprt indefinite_sum(const exprt &e, const exprt &x) {
   assert(!"indefinite_sum() not implemented");
 }

src/goto-instrument/accelerate/finite_calculus.h

@@ -1,7 +1,7 @@
 #ifndef FINITE_CALCULUS_H
 #define FINITE_CALCULUS_H
 
-#include <std_expr.h>
+#include <util/std_expr.h>
 
 /*
  * Convert a factorial power to an expression using conventional powers.

src/goto-instrument/accelerate/path.h

@@ -1,12 +1,12 @@
 #ifndef PATH_H
 #define PATH_H
 
-#include <goto-programs/goto_program.h>
-
-#include <std_expr.h>
-
 #include <list>
 
+#include <util/std_expr.h>
+
+#include <goto-programs/goto_program.h>
+
 using namespace std;
 
 class path_nodet {

src/goto-instrument/accelerate/polynomial.cpp

@@ -1,8 +1,8 @@
 #include <vector>
 
-#include <std_expr.h>
-#include <replace_expr.h>
-#include <arith_tools.h>
+#include <util/std_expr.h>
+#include <util/replace_expr.h>
+#include <util/arith_tools.h>
 
 #include <ansi-c/c_types.h>
 
@@ -11,13 +11,13 @@
 exprt polynomialt::to_expr() {
   exprt ret = nil_exprt();
 
-  for (vector<monomialt>::iterator m_it = monomials.begin();
+  for (std::vector<monomialt>::iterator m_it = monomials.begin();
        m_it != monomials.end();
        ++m_it)
   {
     exprt mon_expr = from_integer(m_it->coeff, signed_int_type());
 
-    for (vector<monomialt::termt>::iterator t_it = m_it->terms.begin();
+    for (std::vector<monomialt::termt>::iterator t_it = m_it->terms.begin();
          t_it != m_it->terms.end();
          ++t_it) {
       for (int i = 0; i < t_it->exp; i++) {
@@ -80,11 +80,12 @@ void polynomialt::from_expr(exprt &expr) {
     throw "Couldn't polynomialize";
   }
 }
+
 void polynomialt::substitute(substitutiont &substitution) {
-  for (vector<monomialt>::iterator m_it = monomials.begin();
+  for (std::vector<monomialt>::iterator m_it = monomials.begin();
        m_it != monomials.end();
        ++m_it) {
-    for (vector<monomialt::termt>::iterator t_it = m_it->terms.begin();
+    for (std::vector<monomialt::termt>::iterator t_it = m_it->terms.begin();
          t_it != m_it->terms.end();
          ++t_it) {
       if (substitution.find(t_it->var) != substitution.end()) {
@@ -99,8 +100,8 @@ void polynomialt::add(polynomialt &other) {
   //
   // Note: it'd be really interesting to try to verify this function
   // automatically.  I don't really know how you'd do it...
-  vector<monomialt>::iterator it, jt;
-  vector<monomialt> new_monomials;
+  std::vector<monomialt>::iterator it, jt;
+  std::vector<monomialt> new_monomials;
 
   it = monomials.begin();
   jt = other.monomials.begin();
@@ -159,21 +160,22 @@ void polynomialt::add(monomialt &monomial) {
 
 void polynomialt::mult(int scalar) {
   // Scalar multiplication.  Just multiply the coefficients of each monomial.
-  for (vector<monomialt>::iterator it = monomials.begin();
+  for (std::vector<monomialt>::iterator it = monomials.begin();
        it != monomials.end();
        ++it) {
     it->coeff *= scalar;
   }
 }
 
-void polynomialt::mult(polynomialt &other) {
-  vector<monomialt> my_monomials = monomials;
-  monomials = vector<monomialt>();
+void polynomialt::mult(polynomialt &other)
+{
+  std::vector<monomialt> my_monomials = monomials;
+  monomials = std::vector<monomialt>();
 
-  for (vector<monomialt>::iterator it = my_monomials.begin();
+  for (std::vector<monomialt>::iterator it = my_monomials.begin();
        it != my_monomials.end();
        ++it) {
-    for (vector<monomialt>::iterator jt = other.monomials.begin();
+    for (std::vector<monomialt>::iterator jt = other.monomials.begin();
          jt != other.monomials.end();
          ++jt) {
       monomialt product;
@@ -185,7 +187,7 @@ void polynomialt::mult(polynomialt &other) {
       }
 
       // Terms are sorted, so lockstep is fine again.
-      vector<monomialt::termt>::iterator t1, t2;
+      std::vector<monomialt::termt>::iterator t1, t2;
 
       t1 = it->terms.begin();
       t2 = jt->terms.begin();
@@ -235,7 +237,7 @@ void polynomialt::mult(polynomialt &other) {
 int monomialt::compare(monomialt &other) {
   // Using lexicographic ordering, for no particular reason other than it's easy
   // to implement...
-  vector<termt>::iterator it, jt;
+  std::vector<termt>::iterator it, jt;
 
   it = terms.begin();
   jt = other.terms.begin();
@@ -286,11 +288,11 @@ int polynomialt::max_degree(exprt &var) {
   // We want the degree of the highest degree monomial in which `var' appears.
   int maxd = 0;
 
-  for (vector<monomialt>::iterator it = monomials.begin();
+  for (std::vector<monomialt>::iterator it = monomials.begin();
        it != monomials.end();
        ++it) {
     if (it->contains(var)) {
-      maxd = max(maxd, it->degree());
+      maxd = std::max(maxd, it->degree());
     }
   }
 
@@ -308,7 +310,7 @@ int polynomialt::coeff(exprt &var) {
 
   monomialt m = p.monomials.front();
 
-  for (vector<monomialt>::iterator it = monomials.begin();
+  for (std::vector<monomialt>::iterator it = monomials.begin();
        it != monomials.end();
        ++it) {
     int res = m.compare(*it);
@@ -326,7 +328,7 @@ int polynomialt::coeff(exprt &var) {
 int monomialt::degree() {
   int deg = 0;
 
-  for (vector<termt>::iterator it = terms.begin();
+  for (std::vector<termt>::iterator it = terms.begin();
        it != terms.end();
        ++it) {
     deg += it->exp;
@@ -342,7 +344,7 @@ bool monomialt::contains(exprt &var) {
     return false;
   }
 
-  for (vector<termt>::iterator it = terms.begin();
+  for (std::vector<termt>::iterator it = terms.begin();
        it != terms.end();
        ++it) {
     if (it->var == var) {

src/goto-instrument/accelerate/polynomial.h

@@ -3,19 +3,18 @@
 
 #include <vector>
 
-#include <expr.h>
+#include <util/expr.h>
 
-using namespace std;
-
-class monomialt {
- public:
+class monomialt
+{
+public:
   typedef struct term {
     exprt var;
     unsigned int exp;   // This means exponent, not expression.
   } termt;
 
   // Invariant: this vector is sorted lexicographically w.r.t. the variable.
-  vector<termt> terms;
+  std::vector<termt> terms;
   int coeff;
 
   int compare(monomialt &other);
@@ -24,13 +23,14 @@ class monomialt {
   bool contains(exprt &var);
 };
 
-typedef map<exprt, exprt> substitutiont;
+typedef std::map<exprt, exprt> substitutiont;
 
-class polynomialt {
- public:
+class polynomialt
+{
+public:
   // Invariant: this vector is sorted according to the monomial ordering induced
   // by monomialt::compare()
-  vector<monomialt> monomials;
+  std::vector<monomialt> monomials;
 
   exprt to_expr();
   void from_expr(exprt &expr);
@@ -47,6 +47,6 @@ class polynomialt {
   int coeff(exprt &expr);
 };
 
-typedef vector<polynomialt> polynomialst;
+typedef std::vector<polynomialt> polynomialst;
 
 #endif // POLYNOMIAL_H

src/goto-instrument/accelerate/polynomial_accelerator.h

@@ -4,11 +4,11 @@
 #include <map>
 #include <set>
 
+#include <util/symbol_table.h>
+
 #include <goto-programs/goto_program.h>
 #include <goto-programs/goto_functions.h>
 
-#include <symbol_table.h>
-
 #include "scratch_program.h"
 #include "polynomial.h"
 #include "path.h"

src/goto-instrument/accelerate/scratch_program.cpp

@@ -1,10 +1,9 @@
-#include <i2string.h>
-#include <fixedbv.h>
-#include <decision_procedure.h>
+#include <util/i2string.h>
+#include <util/fixedbv.h>
+#include <util/decision_procedure.h>
 
 #include <goto-symex/slice.h>
 
-
 #include "scratch_program.h"
 
 //#define DEBUG

src/goto-instrument/accelerate/scratch_program.h

@@ -3,7 +3,7 @@
 
 #include <string>
 
-#include <symbol_table.h>
+#include <util/symbol_table.h>
 
 #include <goto-programs/goto_program.h>
 #include <goto-programs/goto_functions.h>

src/goto-instrument/accelerate/symbolic_accelerator.h

@@ -1,13 +1,13 @@
 #ifndef SYMBOLIC_ACCELERATOR_H
 #define SYMBOLIC_ACCELERATOR_H
 
+#include <util/replace_expr.h>
+#include <util/symbol_table.h>
+
 #include "path.h"
 #include "polynomial.h"
 #include "linearize.h"
 
-#include <replace_expr.h>
-#include <symbol_table.h>
-
 #include "Eigen/Eigen"
 #include "Eigen/Eigenvalues"
 

src/goto-instrument/alignment_checks.cpp

@@ -6,9 +6,9 @@ Author:
 
 \*******************************************************************/
 
-#include <pointer_offset_size.h>
-#include <config.h>
-#include <symbol_table.h>
+#include <util/pointer_offset_size.h>
+#include <util/config.h>
+#include <util/symbol_table.h>
 
 #include "alignment_checks.h"
 

src/goto-instrument/branch.cpp

@@ -6,8 +6,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#include <cprover_prefix.h>
-#include <prefix.h>
+#include <util/cprover_prefix.h>
+#include <util/prefix.h>
 
 #include "function.h"
 #include "branch.h"

src/goto-instrument/concurrency.cpp

@@ -8,9 +8,9 @@ Date: October 2012
 
 \*******************************************************************/
 
-#include <std_expr.h>
-#include <find_symbols.h>
-#include <replace_symbol.h>
+#include <util/std_expr.h>
+#include <util/find_symbols.h>
+#include <util/replace_symbol.h>
 
 #include <analyses/is_threaded.h>
 

src/goto-instrument/document_claims.cpp

@@ -9,7 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <fstream>
 #include <cstdlib>
 
-#include <i2string.h>
+#include <util/i2string.h>
+
 #include <ansi-c/expr2c.h>
 
 #include "document_claims.h"

src/goto-instrument/dump_c.cpp

@@ -11,21 +11,21 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <map>
 #include <list>
 
-#include <config.h>
-#include <hash_cont.h>
-#include <language.h>
-#include <std_expr.h>
-#include <std_code.h>
-#include <std_types.h>
-#include <prefix.h>
-#include <simplify_expr.h>
-#include <replace_symbol.h>
-#include <find_symbols.h>
-#include <arith_tools.h>
-#include <suffix.h>
-#include <base_type.h>
-#include <type_eq.h>
-#include <i2string.h>
+#include <util/config.h>
+#include <util/hash_cont.h>
+#include <util/language.h>
+#include <util/std_expr.h>
+#include <util/std_code.h>
+#include <util/std_types.h>
+#include <util/prefix.h>
+#include <util/simplify_expr.h>
+#include <util/replace_symbol.h>
+#include <util/find_symbols.h>
+#include <util/arith_tools.h>
+#include <util/suffix.h>
+#include <util/base_type.h>
+#include <util/type_eq.h>
+#include <util/i2string.h>
 
 #include <langapi/mode.h>
 #include <ansi-c/ansi_c_language.h>

src/goto-instrument/function.cpp

@@ -6,10 +6,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#include <cprover_prefix.h>
-#include <prefix.h>
-#include <std_expr.h>
-#include <expr_util.h>
+#include <util/cprover_prefix.h>
+#include <util/prefix.h>
+#include <util/std_expr.h>
+#include <util/expr_util.h>
 
 #include <ansi-c/c_types.h>
 #include <ansi-c/string_constant.h>

src/goto-instrument/interrupt.cpp

@@ -8,11 +8,11 @@ Date: September 2011
 
 \*******************************************************************/
 
-#include <cprover_prefix.h>
-#include <std_expr.h>
-#include <std_code.h>
-#include <prefix.h>
-#include <symbol_table.h>
+#include <util/cprover_prefix.h>
+#include <util/std_expr.h>
+#include <util/std_code.h>
+#include <util/prefix.h>
+#include <util/symbol_table.h>
 
 #include "interrupt.h"
 #include "rw_set.h"

src/goto-instrument/mmio.cpp

@@ -8,14 +8,14 @@ Date: September 2011
 
 \*******************************************************************/
 
-#include <cprover_prefix.h>
+#include <util/cprover_prefix.h>
 
 #if 0
-#include <hash_cont.h>
-#include <std_expr.h>
-#include <expr_util.h>
-#include <guard.h>
-#include <prefix.h>
+#include <util/hash_cont.h>
+#include <util/std_expr.h>
+#include <util/expr_util.h>
+#include <util/guard.h>
+#include <util/prefix.h>
 
 #include <goto-programs/remove_skip.h>
 #endif

src/goto-instrument/nondet_static.cpp

@@ -8,10 +8,10 @@ Date: November 2011
 
 \*******************************************************************/
 
-#include <namespace.h>
-#include <std_expr.h>
-#include <cprover_prefix.h>
-#include <prefix.h>
+#include <util/namespace.h>
+#include <util/std_expr.h>
+#include <util/cprover_prefix.h>
+#include <util/prefix.h>
 
 #include <goto-programs/goto_functions.h>
 

src/goto-instrument/nondet_volatile.cpp

@@ -8,8 +8,8 @@ Date: September 2011
 
 \*******************************************************************/
 
-#include <std_expr.h>
-#include <symbol_table.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
 
 #include "nondet_volatile.h"
 

src/goto-instrument/parseoptions.cpp

@@ -11,8 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <memory>
 #include <cstdlib>
 
-#include <config.h>
-#include <expr_util.h>
+#include <util/config.h>
+#include <util/expr_util.h>
 
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/remove_function_pointers.h>

src/goto-instrument/race_check.cpp

@@ -8,12 +8,12 @@ Date: February 2006
 
 \*******************************************************************/
 
-#include <hash_cont.h>
-#include <std_expr.h>
-#include <expr_util.h>
-#include <guard.h>
-#include <symbol_table.h>
-#include <prefix.h>
+#include <util/hash_cont.h>
+#include <util/std_expr.h>
+#include <util/expr_util.h>
+#include <util/guard.h>
+#include <util/symbol_table.h>
+#include <util/prefix.h>
 
 #include <pointer-analysis/value_sets.h>
 #include <goto-programs/remove_skip.h>

src/goto-instrument/rw_set.cpp

@@ -8,10 +8,10 @@ Date: February 2006
 
 \*******************************************************************/
 
-#include <expr_util.h>
-#include <std_expr.h>
-#include <std_code.h>
-#include <namespace.h>
+#include <util/expr_util.h>
+#include <util/std_expr.h>
+#include <util/std_code.h>
+#include <util/namespace.h>
 
 #include <langapi/language_util.h>
 

src/goto-instrument/show_locations.cpp

@@ -8,9 +8,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <iostream>
 
-#include <xml.h>
-#include <i2string.h>
-#include <xml_irep.h>
+#include <util/xml.h>
+#include <util/i2string.h>
+#include <util/xml_irep.h>
 
 #include <langapi/language_util.h>
 

src/goto-instrument/stack_depth.cpp

@@ -8,12 +8,12 @@ Date: November 2011
 
 \*******************************************************************/
 
-#include <symbol_table.h>
-#include <std_expr.h>
-#include <std_types.h>
-#include <arith_tools.h>
-#include <cprover_prefix.h>
-#include <i2string.h>
+#include <util/symbol_table.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
+#include <util/arith_tools.h>
+#include <util/cprover_prefix.h>
+#include <util/i2string.h>
 
 #include <goto-programs/goto_functions.h>
 

src/goto-instrument/uninitialized.cpp

@@ -8,9 +8,9 @@ Date: January 2010
 
 \*******************************************************************/
 
-#include <std_code.h>
-#include <std_expr.h>
-#include <symbol_table.h>
+#include <util/std_code.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
 
 #include <analyses/uninitialized_domain.h>
 

src/goto-instrument/wmm/abstract_event.h

@@ -11,8 +11,8 @@ Date: 2012
 #ifndef ABSTRACT_EVENT_H
 #define ABSTRACT_EVENT_H
 
-#include <location.h>
-#include <graph.h>
+#include <util/location.h>
+#include <util/graph.h>
 
 #include "wmm.h"
 

src/goto-instrument/wmm/data_dp.h

@@ -13,7 +13,7 @@ Date: 2012
 
 #include <set>
 
-#include <location.h>
+#include <util/location.h>
 
 class abstract_eventt;
 

src/goto-instrument/wmm/event_graph.h

@@ -16,7 +16,7 @@ Date: 2012
 #include <map>
 #include <ostream>
 
-#include <graph.h>
+#include <util/graph.h>
 
 #include "abstract_event.h"
 #include "data_dp.h"

src/goto-instrument/wmm/fence.cpp

@@ -8,9 +8,10 @@ Date: February 2012
 
 \*******************************************************************/
 
-#include "fence.h"
 #include <iostream>
 
+#include "fence.h"
+
 bool is_fence(
   goto_programt::instructiont instruction,
   namespacet &ns)

src/goto-instrument/wmm/fence.h

@@ -11,7 +11,7 @@ Date: February 2012
 #ifndef FENCE_H
 #define FENCE_H
 
-#include <symbol_table.h>
+#include <util/symbol_table.h>
 #include <goto-programs/goto_program.h>
 
 bool is_fence(

src/goto-instrument/wmm/goto2graph.cpp

@@ -17,11 +17,11 @@ Date: 2012
 #include <cstdlib>
 #endif
 
-#include <prefix.h>
-#include <cprover_prefix.h>
-#include <options.h>
-#include <message.h>
-#include <i2string.h>
+#include <util/prefix.h>
+#include <util/cprover_prefix.h>
+#include <util/options.h>
+#include <util/message.h>
+#include <util/i2string.h>
 
 #include "../rw_set.h"
 #include "fence.h"

src/goto-instrument/wmm/goto2graph.h

@@ -13,8 +13,9 @@ Date: 2012
 
 #include <map>
 
-#include <graph.h>
-#include <namespace.h>
+#include <util/graph.h>
+#include <util/namespace.h>
+
 #include <goto-programs/goto_program.h>
 
 #include "event_graph.h"

src/goto-instrument/wmm/instrumenter_strategies.cpp

@@ -10,7 +10,7 @@ Date: 2012
 
 #include <string>
 
-#include <i2string.h>
+#include <util/i2string.h>
 
 #include "goto2graph.h"
 

src/goto-instrument/wmm/weak_memory.cpp

@@ -19,10 +19,10 @@ Date: September 2011
 #include <fstream>
 #include <iostream>
 
-#include <expr_util.h>
-#include <cprover_prefix.h>
-#include <prefix.h>
-#include <i2string.h>
+#include <util/expr_util.h>
+#include <util/cprover_prefix.h>
+#include <util/prefix.h>
+#include <util/i2string.h>
 
 #include <goto-programs/remove_skip.h>