Use C++17

.github/workflows/pull-request-check-rust-api.yaml

@@ -62,7 +62,7 @@ jobs:
       # by the other jobs already present in `pull-request-checks.yaml`.
       - name: Run Rust API tests
         run: |
-          VERSION=$(cat src/config.inc | python3 -c "import sys,re;line = [line for line in sys.stdin if re.search('CBMC_VERSION = (\d+\.\d+\.\d+)', line)];sys.stdout.write(re.search('CBMC_VERSION = (\d+\.\d+\.\d+)', line[0]).group(1))")
+          VERSION=$(cat src/config.inc | python3 -c "import sys,re;line = [line for line in sys.stdin if re.search(r'CBMC_VERSION = (\d+\.\d+\.\d+)', line)];sys.stdout.write(re.search(r'CBMC_VERSION = (\d+\.\d+\.\d+)', line[0]).group(1))")
           cd src/libcprover-rust;\
           cargo clean;\
           CBMC_INCLUDE_DIR=../../${{env.default_include_dir}} CBMC_LIB_DIR=../../${{env.default_build_dir}}/lib CBMC_VERSION=$VERSION cargo test -- --test-threads=1
@@ -82,10 +82,10 @@ jobs:
         uses: actions/cache@v3
         with:
           path: .ccache
-          key: ${{ runner.os }}-Release-${{ github.ref }}-${{ github.sha }}-PR-Rust-API
+          key: ${{ runner.os }}-Release-Minisat-${{ github.ref }}-${{ github.sha }}-PR-Rust-API
           restore-keys: |
-            ${{ runner.os }}-Release-${{ github.ref }}
-            ${{ runner.os }}-Release
+            ${{ runner.os }}-Release-Minisat-${{ github.ref }}
+            ${{ runner.os }}-Release-Minisat
       - name: ccache environment
         run: |
           echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
@@ -102,7 +102,8 @@ jobs:
       # by the other jobs already present in `pull-request-checks.yaml`.
       - name: Run Rust API tests
         run: |
-          VERSION=$(cat src/config.inc | python3 -c "import sys,re;line = [line for line in sys.stdin if re.search('CBMC_VERSION = (\d+\.\d+\.\d+)', line)];sys.stdout.write(re.search('CBMC_VERSION = (\d+\.\d+\.\d+)', line[0]).group(1))")
+          export MACOSX_DEPLOYMENT_TARGET=10.15
+          VERSION=$(cat src/config.inc | python3 -c "import sys,re;line = [line for line in sys.stdin if re.search(r'CBMC_VERSION = (\d+\.\d+\.\d+)', line)];sys.stdout.write(re.search(r'CBMC_VERSION = (\d+\.\d+\.\d+)', line[0]).group(1))")
           cd src/libcprover-rust;\
           cargo clean;\
           CBMC_INCLUDE_DIR=../../${{env.default_include_dir}} CBMC_LIB_DIR=../../${{env.default_build_dir}}/lib CBMC_VERSION=$VERSION cargo test -- --test-threads=1

CODEOWNERS

@@ -23,7 +23,6 @@
 /src/json-symtab-language/ @martin-cs
 /src/langapi/ @kroening @tautschnig @peterschrammel
 /src/xmllang/ @kroening @tautschnig @peterschrammel
-/src/nonstd/ @peterschrammel
 /src/solvers/flattening @martin-cs @kroening @tautschnig @peterschrammel
 /src/solvers/floatbv @martin-cs @kroening
 /src/solvers/miniBDD @tautschnig @kroening

doc/architectural/folder-walkthrough.md

@@ -51,7 +51,6 @@ containing the code for a different part of the system.
   * \ref xmllang
   * \ref util
   * \ref miniz
-  * \ref nonstd
 
 In the top level of `src` there are only a few files:
 
