Remove all references to optionalt

We now use `std::optional` instead.

.clang-format-ignore

@@ -1,4 +1,3 @@
 jbmc/src/miniz/miniz.cpp
 src/cprover/wcwidth.c
-src/nonstd/optional.hpp
 unit/catch/catch.hpp

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -445,7 +445,7 @@ int janalyzer_parse_optionst::perform_analysis(
     }
     else
     {
-      optionalt<std::string> json_file;
+      std::optional<std::string> json_file;
       if(cmdline.isset("json"))
         json_file = cmdline.get_value("json");
       bool result = taint_analysis(

jbmc/src/java_bytecode/README.md

@@ -677,7 +677,7 @@ used. Under eager loading
 \ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, lazy_class_to_declared_symbols_mapt &, message_handlert &)
 is called once for each method listed in method_bytecode (described above). This
 then calls
-\ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, optionalt<ci_lazy_methods_neededt>, lazy_class_to_declared_symbols_mapt &, message_handlert &);
+\ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, std::optional<ci_lazy_methods_neededt>, lazy_class_to_declared_symbols_mapt &, message_handlert &);
 
 without a ci_lazy_methods_neededt object, which calls
 \ref java_bytecode_convert_method, passing in the method parse tree. This in

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -44,7 +44,7 @@ struct object_creation_infot
 
   /// Where runtime types differ from compile-time types, we need to mark the
   /// runtime types as needed by lazy methods.
-  optionalt<ci_lazy_methods_neededt> &needed_lazy_methods;
+  std::optional<ci_lazy_methods_neededt> &needed_lazy_methods;
 
   /// Map to keep track of reference-equal objects. Each entry has an ID (such
   /// that any two reference-equal objects have the same ID) and the expression
