Renaming from McTest to DeepState.

examples/CMakeLists.txt

@@ -12,14 +12,14 @@
 # See the License for the specific language governing permissions and
 # limitations under the License.
 
-add_executable(OutOfBoundsInt OutOfBoundsInt.cpp)
-target_link_libraries(OutOfBoundsInt mctest)
+add_executable(IntegerOverflow IntegerOverflow.cpp)
+target_link_libraries(IntegerOverflow deepstate)
 
-add_executable(ArithmeticProperties ArithmeticProperties.cpp)
-target_link_libraries(ArithmeticProperties mctest)
+add_executable(IntegerArtihmetic IntegerArithmetic.cpp)
+target_link_libraries(IntegerArtihmetic deepstate)
 
 add_executable(Lists Lists.cpp)
-target_link_libraries(Lists mctest)
+target_link_libraries(Lists deepstate)
 
 add_executable(StreamingAndFormatting StreamingAndFormatting.cpp)
-target_link_libraries(StreamingAndFormatting mctest)
+target_link_libraries(StreamingAndFormatting deepstate)

examples/IntegerArithmetic.cpp

@@ -14,12 +14,11 @@
  * limitations under the License.
  */
 
-#include <mctest/McUnit.hpp>
-#include <mctest/Quantified.hpp>
+#include <deepstate/DeepState.hpp>
 
-using namespace mctest;
+using namespace deepstate;
 
-MCTEST_NOINLINE int add(int x, int y) {
+DEEPSTATE_NOINLINE int add(int x, int y) {
   return x + y;
 }
 
@@ -47,5 +46,5 @@ TEST(Arithmetic, InvertibleMultiplication_CanFail) {
 }
 
 int main(void) {
-  return McTest_Run();
+  return DeepState_Run();
 }

examples/IntegerOverflow.cpp

@@ -14,30 +14,32 @@
  * limitations under the License.
  */
 
-#include <mctest/McUnit.hpp>
+#include <deepstate/DeepState.hpp>
 
-MCTEST_NOINLINE int ident1(int x) {
+using namespace deepstate;
+
+DEEPSTATE_NOINLINE int ident1(int x) {
   return x;
 }
 
-MCTEST_NOINLINE int ident2(int x) {
+DEEPSTATE_NOINLINE int ident2(int x) {
   return x;
 }
 
-TEST(BoundsCheck, YIsAlwaysPositive) {
-  int x = McTest_IntInRange(-10, 10);
-  int y = ident1(x) * ident2(x);
+TEST(SignedInteger, AdditionOverflow) {
+  Symbolic<int> x;
+  int y = ident1(x) + ident2(x);  // Can overflow!
   ASSERT_GE(y, 0)
       << "Found y=" << y << " was not always positive.";
 }
 
-TEST(BoundsCheck, YIsAlwaysPositive_CanFail) {
-  int x = McTest_Int();
+TEST(SignedInteger, MultiplicationOverflow) {
+  Symbolic<int> x;
   int y = ident1(x) * ident2(x);  // Can overflow!
   ASSERT_GE(y, 0)
-      << "Found y=" << y << " was not always positive.";
+      << x << " squared overflowed.";
 }
 
 int main(int argc, char *argv[]) {
-  return McTest_Run();
+  return DeepState_Run();
 }

examples/Lists.cpp

@@ -14,13 +14,12 @@
  * limitations under the License.
  */
 
-#include <mctest/McUnit.hpp>
-#include <mctest/Quantified.hpp>
+#include <deepstate/DeepState.hpp>
 
 #include <algorithm>
 #include <vector>
 
-using namespace mctest;
+using namespace deepstate;
 
 TEST(Vector, DoubleReversal) {
   ForAll<std::vector<int>>([] (const std::vector<int> &vec1) {
@@ -33,5 +32,5 @@ TEST(Vector, DoubleReversal) {
 }
 
 int main(void) {
-  McTest_Run();
+  DeepState_Run();
 }

examples/StreamingAndFormatting.cpp

@@ -14,7 +14,7 @@
  * limitations under the License.
  */
 
-#include <mctest/McUnit.hpp>
+#include <deepstate/DeepState.hpp>
 
 TEST(Streaming, BasicLevels) {
   LOG(DEBUG) << "This is a debug message";
@@ -40,5 +40,5 @@ TEST(Formatting, OverridePrintf) {
 }
 
 int main(void) {
-  return McTest_Run();
+  return DeepState_Run();
 }