@@ -167,7 +166,6 @@ digraph directory_dependencies {
     big_int [label = "big-int", URL = "\ref big-int"];
     miniz [URL = "\ref miniz"];
     util [URL = "\ref util"];
-    nonstd [URL = "\ref nonstd"];
     json [URL = "\ref json"];
     xmllang [URL = "\ref xmllang"];
     assembler [URL = "\ref assembler"];
@@ -203,6 +201,5 @@ digraph directory_dependencies {
   xmllang -> util;
   assembler -> util;
   util -> big_int;
-  util -> nonstd;
 }
 \enddot

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -396,7 +396,7 @@ int janalyzer_parse_optionst::doit()
   lazy_goto_model.initialize(cmdline.args, options);
 
   class_hierarchy =
-    util_make_unique<class_hierarchyt>(lazy_goto_model.symbol_table);
+    std::make_unique<class_hierarchyt>(lazy_goto_model.symbol_table);
 
   log.status() << "Generating GOTO Program" << messaget::eom;
   lazy_goto_model.load_all_functions();

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -745,7 +745,13 @@ static get_or_create_reference_resultt get_or_create_reference(
   if(id_it == info.references.end())
   {
     code_with_references_listt code;
+// Work around spurious GCC 13 warning about references being uninitialised.
+#pragma GCC diagnostic push
+#ifndef __clang__
+#  pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
+#endif
     object_creation_referencet reference;
+#pragma GCC diagnostic pop
     if(is_java_array_type(expr.type()))
     {
       reference.expr = info.allocate_objects.allocate_automatic_local_object(

jbmc/src/java_bytecode/ci_lazy_methods.h

@@ -82,7 +82,7 @@ class method_bytecodet
   {
     const auto it = map.find(method_id);
     if(it == map.end())
-      return opt_reft();
+      return std::nullopt;
     return std::cref(it->second);
   }
 };

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -1517,7 +1517,7 @@ void java_bytecode_languaget::show_parse(std::ostream &out)
 
 std::unique_ptr<languaget> new_java_bytecode_language()
 {
-  return util_make_unique<java_bytecode_languaget>();
+  return std::make_unique<java_bytecode_languaget>();
 }
 
 bool java_bytecode_languaget::from_expr(

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H
 
 #include <util/json.h>
-#include <util/make_unique.h>
 #include <util/prefix_filter.h>
 #include <util/symbol.h> // IWYU pragma: keep
 
@@ -319,7 +318,9 @@ class java_bytecode_languaget:public languaget
     const namespacet &ns) override;
 
   std::unique_ptr<languaget> new_language() override
-  { return util_make_unique<java_bytecode_languaget>(); }
+  {
+    return std::make_unique<java_bytecode_languaget>();
+  }
 
   std::string id() const override { return "java"; }
   std::string description() const override { return "Java Bytecode"; }

jbmc/src/java_bytecode/java_class_loader_base.cpp

@@ -8,15 +8,15 @@ Author: Daniel Kroening, [email protected]
 
 #include "java_class_loader_base.h"
 
-#include "jar_file.h"
-#include "java_bytecode_parse_tree.h"
-#include "java_bytecode_parser.h"
-
-#include <util/file_util.h>
 #include <util/message.h>
 #include <util/prefix.h>
 #include <util/suffix.h>
 
+#include "jar_file.h"
+#include "java_bytecode_parse_tree.h"
+#include "java_bytecode_parser.h"
+
+#include <filesystem>
 #include <fstream>
 
 void java_class_loader_baset::add_classpath_entry(
@@ -40,7 +40,7 @@ void java_class_loader_baset::add_classpath_entry(
   }
   else
   {
-    if(is_directory(path))
+    if(std::filesystem::is_directory(path))
     {
       classpath_entries.push_back(
         classpath_entryt(classpath_entryt::DIRECTORY, path));
@@ -197,7 +197,8 @@ java_class_loader_baset::get_class_from_directory(
 {
   // Look in the given directory
   const std::string class_file = class_name_to_os_file(class_name);
-  const std::string full_path = concat_dir_file(path, class_file);
+  const std::string full_path =
+    std::filesystem::path(path).append(class_file).string();
 
   if(std::ifstream(full_path))
   {

jbmc/src/java_bytecode/java_qualifiers.cpp

@@ -8,8 +8,6 @@
 #include <sstream>
 #include <iterator>
 
-#include <util/make_unique.h>
-
 #include "expr2java.h"
 
 java_qualifierst &java_qualifierst::operator=(const java_qualifierst &other)
@@ -24,7 +22,7 @@ java_qualifierst &java_qualifierst::operator=(const java_qualifierst &other)
 
 std::unique_ptr<qualifierst> java_qualifierst::clone() const
 {
-  auto other = util_make_unique<java_qualifierst>(ns);
+  auto other = std::make_unique<java_qualifierst>(ns);
   *other = *this;
   return std::move(other);
 }

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/exit_codes.h>
 #include <util/help_formatter.h>
 #include <util/invariant.h>
-#include <util/make_unique.h>
 #include <util/version.h>
 #include <util/xml.h>
 
@@ -535,7 +534,7 @@ int jbmc_parse_optionst::doit()
     options.get_bool_option("stop-on-fail") && options.get_bool_option("paths"))
   {
     verifier =
-      util_make_unique<stop_on_fail_verifiert<java_single_path_symex_checkert>>(
+      std::make_unique<stop_on_fail_verifiert<java_single_path_symex_checkert>>(
         options, ui_message_handler, *goto_model_ptr);
   }
   else if(
@@ -545,13 +544,13 @@ int jbmc_parse_optionst::doit()
     if(options.get_bool_option("localize-faults"))
     {
       verifier =
-        util_make_unique<stop_on_fail_verifier_with_fault_localizationt<
+        std::make_unique<stop_on_fail_verifier_with_fault_localizationt<
           java_multi_path_symex_checkert>>(
           options, ui_message_handler, *goto_model_ptr);
     }
     else
     {
-      verifier = util_make_unique<
+      verifier = std::make_unique<
         stop_on_fail_verifiert<java_multi_path_symex_checkert>>(
         options, ui_message_handler, *goto_model_ptr);
     }
@@ -560,7 +559,7 @@ int jbmc_parse_optionst::doit()
     !options.get_bool_option("stop-on-fail") &&
     options.get_bool_option("paths"))
   {
-    verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
+    verifier = std::make_unique<all_properties_verifier_with_trace_storaget<
       java_single_path_symex_checkert>>(
       options, ui_message_handler, *goto_model_ptr);
   }
@@ -571,13 +570,13 @@ int jbmc_parse_optionst::doit()
     if(options.get_bool_option("localize-faults"))
     {
       verifier =
-        util_make_unique<all_properties_verifier_with_fault_localizationt<
+        std::make_unique<all_properties_verifier_with_fault_localizationt<
           java_multi_path_symex_checkert>>(
           options, ui_message_handler, *goto_model_ptr);
     }
     else
     {
-      verifier = util_make_unique<all_properties_verifier_with_trace_storaget<
+      verifier = std::make_unique<all_properties_verifier_with_trace_storaget<
         java_multi_path_symex_checkert>>(
         options, ui_message_handler, *goto_model_ptr);
     }
@@ -603,7 +602,7 @@ int jbmc_parse_optionst::get_goto_program(
   lazy_goto_model.initialize(cmdline.args, options);
 
   class_hierarchy =
-    util_make_unique<class_hierarchyt>(lazy_goto_model.symbol_table);
+    std::make_unique<class_hierarchyt>(lazy_goto_model.symbol_table);
 
   // Show the class hierarchy
   if(cmdline.isset("show-class-hierarchy"))
@@ -662,7 +661,7 @@ int jbmc_parse_optionst::get_goto_program(
     }
 
     goto_model_ptr =
-      util_make_unique<lazy_goto_modelt>(std::move(lazy_goto_model));
+      std::make_unique<lazy_goto_modelt>(std::move(lazy_goto_model));
   }
 
   log.status() << config.object_bits_info() << messaget::eom;

jbmc/unit/java-testing-utils/load_java_class.cpp

@@ -8,19 +8,18 @@ Author: Diffblue Ltd.
 
 #include "load_java_class.h"
 
-#include <iostream>
-#include <testing-utils/free_form_cmdline.h>
-#include <testing-utils/message.h>
-#include <testing-utils/use_catch.h>
-
 #include <util/config.h>
 #include <util/options.h>
 #include <util/suffix.h>
 
+#include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/lazy_goto_model.h>
+#include <testing-utils/free_form_cmdline.h>
+#include <testing-utils/message.h>
+#include <testing-utils/use_catch.h>
 
-#include <java_bytecode/java_bytecode_language.h>
-#include <util/file_util.h>
+#include <filesystem>
+#include <iostream>
 
 /// Go through the process of loading, type-checking and finalising loading a
 /// specific class file to build the symbol table. The functions are converted
@@ -149,7 +148,7 @@ goto_modelt load_goto_model_from_java_class(
   // Log the working directory to help people identify the common error
   // of wrong working directory (should be the `unit` directory when running
   // the unit tests).
-  std::string path = get_current_working_directory();
+  std::string path = std::filesystem::current_path().string();
   INFO("Working directory: " << path);
 
   // if this fails it indicates the class was not loaded

src/analyses/ai.h

@@ -50,7 +50,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/deprecate.h>
 #include <util/json.h>
-#include <util/make_unique.h>
 #include <util/message.h>
 #include <util/xml.h>
 
@@ -565,20 +564,20 @@ class ait : public ai_recursive_interproceduralt
   // constructor
   ait()
     : ai_recursive_interproceduralt(
-        util_make_unique<
+        std::make_unique<
           ai_history_factory_default_constructort<ahistoricalt>>(),
-        util_make_unique<ai_domain_factory_default_constructort<domainT>>(),
-        util_make_unique<location_sensitive_storaget>(),
+        std::make_unique<ai_domain_factory_default_constructort<domainT>>(),
+        std::make_unique<location_sensitive_storaget>(),
         no_logging)
   {
   }
 
   explicit ait(std::unique_ptr<ai_domain_factory_baset> &&df)
     : ai_recursive_interproceduralt(
-        util_make_unique<
+        std::make_unique<
           ai_history_factory_default_constructort<ahistoricalt>>(),
         std::move(df),
-        util_make_unique<location_sensitive_storaget>(),
+        std::make_unique<location_sensitive_storaget>(),
         no_logging)
   {
   }

src/analyses/ai_domain.h

@@ -41,7 +41,6 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_ANALYSES_AI_DOMAIN_H
 
 #include <util/json.h>
-#include <util/make_unique.h>
 #include <util/xml.h>
 
 #include "ai_history.h"
@@ -206,7 +205,7 @@ class ai_domain_factoryt : public ai_domain_factory_baset
 
   std::unique_ptr<statet> copy(const statet &s) const override
   {
-    return util_make_unique<domainT>(static_cast<const domainT &>(s));
+    return std::make_unique<domainT>(static_cast<const domainT &>(s));
   }
 
   bool merge(statet &dest, const statet &src, trace_ptrt from, trace_ptrt to)
@@ -229,7 +228,7 @@ class ai_domain_factory_default_constructort
 
   std::unique_ptr<statet> make(locationt l) const override
   {
-    auto d = util_make_unique<domainT>();
+    auto d = std::make_unique<domainT>();
     CHECK_RETURN(d->is_bottom());
     return std::unique_ptr<statet>(d.release());
   }
@@ -246,7 +245,7 @@ class ai_domain_factory_location_constructort
 
   std::unique_ptr<statet> make(locationt l) const override
   {
-    auto d = util_make_unique<domainT>(l);
+    auto d = std::make_unique<domainT>(l);
     CHECK_RETURN(d->is_bottom());
     return std::unique_ptr<statet>(d.release());
   }

src/analyses/dependence_graph.cpp

@@ -349,7 +349,7 @@ class dep_graph_domain_factoryt : public ai_domain_factoryt<dep_graph_domaint>
   {
     auto node_id = dg.add_node();
     dg.nodes[node_id].PC = l;
-    auto p = util_make_unique<dep_graph_domaint>(node_id);
+    auto p = std::make_unique<dep_graph_domaint>(node_id);
     CHECK_RETURN(p->is_bottom());
 
     return std::unique_ptr<statet>(p.release());
@@ -360,7 +360,7 @@ class dep_graph_domain_factoryt : public ai_domain_factoryt<dep_graph_domaint>
 };
 
 dependence_grapht::dependence_grapht(const namespacet &_ns)
-  : ait<dep_graph_domaint>(util_make_unique<dep_graph_domain_factoryt>(*this)),
+  : ait<dep_graph_domaint>(std::make_unique<dep_graph_domain_factoryt>(*this)),
     ns(_ns),
     rd(ns)
 {