Fix compiler warning in hashsmt example (#1927)
authorAndres Noetzli <andres.noetzli@gmail.com>
Mon, 21 May 2018 18:00:44 +0000 (21:00 +0300)
committerGitHub <noreply@github.com>
Mon, 21 May 2018 18:00:44 +0000 (21:00 +0300)
Previously, we were using delete for an array allocated on the heap,
which caused a warning. @dddejan fixed this and other issues in PR #1909
but after @ajreynol fixed the other issues in a separate PR and to not
waste @dddejan's time, I am submitting this fix separately (note: the
fix is slightly different in that it changes the array to a vector,
making a delete[] unnecessary).

examples/hashsmt/sha1_inversion.cpp

index 1a99ee4060578eb1d8b4d543523a19766a60c417..8704b582ffc92d386182b61523b5e6b289a95b64 100644 (file)
@@ -27,6 +27,7 @@
 #include <iostream>
 #include <sstream>
 #include <string>
+#include <vector>
 
 #include "expr/expr_iomanip.h"
 #include "options/language.h"
@@ -57,7 +58,7 @@ int main(int argc, char* argv[]) {
     output << SetBenchmarkStatusCommand(SMT_SATISFIABLE) << endl;
 
     // Make the variables the size of the string
-    hashsmt::cvc4_uchar8 *cvc4input = new hashsmt::cvc4_uchar8[msgSize];
+    std::vector<hashsmt::cvc4_uchar8> cvc4input(msgSize);
     for (unsigned i = 0; i < msgSize; ++ i) {
       stringstream ss;
       ss << "x" << i;
@@ -71,7 +72,7 @@ int main(int argc, char* argv[]) {
 
     // Do the cvc4 encoding
     hashsmt::sha1 cvc4encoder;
-    cvc4encoder.process_bytes(cvc4input, msgSize);
+    cvc4encoder.process_bytes(cvc4input.data(), msgSize);
 
     // Get the digest as bitvectors
     hashsmt::cvc4_uint32 cvc4digest[5];
@@ -97,9 +98,6 @@ int main(int argc, char* argv[]) {
 
     // Checksat command
     output << CheckSatCommand() << endl;
-
-    delete cvc4input;
-
   } catch (CVC4::Exception& e) {
     cerr << e << endl;
   }