@@ -117,7 +117,7 @@ static bool is_enum_with_type_equal_to_declaring_type(
 /// A runtime type that is different from the objects compile-time type should
 /// be specified in `json` in this way.
 /// Type values are of the format "my.package.name.ClassName".
-static optionalt<std::string> get_type(const jsont &json)
+static std::optional<std::string> get_type(const jsont &json)
 {
   if(!json.is_object())
     return {};
@@ -267,9 +267,9 @@ static jsont get_untyped_string(const jsont &json)
 /// \param symbol_table: used to look up the type given its name.
 /// \return runtime type of the object, if specified by at least one of the
 ///   parameters.
-static optionalt<java_class_typet> runtime_type(
+static std::optional<java_class_typet> runtime_type(
   const jsont &json,
-  const optionalt<std::string> &type_from_array,
+  const std::optional<std::string> &type_from_array,
   const symbol_table_baset &symbol_table)
 {
   const auto type_from_json = get_type(json);
@@ -304,9 +304,9 @@ static optionalt<java_class_typet> runtime_type(
 ///   field, this takes priority over \p type_from_array.
 /// \param type_from_array: may contain a type name from a containing array.
 /// \return if the type of an array was given, the type of its elements.
-static optionalt<std::string> element_type_from_array_type(
+static std::optional<std::string> element_type_from_array_type(
   const jsont &json,
-  const optionalt<std::string> &type_from_array)
+  const std::optional<std::string> &type_from_array)
 {
   if(const auto json_array_type = get_type(json))
   {
@@ -332,7 +332,7 @@ static optionalt<std::string> element_type_from_array_type(
 code_with_references_listt assign_from_json_rec(
   const exprt &expr,
   const jsont &json,
-  const optionalt<std::string> &type_from_array,
+  const std::optional<std::string> &type_from_array,
   object_creation_infot &info);
 
 /// One of the base cases (primitive case) of the recursion.
@@ -392,7 +392,7 @@ static code_frontend_assignt assign_null(const exprt &expr)
 static code_with_references_listt assign_array_data_component_from_json(
   const exprt &expr,
   const jsont &json,
-  const optionalt<std::string> &type_from_array,
+  const std::optional<std::string> &type_from_array,
   object_creation_infot &info)
 {
   const auto &java_class_type = followed_class_type(expr, info.symbol_table);
@@ -411,7 +411,7 @@ static code_with_references_listt assign_array_data_component_from_json(
     code_frontend_assignt{array_init_data, data_member_expr, info.loc});
 
   size_t index = 0;
-  const optionalt<std::string> inferred_element_type =
+  const std::optional<std::string> inferred_element_type =
     element_type_from_array_type(json, type_from_array);
   const json_arrayt json_array = get_untyped_array(json, element_type);
   for(auto it = json_array.begin(); it < json_array.end(); it++, index++)
@@ -457,7 +457,7 @@ static std::pair<code_with_references_listt, exprt>
 assign_det_length_array_from_json(
   const exprt &expr,
   const jsont &json,
-  const optionalt<std::string> &type_from_array,
+  const std::optional<std::string> &type_from_array,
   object_creation_infot &info)
 {
   PRECONDITION(is_java_array_type(expr.type()));
@@ -486,7 +486,7 @@ static code_with_references_listt assign_nondet_length_array_from_json(
   const exprt &array,
   const jsont &json,
   const exprt &given_length_expr,
-  const optionalt<std::string> &type_from_array,
+  const std::optional<std::string> &type_from_array,
   object_creation_infot &info)
 {
   PRECONDITION(is_java_array_type(array.type()));
@@ -793,7 +793,7 @@ static get_or_create_reference_resultt get_or_create_reference(
 static code_with_references_listt assign_reference_from_json(
   const exprt &expr,
   const jsont &json,
-  const optionalt<std::string> &type_from_array,
+  const std::optional<std::string> &type_from_array,
   object_creation_infot &info)
 {
   const std::string &id = has_enum_type(expr, info.symbol_table)
@@ -849,7 +849,7 @@ static code_with_references_listt assign_reference_from_json(
 code_with_references_listt assign_from_json_rec(
   const exprt &expr,
   const jsont &json,
-  const optionalt<std::string> &type_from_array,
+  const std::optional<std::string> &type_from_array,
   object_creation_infot &info)
 {
   code_with_references_listt result;
@@ -915,7 +915,7 @@ code_with_references_listt assign_from_json(
   const jsont &json,
   const irep_idt &function_id,
   symbol_table_baset &symbol_table,
-  optionalt<ci_lazy_methods_neededt> &needed_lazy_methods,
+  std::optional<ci_lazy_methods_neededt> &needed_lazy_methods,
   size_t max_user_array_length,
   std::unordered_map<std::string, object_creation_referencet> &references)
 {

jbmc/src/java_bytecode/assignments_from_json.h

@@ -100,7 +100,7 @@ code_with_references_listt assign_from_json(
   const jsont &json,
   const irep_idt &function_id,
   symbol_table_baset &symbol_table,
-  optionalt<ci_lazy_methods_neededt> &needed_lazy_methods,
+  std::optional<ci_lazy_methods_neededt> &needed_lazy_methods,
   size_t max_user_array_length,
   std::unordered_map<std::string, object_creation_referencet> &references);
 

jbmc/src/java_bytecode/ci_lazy_methods.h

@@ -41,7 +41,8 @@ class method_bytecodet
     const java_bytecode_parse_treet::methodt &method;
   };
 
-  typedef optionalt<std::reference_wrapper<const class_method_and_bytecodet>>
+  typedef std::optional<
+    std::reference_wrapper<const class_method_and_bytecodet>>
     opt_reft;
 
 private:

jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp

@@ -53,7 +53,7 @@ void ci_lazy_methods_neededt::add_cprover_nondet_initialize_if_it_exists(
   const irep_idt &class_id)
 {
   resolve_inherited_componentt resolve_inherited_component{symbol_table};
-  optionalt<resolve_inherited_componentt::inherited_componentt>
+  std::optional<resolve_inherited_componentt::inherited_componentt>
     cprover_nondet_initialize = resolve_inherited_component(
       class_id, "cproverNondetInitialize:()V", true);
 

jbmc/src/java_bytecode/code_with_references.h

@@ -30,7 +30,7 @@ struct object_creation_referencet
   /// This should only be set once the actual elements of the array have been
   /// seen, not the first time an `@ref` have been seen, only when `@id` is
   /// seen.
-  optionalt<exprt> array_length;
+  std::optional<exprt> array_length;
 };
 
 /// Base class for code which can contain references which can get replaced

jbmc/src/java_bytecode/generic_parameter_specialization_map.cpp

@@ -51,7 +51,7 @@ void generic_parameter_specialization_mapt::pop(std::size_t container_index)
   container_to_specializations.at(container_index).pop();
 }
 
-optionalt<reference_typet>
+std::optional<reference_typet>
 generic_parameter_specialization_mapt::pop(const irep_idt &parameter_name)
 {
   const auto types_it = param_to_container.find(parameter_name);

jbmc/src/java_bytecode/generic_parameter_specialization_map.h

@@ -53,8 +53,8 @@ class generic_parameter_specialization_mapt
   /// a given type parameter
   /// \param parameter_name: The name of the type parameter
   /// \returns: The specialization for the given type parameter, if there was
-  ///   one before the pop, or an empty optionalt if the stack was empty
-  optionalt<reference_typet> pop(const irep_idt &parameter_name);
+  ///   one before the pop, or an empty std::optional if the stack was empty
+  std::optional<reference_typet> pop(const irep_idt &parameter_name);
 
   /// A wrapper for a generic_parameter_specialization_mapt and a namespacet
   /// that can be output to a stream

jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h

@@ -17,7 +17,7 @@ class generic_parameter_specialization_map_keyst
   /// Generic parameter specialization map to modify
   generic_parameter_specialization_mapt &generic_parameter_specialization_map;
   /// Key of the container to pop on destruction
-  optionalt<std::size_t> container_id;
+  std::optional<std::size_t> container_id;
 
 public:
   /// Initialize a generic-parameter-specialization-map entry owner operating

jbmc/src/java_bytecode/jar_file.cpp

@@ -54,7 +54,7 @@ jar_filet &jar_filet::operator=(jar_filet &&other)
   return *this;
 }
 
-optionalt<std::string> jar_filet::get_entry(const std::string &name)
+std::optional<std::string> jar_filet::get_entry(const std::string &name)
 {
   const auto entry=m_name_to_index.find(name);
   if(entry==m_name_to_index.end())

jbmc/src/java_bytecode/jar_file.h

@@ -9,14 +9,13 @@ Author: Diffblue Ltd
 #ifndef CPROVER_JAVA_BYTECODE_JAR_FILE_H
 #define CPROVER_JAVA_BYTECODE_JAR_FILE_H
 
-#include <unordered_map>
+#include "mz_zip_archive.h"
+
+#include <optional>
 #include <string>
+#include <unordered_map>
 #include <vector>
 
-#include <util/optional.h>
-
-#include "mz_zip_archive.h"
-
 /// Class representing a .jar archive. Uses miniz to decompress and index
 /// archive.
 class jar_filet final
@@ -42,7 +41,7 @@ class jar_filet final
   /// Get contents of a file in the jar archive.
   /// Returns nullopt if file doesn't exist.
   /// \param filename: Name of the file in the archive
-  optionalt<std::string> get_entry(const std::string &filename);
+  std::optional<std::string> get_entry(const std::string &filename);
 
   /// Get contents of the Manifest file in the jar archive as a key-value map
   /// (both as strings)

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -186,8 +186,8 @@ class java_bytecode_convert_classt
 /// \param signature: Signature of the class
 /// \return Reference of the generic superclass, or empty if the superclass
 ///   is not generic
-static optionalt<std::string>
-extract_generic_superclass_reference(const optionalt<std::string> &signature)
+static std::optional<std::string> extract_generic_superclass_reference(
+  const std::optional<std::string> &signature)
 {
   if(signature.has_value())
   {
@@ -226,8 +226,8 @@ extract_generic_superclass_reference(const optionalt<std::string> &signature)
 /// \param interface_name: The interface name
 /// \return Reference of the generic interface, or empty if the interface
 ///   is not generic
-static optionalt<std::string> extract_generic_interface_reference(
-  const optionalt<std::string> &signature,
+static std::optional<std::string> extract_generic_interface_reference(
+  const std::optional<std::string> &signature,
   const std::string &interface_name)
 {
   if(signature.has_value())
@@ -355,7 +355,7 @@ void java_bytecode_convert_classt::convert(
     // including the generic info in its signature
     // e.g., signature for class 'A<T>' that extends
     // 'Generic<Integer>' is '<T:Ljava/lang/Object;>LGeneric<LInteger;>;'
-    const optionalt<std::string> &superclass_ref =
+    const std::optional<std::string> &superclass_ref =
       extract_generic_superclass_reference(c.signature);
     if(superclass_ref.has_value())
     {
@@ -397,7 +397,7 @@ void java_bytecode_convert_classt::convert(
     // including the generic info in its signature
     // e.g., signature for class 'A implements GenericInterface<Integer>' is
     // 'Ljava/lang/Object;LGenericInterface<LInteger;>;'
-    const optionalt<std::string> interface_ref =
+    const std::optional<std::string> interface_ref =
       extract_generic_interface_reference(c.signature, id2string(interface));
     if(interface_ref.has_value())
     {

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -228,7 +228,7 @@ exprt java_bytecode_convert_methodt::variable(
 /// \return the constructed member type
 java_method_typet member_type_lazy(
   const std::string &descriptor,
-  const optionalt<std::string> &signature,
+  const std::optional<std::string> &signature,
   const std::string &class_name,
   const std::string &method_name,
   message_handlert &message_handler)
@@ -534,7 +534,7 @@ void create_parameter_symbols(
 void java_bytecode_convert_methodt::convert(
   const symbolt &class_symbol,
   const methodt &m,
-  const optionalt<prefix_filtert> &method_context)
+  const std::optional<prefix_filtert> &method_context)
 {
   // Construct the fully qualified method name
   // (e.g. "my.package.ClassName.myMethodName:(II)I") and query the symbol table
@@ -1263,7 +1263,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
       }
     }
 
-    optionalt<codet> catch_instruction;
+    std::optional<codet> catch_instruction;
 
     if(catch_type!=typet())
     {
@@ -3083,7 +3083,7 @@ code_blockt java_bytecode_convert_methodt::convert_astore(
   return block;
 }
 
-optionalt<exprt> java_bytecode_convert_methodt::convert_invoke_dynamic(
+std::optional<exprt> java_bytecode_convert_methodt::convert_invoke_dynamic(
   const source_locationt &location,
   std::size_t instruction_address,
   const exprt &arg0,
@@ -3282,11 +3282,11 @@ void java_bytecode_convert_method(
   message_handlert &message_handler,
   size_t max_array_length,
   bool throw_assertion_error,
-  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
+  std::optional<ci_lazy_methods_neededt> needed_lazy_methods,
   java_string_library_preprocesst &string_preprocess,
   const class_hierarchyt &class_hierarchy,
   bool threading_support,
-  const optionalt<prefix_filtert> &method_context,
+  const std::optional<prefix_filtert> &method_context,
   bool assert_no_exceptions_thrown)
 
 {

jbmc/src/java_bytecode/java_bytecode_convert_method.h

@@ -31,11 +31,11 @@ void java_bytecode_convert_method(
   message_handlert &message_handler,
   size_t max_array_length,
   bool throw_assertion_error,
-  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
+  std::optional<ci_lazy_methods_neededt> needed_lazy_methods,
   java_string_library_preprocesst &string_preprocess,
   const class_hierarchyt &class_hierarchy,
   bool threading_support,
-  const optionalt<prefix_filtert> &method_context,
+  const std::optional<prefix_filtert> &method_context,
   bool assert_no_exceptions_thrown);
 
 void create_method_stub_symbol(

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -40,7 +40,7 @@ class java_bytecode_convert_methodt
     message_handlert &_message_handler,
     size_t _max_array_length,
     bool throw_assertion_error,
-    optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
+    std::optional<ci_lazy_methods_neededt> needed_lazy_methods,
     java_string_library_preprocesst &_string_preprocess,
     const class_hierarchyt &class_hierarchy,
     bool threading_support,
@@ -69,7 +69,7 @@ class java_bytecode_convert_methodt
   void operator()(
     const symbolt &class_symbol,
     const methodt &method,
-    const optionalt<prefix_filtert> &method_context)
+    const std::optional<prefix_filtert> &method_context)
   {
     convert(class_symbol, method, method_context);
   }
@@ -84,7 +84,7 @@ class java_bytecode_convert_methodt
   const bool throw_assertion_error;
   const bool assert_no_exceptions_thrown;
   const bool threading_support;
-  optionalt<ci_lazy_methods_neededt> needed_lazy_methods;
+  std::optional<ci_lazy_methods_neededt> needed_lazy_methods;
 
   /// Fully qualified name of the method under translation.
   /// Initialized by `convert`.
@@ -319,7 +319,7 @@ class java_bytecode_convert_methodt
   void convert(
     const symbolt &class_symbol,
     const methodt &,
-    const optionalt<prefix_filtert> &method_context);
+    const std::optional<prefix_filtert> &method_context);
 
   code_blockt convert_parameter_annotations(
     const methodt &method,
@@ -368,7 +368,7 @@ class java_bytecode_convert_methodt
       std::vector<java_bytecode_parse_treet::instructiont>::const_iterator>
       &ret_instructions) const;
 
-  optionalt<exprt> convert_invoke_dynamic(
+  std::optional<exprt> convert_invoke_dynamic(
     const source_locationt &location,
     std::size_t instruction_address,
     const exprt &arg0,