From f0262affb354490a5b39d35d8e03a030900e9d36 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 23 Mar 2022 11:47:19 +0000 Subject: [PATCH 1/7] Replace nonstd::optional by C++17 std::optional Removes third-party code that is no longer necessary now that we use C++ 17 as build standard. Future uses of optionalt should instead use std::optional directly. --- CODEOWNERS | 1 - doc/architectural/folder-walkthrough.md | 3 - .../java_bytecode/assignments_from_json.cpp | 6 + jbmc/src/java_bytecode/ci_lazy_methods.h | 2 +- .../dynamic-frames/dfcc_cfg_info.cpp | 4 +- .../dfcc_lift_memory_predicates.cpp | 2 +- src/goto-programs/link_goto_model.cpp | 2 +- src/nonstd/README.md | 7 - src/nonstd/module_dependencies.txt | 1 - src/nonstd/optional.hpp | 1089 ----------------- src/solvers/flattening/boolbv_overflow.cpp | 2 +- src/solvers/flattening/boolbv_width.h | 2 +- src/solvers/strings/string_dependencies.h | 3 +- src/util/arith_tools.h | 6 +- src/util/module_dependencies.txt | 1 - src/util/numbering.h | 2 +- src/util/optional.h | 48 +- src/util/sharing_map.h | 2 +- src/util/string2int.h | 4 +- unit/Makefile | 1 - unit/util/optional.cpp | 32 - 21 files changed, 25 insertions(+), 1195 deletions(-) delete mode 100644 src/nonstd/README.md delete mode 100644 src/nonstd/module_dependencies.txt delete mode 100644 src/nonstd/optional.hpp delete mode 100644 unit/util/optional.cpp diff --git a/CODEOWNERS b/CODEOWNERS index 1b456784481..8fc1e16f58f 100644 --- a/CODEOWNERS +++ b/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 diff --git a/doc/architectural/folder-walkthrough.md b/doc/architectural/folder-walkthrough.md index 53b69641bf9..5d5643d804c 100644 --- a/doc/architectural/folder-walkthrough.md +++ b/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 diff --git a/jbmc/src/java_bytecode/assignments_from_json.cpp b/jbmc/src/java_bytecode/assignments_from_json.cpp index 223f5a5187e..eeca79ce253 100644 --- a/jbmc/src/java_bytecode/assignments_from_json.cpp +++ b/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( diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.h b/jbmc/src/java_bytecode/ci_lazy_methods.h index 04fab8e5068..d96174aec39 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.h +++ b/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); } }; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp index 25142e28307..7eb14538971 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp @@ -138,7 +138,7 @@ dfcc_loop_infot::find_head(goto_programt &goto_program) const optionalt dfcc_loop_infot::find_latch(goto_programt &goto_program) const { - optionalt result = nullopt; + optionalt result = std::nullopt; for(auto target = goto_program.instructions.begin(); target != goto_program.instructions.end(); target++) @@ -728,7 +728,7 @@ dfcc_cfg_infot::get_outer_loop_identifier(const std::size_t loop_id) const } } // return nullopt for loops that are not nested in other loops - return nullopt; + return std::nullopt; } bool dfcc_cfg_infot::is_valid_loop_or_top_level_id(const std::size_t id) const diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp index 47953afeda8..3669ab3c183 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp @@ -331,7 +331,7 @@ void dfcc_lift_memory_predicatest::lift_parameters_and_update_body( // rewrite all occurrences of lifted parameters instruction.transform([&replace_lifted_params](exprt expr) { const bool changed = !replace_lifted_params.replace(expr); - return changed ? optionalt{expr} : nullopt; + return changed ? optionalt{expr} : std::nullopt; }); // add address-of to all arguments expressions passed in lifted position to diff --git a/src/goto-programs/link_goto_model.cpp b/src/goto-programs/link_goto_model.cpp index 9d8343977b8..5c66ae0d6ef 100644 --- a/src/goto-programs/link_goto_model.cpp +++ b/src/goto-programs/link_goto_model.cpp @@ -217,7 +217,7 @@ void finalize_linking( { instruction.transform([&object_type_updates](exprt expr) { const bool changed = !object_type_updates.replace(expr); - return changed ? optionalt{expr} : nullopt; + return changed ? optionalt{expr} : std::nullopt; }); } } diff --git a/src/nonstd/README.md b/src/nonstd/README.md deleted file mode 100644 index aebbaabb6ff..00000000000 --- a/src/nonstd/README.md +++ /dev/null @@ -1,7 +0,0 @@ -\ingroup module_hidden -\defgroup nonstd nonstd - -# Folder nonstd - -`nonstd` contains implementations of C++ utilities that are not yet -part of the standard library, e.g. for `optional`. diff --git a/src/nonstd/module_dependencies.txt b/src/nonstd/module_dependencies.txt deleted file mode 100644 index 55e484b8664..00000000000 --- a/src/nonstd/module_dependencies.txt +++ /dev/null @@ -1 +0,0 @@ -nonstd diff --git a/src/nonstd/optional.hpp b/src/nonstd/optional.hpp deleted file mode 100644 index 60011dff73c..00000000000 --- a/src/nonstd/optional.hpp +++ /dev/null @@ -1,1089 +0,0 @@ -// -// Copyright (c) 2016 Martin Moene -// -// https://github.com/martinmoene/optional-lite -// -// This code is licensed under the MIT License (MIT). -// -// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR -// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, -// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE -// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER -// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, -// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN -// THE SOFTWARE. - -// IWYU pragma: private, include -// IWYU pragma: private, include "optional.h" - -#pragma once - -#ifndef NONSTD_OPTIONAL_LITE_HPP -#define NONSTD_OPTIONAL_LITE_HPP - -#include -#include -#include - -#define optional_lite_VERSION "2.1.0" - -// variant-lite alignment configuration: - -#ifndef optional_CONFIG_MAX_ALIGN_HACK -# define optional_CONFIG_MAX_ALIGN_HACK 0 -#endif - -#ifndef optional_CONFIG_ALIGN_AS -// no default, used in #if defined() -#endif - -#ifndef optional_CONFIG_ALIGN_AS_FALLBACK -# define optional_CONFIG_ALIGN_AS_FALLBACK double -#endif - -// Compiler detection (C++17 is speculative): - -#define optional_CPP11_OR_GREATER ( __cplusplus >= 201103L ) -#define optional_CPP14_OR_GREATER ( __cplusplus >= 201402L ) -#define optional_CPP17_OR_GREATER ( __cplusplus >= 201700L ) - -// half-open range [lo..hi): -#define optional_BETWEEN( v, lo, hi ) ( lo <= v && v < hi ) - -#if defined(_MSC_VER) && !defined(__clang__) -# define optional_COMPILER_MSVC_VERSION (_MSC_VER / 100 - 5 - (_MSC_VER < 1900)) -#else -# define optional_COMPILER_MSVC_VERSION 0 -#endif - -#if defined __GNUC__ -# define optional_COMPILER_GNUC_VERSION __GNUC__ -#else -# define optional_COMPILER_GNUC_VERSION 0 -#endif - -#if optional_BETWEEN(optional_COMPILER_MSVC_VERSION, 7, 14 ) -# pragma warning( push ) -# pragma warning( disable: 4345 ) // initialization behavior changed -#endif - -#if optional_BETWEEN(optional_COMPILER_MSVC_VERSION, 7, 15 ) -# pragma warning( push ) -# pragma warning( disable: 4814 ) // in C++14 'constexpr' will not imply 'const' -#endif - -// Presence of C++11 language features: - -#if optional_CPP11_OR_GREATER || optional_COMPILER_MSVC_VERSION >= 10 -# define optional_HAVE_AUTO 1 -# define optional_HAVE_NULLPTR 1 -# define optional_HAVE_STATIC_ASSERT 1 -#endif - -#if optional_CPP11_OR_GREATER || optional_COMPILER_MSVC_VERSION >= 12 -# define optional_HAVE_DEFAULT_FUNCTION_TEMPLATE_ARG 1 -# define optional_HAVE_INITIALIZER_LIST 1 -#endif - -#if optional_CPP11_OR_GREATER || optional_COMPILER_MSVC_VERSION >= 14 -# define optional_HAVE_ALIAS_TEMPLATE 1 -# define optional_HAVE_CONSTEXPR_11 1 -# define optional_HAVE_ENUM_CLASS 1 -# define optional_HAVE_EXPLICIT_CONVERSION 1 -# define optional_HAVE_IS_DEFAULT 1 -# define optional_HAVE_IS_DELETE 1 -# define optional_HAVE_NOEXCEPT 1 -# define optional_HAVE_REF_QUALIFIER 1 -#endif - -// Presence of C++14 language features: - -#if optional_CPP14_OR_GREATER -# define optional_HAVE_CONSTEXPR_14 1 -#endif - -// Presence of C++17 language features: - -#if optional_CPP17_OR_GREATER -# define optional_HAVE_ENUM_CLASS_CONSTRUCTION_FROM_UNDERLYING_TYPE 1 -#endif - -// Presence of C++ library features: - -#if optional_COMPILER_GNUC_VERSION -# define optional_HAVE_TR1_TYPE_TRAITS 1 -# define optional_HAVE_TR1_ADD_POINTER 1 -#endif - -#if optional_CPP11_OR_GREATER || optional_COMPILER_MSVC_VERSION >= 9 -# define optional_HAVE_TYPE_TRAITS 1 -# define optional_HAVE_STD_ADD_POINTER 1 -#endif - -#if optional_CPP11_OR_GREATER || optional_COMPILER_MSVC_VERSION >= 11 -# define optional_HAVE_ARRAY 1 -#endif - -#if optional_CPP11_OR_GREATER || optional_COMPILER_MSVC_VERSION >= 12 -# define optional_HAVE_CONDITIONAL 1 -#endif - -#if optional_CPP11_OR_GREATER || optional_COMPILER_MSVC_VERSION >= 14 || (optional_COMPILER_MSVC_VERSION >= 9 && _HAS_CPP0X) -# define optional_HAVE_CONTAINER_DATA_METHOD 1 -#endif - -#if optional_CPP11_OR_GREATER || optional_COMPILER_MSVC_VERSION >= 12 -# define optional_HAVE_REMOVE_CV 1 -#endif - -#if optional_CPP11_OR_GREATER || optional_COMPILER_MSVC_VERSION >= 14 -# define optional_HAVE_SIZED_TYPES 1 -#endif - -// For the rest, consider VC14 as C++11 for variant-lite: - -#if optional_COMPILER_MSVC_VERSION >= 14 -# undef optional_CPP11_OR_GREATER -# define optional_CPP11_OR_GREATER 1 -#endif - -// C++ feature usage: - -#if optional_HAVE_CONSTEXPR_11 -# define optional_constexpr constexpr -#else -# define optional_constexpr /*constexpr*/ -#endif - -#if optional_HAVE_CONSTEXPR_14 -# define optional_constexpr14 constexpr -#else -# define optional_constexpr14 /*constexpr*/ -#endif - -#if optional_HAVE_NOEXCEPT -# define optional_noexcept noexcept -#else -# define optional_noexcept /*noexcept*/ -#endif - -#if optional_HAVE_NULLPTR -# define optional_nullptr nullptr -#else -# define optional_nullptr NULL -#endif - -#if optional_HAVE_REF_QUALIFIER -# define optional_ref_qual & -# define optional_refref_qual && -#else -# define optional_ref_qual /*&*/ -# define optional_refref_qual /*&&*/ -#endif - -// additional includes: - -#if optional_CPP11_OR_GREATER -# include -#endif - -#if optional_HAVE_INITIALIZER_LIST -# include -#endif - -#if optional_HAVE_TYPE_TRAITS -# include -#elif optional_HAVE_TR1_TYPE_TRAITS -# include -#endif - -// -// in_place: code duplicated in any-lite, optional-lite, variant-lite: -// - -#if ! nonstd_lite_HAVE_IN_PLACE_TYPES - -namespace nonstd { - -namespace detail { - -template< class T > -struct in_place_type_tag {}; - -template< std::size_t I > -struct in_place_index_tag {}; - -} // namespace detail - -struct in_place_t {}; - -template< class T > -inline in_place_t in_place( detail::in_place_type_tag = detail::in_place_type_tag() ) -{ - return in_place_t(); -} - -template< std::size_t I > -inline in_place_t in_place( detail::in_place_index_tag = detail::in_place_index_tag() ) -{ - return in_place_t(); -} - -// mimic templated typedef: - -#define nonstd_lite_in_place_type_t( T) nonstd::in_place_t(&)( nonstd::detail::in_place_type_tag ) -#define nonstd_lite_in_place_index_t(T) nonstd::in_place_t(&)( nonstd::detail::in_place_index_tag ) - -#define nonstd_lite_HAVE_IN_PLACE_TYPES 1 - -} // namespace nonstd - -#endif // nonstd_lite_HAVE_IN_PLACE_TYPES - -// -// optional: -// - -namespace nonstd { namespace optional_lite { - -/// class optional - -template< typename T > -class optional; - -namespace detail { - -// C++11 emulation: - -#if variant_HAVE_CONDITIONAL - -using std::conditional; - -#else - -template< bool Cond, class Then, class Else > -struct conditional; - -template< class Then, class Else > -struct conditional< true , Then, Else > { typedef Then type; }; - -template< class Then, class Else > -struct conditional< false, Then, Else > { typedef Else type; }; - -#endif // variant_HAVE_CONDITIONAL - -struct nulltype{}; - -template< typename Head, typename Tail > -struct typelist -{ - typedef Head head; - typedef Tail tail; -}; - -#if optional_CONFIG_MAX_ALIGN_HACK - -// Max align, use most restricted type for alignment: - -#define optional_UNIQUE( name ) optional_UNIQUE2( name, __LINE__ ) -#define optional_UNIQUE2( name, line ) optional_UNIQUE3( name, line ) -#define optional_UNIQUE3( name, line ) name ## line - -#define optional_ALIGN_TYPE( type ) \ - type optional_UNIQUE( _t ); struct_t< type > optional_UNIQUE( _st ) - -template< typename T > -struct struct_t { T _; }; - -union max_align_t -{ - optional_ALIGN_TYPE( char ); - optional_ALIGN_TYPE( short int ); - optional_ALIGN_TYPE( int ); - optional_ALIGN_TYPE( long int ); - optional_ALIGN_TYPE( float ); - optional_ALIGN_TYPE( double ); - optional_ALIGN_TYPE( long double ); - optional_ALIGN_TYPE( char * ); - optional_ALIGN_TYPE( short int * ); - optional_ALIGN_TYPE( int * ); - optional_ALIGN_TYPE( long int * ); - optional_ALIGN_TYPE( float * ); - optional_ALIGN_TYPE( double * ); - optional_ALIGN_TYPE( long double * ); - optional_ALIGN_TYPE( void * ); - -#ifdef HAVE_LONG_LONG - optional_ALIGN_TYPE( long long ); -#endif - - struct Unknown; - - Unknown ( * optional_UNIQUE(_) )( Unknown ); - Unknown * Unknown::* optional_UNIQUE(_); - Unknown ( Unknown::* optional_UNIQUE(_) )( Unknown ); - - struct_t< Unknown ( * )( Unknown) > optional_UNIQUE(_); - struct_t< Unknown * Unknown::* > optional_UNIQUE(_); - struct_t< Unknown ( Unknown::* )(Unknown) > optional_UNIQUE(_); -}; - -#undef optional_UNIQUE -#undef optional_UNIQUE2 -#undef optional_UNIQUE3 - -#undef optional_ALIGN_TYPE - -#elif defined( optional_CONFIG_ALIGN_AS ) // optional_CONFIG_MAX_ALIGN_HACK - -// Use user-specified type for alignment: - -#define optional_ALIGN_AS( unused ) \ - optional_CONFIG_ALIGN_AS - -#else // optional_CONFIG_MAX_ALIGN_HACK - -// Determine POD type to use for alignment: - -#define optional_ALIGN_AS( to_align ) \ - typename type_of_size< alignment_types, alignment_of< to_align >::value >::type - -template -struct alignment_of; - -template -struct alignment_of_hack -{ - char c; - T t; - alignment_of_hack(); -}; - -template -struct alignment_logic -{ - enum { value = A < S ? A : S }; -}; - -template< typename T > -struct alignment_of -{ - enum { value = alignment_logic< - sizeof( alignment_of_hack ) - sizeof(T), sizeof(T) >::value, }; -}; - -template< typename List, size_t N > -struct type_of_size -{ - typedef typename conditional< - N == sizeof( typename List::head ), - typename List::head, - typename type_of_size::type >::type type; -}; - -template< size_t N > -struct type_of_size< nulltype, N > -{ - typedef optional_CONFIG_ALIGN_AS_FALLBACK type; -}; - -template< typename T> -struct struct_t { T _; }; - -#define optional_ALIGN_TYPE( type ) \ - typelist< type , typelist< struct_t< type > - -struct Unknown; - -typedef - optional_ALIGN_TYPE( char ), - optional_ALIGN_TYPE( short ), - optional_ALIGN_TYPE( int ), - optional_ALIGN_TYPE( long ), - optional_ALIGN_TYPE( float ), - optional_ALIGN_TYPE( double ), - optional_ALIGN_TYPE( long double ), - - optional_ALIGN_TYPE( char *), - optional_ALIGN_TYPE( short * ), - optional_ALIGN_TYPE( int * ), - optional_ALIGN_TYPE( long * ), - optional_ALIGN_TYPE( float * ), - optional_ALIGN_TYPE( double * ), - optional_ALIGN_TYPE( long double * ), - - optional_ALIGN_TYPE( Unknown ( * )( Unknown ) ), - optional_ALIGN_TYPE( Unknown * Unknown::* ), - optional_ALIGN_TYPE( Unknown ( Unknown::* )( Unknown ) ), - - nulltype - > > > > > > > > > > > > > > - > > > > > > > > > > > > > > - > > > > > > - alignment_types; - -#undef optional_ALIGN_TYPE - -#endif // optional_CONFIG_MAX_ALIGN_HACK - -/// C++03 constructed union to hold value. - -template< typename T > -union storage_t -{ -private: - friend class optional; - - typedef T value_type; - - storage_t() {} - - storage_t( value_type const & v ) - { - construct_value( v ); - } - - void construct_value( value_type const & v ) - { - ::new( value_ptr() ) value_type( v ); - } - -#if optional_CPP11_OR_GREATER - - storage_t( value_type && v ) - { - construct_value( std::move( v ) ); - } - - void construct_value( value_type && v ) - { - ::new( value_ptr() ) value_type( std::move( v ) ); - } - -#endif - - void destruct_value() - { - value_ptr()->~T(); - } - - value_type const * value_ptr() const - { - return as(); - } - - value_type * value_ptr() - { - return as(); - } - - value_type const & value() const optional_ref_qual - { - return * value_ptr(); - } - - value_type & value() optional_ref_qual - { - return * value_ptr(); - } - -#if optional_CPP11_OR_GREATER - - value_type const && value() const optional_refref_qual - { - return * value_ptr(); - } - - value_type && value() optional_refref_qual - { - return * value_ptr(); - } - -#endif - -#if optional_CPP11_OR_GREATER - - using aligned_storage_t = typename std::aligned_storage< sizeof(value_type), alignof(value_type) >::type; - aligned_storage_t data; - -#elif optional_CONFIG_MAX_ALIGN_HACK - - typedef struct { unsigned char data[ sizeof(value_type) ]; } aligned_storage_t; - - max_align_t hack; - aligned_storage_t data; - -#else - typedef optional_ALIGN_AS(value_type) align_as_type; - - typedef struct { align_as_type data[ 1 + ( sizeof(value_type) - 1 ) / sizeof(align_as_type) ]; } aligned_storage_t; - aligned_storage_t data; - -#undef optional_ALIGN_AS - -#endif // optional_CONFIG_MAX_ALIGN_HACK - - void * ptr() optional_noexcept - { - return &data; - } - - void const * ptr() const optional_noexcept - { - return &data; - } - - template - U * as() - { - return reinterpret_cast( ptr() ); - } - - template - U const * as() const - { - return reinterpret_cast( ptr() ); - } -}; - -} // namespace detail - -/// disengaged state tag - -struct nullopt_t -{ - struct init{}; - optional_constexpr nullopt_t( init ) {} -}; - -#if optional_HAVE_CONSTEXPR_11 -constexpr nullopt_t nullopt{ nullopt_t::init{} }; -#else -// extra parenthesis to prevent the most vexing parse: -const nullopt_t nullopt(( nullopt_t::init() )); -#endif - -/// optional access error - -class bad_optional_access : public std::logic_error -{ -public: - explicit bad_optional_access() - : logic_error( "bad optional access" ) {} -}; - -/// optional - -template< typename T> -class optional -{ -private: - typedef void (optional::*safe_bool)() const; - -public: - typedef T value_type; - - optional_constexpr optional() optional_noexcept - : has_value_( false ) - , contained() - {} - - optional_constexpr optional( nullopt_t ) optional_noexcept - : has_value_( false ) - , contained() - {} - - optional( optional const & rhs ) - : has_value_( rhs.has_value() ) - { - if ( rhs.has_value() ) - contained.construct_value( rhs.contained.value() ); - } - -#if optional_CPP11_OR_GREATER - optional_constexpr14 optional( optional && rhs ) noexcept( std::is_nothrow_move_constructible::value ) - : has_value_( rhs.has_value() ) - { - if ( rhs.has_value() ) - contained.construct_value( std::move( rhs.contained.value() ) ); - } -#endif - - optional_constexpr optional( value_type const & value ) - : has_value_( true ) - , contained( value ) - {} - -#if optional_CPP11_OR_GREATER - - optional_constexpr optional( value_type && value ) - : has_value_( true ) - , contained( std::move( value ) ) - {} - - template< class... Args > - optional_constexpr explicit optional( nonstd_lite_in_place_type_t(T), Args&&... args ) - : has_value_( true ) - , contained( T( std::forward(args)...) ) - {} - - template< class U, class... Args > - optional_constexpr explicit optional( nonstd_lite_in_place_type_t(T), std::initializer_list il, Args&&... args ) - : has_value_( true ) - , contained( T( il, std::forward(args)...) ) - {} - -#endif // optional_CPP11_OR_GREATER - - ~optional() - { - if ( has_value() ) - contained.destruct_value(); - } - - // assignment - - optional & operator=( nullopt_t ) optional_noexcept - { - reset(); - return *this; - } - - optional & operator=( optional const & rhs ) -#if optional_CPP11_OR_GREATER - noexcept( std::is_nothrow_move_assignable::value && std::is_nothrow_move_constructible::value ) -#endif - { - if ( has_value() == true && rhs.has_value() == false ) reset(); - else if ( has_value() == false && rhs.has_value() == true ) initialize( *rhs ); - else if ( has_value() == true && rhs.has_value() == true ) contained.value() = *rhs; - return *this; - } - -#if optional_CPP11_OR_GREATER - - optional & operator=( optional && rhs ) noexcept - { - if ( has_value() == true && rhs.has_value() == false ) reset(); - else if ( has_value() == false && rhs.has_value() == true ) initialize( std::move( *rhs ) ); - else if ( has_value() == true && rhs.has_value() == true ) contained.value() = std::move( *rhs ); - return *this; - } - - template< class U, - typename = typename std::enable_if< std::is_same< typename std::decay::type, T>::value >::type > - optional & operator=( U && v ) - { - if ( has_value() ) contained.value() = std::forward( v ); - else initialize( T( std::forward( v ) ) ); - return *this; - } - - template< class... Args > - void emplace( Args&&... args ) - { - *this = nullopt; - initialize( T( std::forward(args)...) ); - } - - template< class U, class... Args > - void emplace( std::initializer_list il, Args&&... args ) - { - *this = nullopt; - initialize( T( il, std::forward(args)...) ); - } - -#endif // optional_CPP11_OR_GREATER - - // swap - - void swap( optional & rhs ) -#if optional_CPP11_OR_GREATER - noexcept( std::is_nothrow_move_constructible::value && noexcept( std::swap( std::declval(), std::declval() ) ) ) -#endif - { - using std::swap; - if ( has_value() == true && rhs.has_value() == true ) { swap( **this, *rhs ); } - else if ( has_value() == false && rhs.has_value() == true ) { initialize( *rhs ); rhs.reset(); } - else if ( has_value() == true && rhs.has_value() == false ) { rhs.initialize( **this ); reset(); } - } - - // observers - - optional_constexpr value_type const * operator ->() const - { - return assert( has_value() ), - contained.value_ptr(); - } - - optional_constexpr14 value_type * operator ->() - { - return assert( has_value() ), - contained.value_ptr(); - } - - optional_constexpr value_type const & operator *() const optional_ref_qual - { - return assert( has_value() ), - contained.value(); - } - - optional_constexpr14 value_type & operator *() optional_ref_qual - { - return assert( has_value() ), - contained.value(); - } - -#if optional_CPP11_OR_GREATER - - optional_constexpr value_type const && operator *() const optional_refref_qual - { - return assert( has_value() ), std::move( contained.value() ); - } - - optional_constexpr14 value_type && operator *() optional_refref_qual - { - assert( has_value() ); - return std::move( contained.value() ); - } - -#endif - -#if optional_CPP11_OR_GREATER - optional_constexpr explicit operator bool() const optional_noexcept - { - return has_value(); - } -#else - optional_constexpr operator safe_bool() const optional_noexcept - { - return has_value() ? &optional::this_type_does_not_support_comparisons : 0; - } -#endif - - optional_constexpr bool has_value() const optional_noexcept - { - return has_value_; - } - - optional_constexpr14 value_type const & value() const optional_ref_qual - { - if ( ! has_value() ) - throw bad_optional_access(); - - return contained.value(); - } - - optional_constexpr14 value_type & value() optional_ref_qual - { - if ( ! has_value() ) - throw bad_optional_access(); - - return contained.value(); - } - -#if optional_HAVE_REF_QUALIFIER - - optional_constexpr14 value_type const && value() const optional_refref_qual - { - if ( ! has_value() ) - throw bad_optional_access(); - - return std::move( contained.value() ); - } - - optional_constexpr14 value_type && value() optional_refref_qual - { - if ( ! has_value() ) - throw bad_optional_access(); - - return std::move( contained.value() ); - } - -#endif - -#if optional_CPP11_OR_GREATER - - template< class U > - optional_constexpr value_type value_or( U && v ) const optional_ref_qual - { - return has_value() ? contained.value() : static_cast(std::forward( v ) ); - } - - template< class U > - optional_constexpr value_type value_or( U && v ) const optional_refref_qual - { - return has_value() ? std::move( contained.value() ) : static_cast(std::forward( v ) ); - } - -#else - - template< class U > - optional_constexpr value_type value_or( U const & v ) const - { - return has_value() ? contained.value() : static_cast( v ); - } - -#endif // optional_CPP11_OR_GREATER - - // modifiers - - void reset() optional_noexcept - { - if ( has_value() ) - contained.destruct_value(); - - has_value_ = false; - } - -private: - void this_type_does_not_support_comparisons() const {} - - template< typename V > - void initialize( V const & value ) - { - assert( ! has_value() ); - contained.construct_value( value ); - has_value_ = true; - } - -#if optional_CPP11_OR_GREATER - template< typename V > - void initialize( V && value ) - { - assert( ! has_value() ); - contained.construct_value( std::move( value ) ); - has_value_ = true; - } -#endif - -private: - bool has_value_; - detail::storage_t< value_type > contained; - -}; - -// Relational operators - -template< typename T > bool operator==( optional const & x, optional const & y ) -{ - return bool(x) != bool(y) ? false : bool(x) == false ? true : *x == *y; -} - -template< typename T > bool operator!=( optional const & x, optional const & y ) -{ - return !(x == y); -} - -template< typename T > bool operator<( optional const & x, optional const & y ) -{ - return (!y) ? false : (!x) ? true : *x < *y; -} - -template< typename T > bool operator>( optional const & x, optional const & y ) -{ - return (y < x); -} - -template< typename T > bool operator<=( optional const & x, optional const & y ) -{ - return !(y < x); -} - -template< typename T > bool operator>=( optional const & x, optional const & y ) -{ - return !(x < y); -} - -// Comparison with nullopt - -template< typename T > bool operator==( optional const & x, nullopt_t ) optional_noexcept -{ - return (!x); -} - -template< typename T > bool operator==( nullopt_t, optional const & x ) optional_noexcept -{ - return (!x); -} - -template< typename T > bool operator!=( optional const & x, nullopt_t ) optional_noexcept -{ - return bool(x); -} - -template< typename T > bool operator!=( nullopt_t, optional const & x ) optional_noexcept -{ - return bool(x); -} - -template< typename T > bool operator<( optional const &, nullopt_t ) optional_noexcept -{ - return false; -} - -template< typename T > bool operator<( nullopt_t, optional const & x ) optional_noexcept -{ - return bool(x); -} - -template< typename T > bool operator<=( optional const & x, nullopt_t ) optional_noexcept -{ - return (!x); -} - -template< typename T > bool operator<=( nullopt_t, optional const & ) optional_noexcept -{ - return true; -} - -template< typename T > bool operator>( optional const & x, nullopt_t ) optional_noexcept -{ - return bool(x); -} - -template< typename T > bool operator>( nullopt_t, optional const & ) optional_noexcept -{ - return false; -} - -template< typename T > bool operator>=( optional const &, nullopt_t ) -{ - return true; -} - -template< typename T > bool operator>=( nullopt_t, optional const & x ) -{ - return (!x); -} - -// Comparison with T - -template< typename T > bool operator==( optional const & x, const T& v ) -{ - return bool(x) ? *x == v : false; -} - -template< typename T > bool operator==( T const & v, optional const & x ) -{ - return bool(x) ? v == *x : false; -} - -template< typename T > bool operator!=( optional const & x, const T& v ) -{ - return bool(x) ? *x != v : true; -} - -template< typename T > bool operator!=( T const & v, optional const & x ) -{ - return bool(x) ? v != *x : true; -} - -template< typename T > bool operator<( optional const & x, const T& v ) -{ - return bool(x) ? *x < v : true; -} - -template< typename T > bool operator<( T const & v, optional const & x ) -{ - return bool(x) ? v < *x : false; -} - -template< typename T > bool operator<=( optional const & x, const T& v ) -{ - return bool(x) ? *x <= v : true; -} - -template< typename T > bool operator<=( T const & v, optional const & x ) -{ - return bool(x) ? v <= *x : false; -} - -template< typename T > bool operator>( optional const & x, const T& v ) -{ - return bool(x) ? *x > v : false; -} - -template< typename T > bool operator>( T const & v, optional const & x ) -{ - return bool(x) ? v > *x : true; -} - -template< typename T > bool operator>=( optional const & x, const T& v ) -{ - return bool(x) ? *x >= v : false; -} - -template< typename T > bool operator>=( T const & v, optional const & x ) -{ - return bool(x) ? v >= *x : true; -} - -// Specialized algorithms - -template< typename T > -void swap( optional & x, optional & y ) -#if optional_CPP11_OR_GREATER - noexcept( noexcept( x.swap(y) ) ) -#endif -{ - x.swap( y ); -} - -#if optional_CPP11_OR_GREATER - -template< class T > -optional_constexpr optional< typename std::decay::type > make_optional( T && v ) -{ - return optional< typename std::decay::type >( std::forward( v ) ); -} - -template< class T, class...Args > -optional_constexpr optional make_optional( Args&&... args ) -{ - return optional( in_place, std::forward(args)...); -} - -template< class T, class U, class... Args > -optional_constexpr optional make_optional( std::initializer_list il, Args&&... args ) -{ - return optional( in_place, il, std::forward(args)...); -} - -#else - -template< typename T > -optional make_optional( T const & v ) -{ - return optional( v ); -} - -#endif // optional_CPP11_OR_GREATER - -} // namespace optional - -using namespace optional_lite; - -} // namespace nonstd - -#if optional_CPP11_OR_GREATER - -// specialize the std::hash algorithm: - -namespace std { - -template< class T > -struct hash< nonstd::optional > -{ -public: - std::size_t operator()( nonstd::optional const & v ) const optional_noexcept - { - return bool( v ) ? hash()( *v ) : 0; - } -}; - -} //namespace std - -#endif // optional_CPP11_OR_GREATER - -#endif // NONSTD_OPTIONAL_LITE_HPP diff --git a/src/solvers/flattening/boolbv_overflow.cpp b/src/solvers/flattening/boolbv_overflow.cpp index f9a0a3ea188..dcebd389089 100644 --- a/src/solvers/flattening/boolbv_overflow.cpp +++ b/src/solvers/flattening/boolbv_overflow.cpp @@ -118,7 +118,7 @@ literalt boolbvt::convert_binary_overflow(const binary_overflow_exprt &expr) expr.rhs(), can_cast_expr(expr) ? optionalt{bv0.size()} - : nullopt); + : std::nullopt); const bv_utilst::representationt rep = can_cast_type(expr.lhs().type()) diff --git a/src/solvers/flattening/boolbv_width.h b/src/solvers/flattening/boolbv_width.h index d50c433109e..24c8909fe00 100644 --- a/src/solvers/flattening/boolbv_width.h +++ b/src/solvers/flattening/boolbv_width.h @@ -32,7 +32,7 @@ class boolbv_widtht { const auto &entry_opt = get_entry(type); if(!entry_opt.has_value()) - return {}; + return std::nullopt; return entry_opt->total_width; } diff --git a/src/solvers/strings/string_dependencies.h b/src/solvers/strings/string_dependencies.h index 03a455117eb..ce06aa64143 100644 --- a/src/solvers/strings/string_dependencies.h +++ b/src/solvers/strings/string_dependencies.h @@ -164,8 +164,7 @@ class string_dependenciest // NOLINTNEXTLINE(readability/identifiers) struct node_hash { - size_t - operator()(const string_dependenciest::nodet &node) const optional_noexcept + size_t operator()(const string_dependenciest::nodet &node) const { return 2 * node.index + (node.kind == string_dependenciest::nodet::STRING ? 0 : 1); diff --git a/src/util/arith_tools.h b/src/util/arith_tools.h index 9d80873b30c..d5aa518b05d 100644 --- a/src/util/arith_tools.h +++ b/src/util/arith_tools.h @@ -94,7 +94,7 @@ struct numeric_castt(get_val(mpi)); else - return {}; + return std::nullopt; } // Conversion from expression @@ -103,7 +103,7 @@ struct numeric_castt{}(to_constant_expr(expr)); else - return {}; + return std::nullopt; } // Conversion from expression @@ -112,7 +112,7 @@ struct numeric_castt{}(expr)) return numeric_castt{}(*mpi_opt); else - return {}; + return std::nullopt; } }; diff --git a/src/util/module_dependencies.txt b/src/util/module_dependencies.txt index a0f86e99c8f..5300da7dfd3 100644 --- a/src/util/module_dependencies.txt +++ b/src/util/module_dependencies.txt @@ -1,6 +1,5 @@ big-int mach # system malloc # system -nonstd sys # system util diff --git a/src/util/numbering.h b/src/util/numbering.h index ea9fc6e94eb..b12ae04e6f3 100644 --- a/src/util/numbering.h +++ b/src/util/numbering.h @@ -52,7 +52,7 @@ class numberingt final const auto it = numbers_.find(a); if(it == numbers_.end()) { - return {}; + return std::nullopt; } return it->second; } diff --git a/src/util/optional.h b/src/util/optional.h index 3581e3d9f31..0a47ad5f817 100644 --- a/src/util/optional.h +++ b/src/util/optional.h @@ -1,7 +1,7 @@ /*******************************************************************\ -Module: typedef for optional class template. To be replaced with - std::optional once C++17 support is enabled +Module: typedef for optional class template. New code should directly + use std::optional. Author: Diffblue Ltd. @@ -10,49 +10,9 @@ Author: Diffblue Ltd. #ifndef CPROVER_UTIL_OPTIONAL_H #define CPROVER_UTIL_OPTIONAL_H -#if defined __clang__ - #pragma clang diagnostic push ignore "-Wall" - #pragma clang diagnostic push ignore "-Wpedantic" -#elif defined __GNUC__ - #pragma GCC diagnostic push ignore "-Wall" - #pragma GCC diagnostic push ignore "-Wpedantic" -#elif defined _MSC_VER - #pragma warning(push) -#endif -#include -#if defined __clang__ - #pragma clang diagnostic pop - #pragma clang diagnostic pop -#elif defined __GNUC__ - #pragma GCC diagnostic pop - #pragma GCC diagnostic pop -#elif defined _MSC_VER - #pragma warning(pop) -#endif +#include -// Swap for std::optional when switching to C++17 -template -using optionalt=nonstd::optional; // NOLINT template typedef - -typedef nonstd::bad_optional_access bad_optional_accesst; - -using nonstd::nullopt; - -/// Similar to optionalt::value but in case of empty optional, generates an -/// invariant failure instead of throwing an exception. -template -T &get_value_or_abort(optionalt &opt) -{ - PRECONDITION(opt.has_value()); - return opt.value(); -} - -/// \copydoc get_value_or_abort(optionalt &) template -const T &get_value_or_abort(const optionalt &opt) -{ - PRECONDITION(opt.has_value()); - return opt.value(); -} +using optionalt = std::optional; // NOLINT template typedef #endif // CPROVER_UTIL_OPTIONAL_H diff --git a/src/util/sharing_map.h b/src/util/sharing_map.h index 48158b29887..a45b693fad7 100644 --- a/src/util/sharing_map.h +++ b/src/util/sharing_map.h @@ -1454,7 +1454,7 @@ SHARING_MAPT2(optionalt>)::find( const nodet *lp = get_leaf_node(k); if(lp == nullptr) - return {}; + return std::nullopt; return optionalt>(lp->get_value()); } diff --git a/src/util/string2int.h b/src/util/string2int.h index ff6737aa688..0d9d71defe8 100644 --- a/src/util/string2int.h +++ b/src/util/string2int.h @@ -94,11 +94,11 @@ auto wrap_string_conversion(do_conversiont do_conversion) } catch(const std::invalid_argument &) { - return nullopt; + return std::nullopt; } catch(const std::out_of_range &) { - return nullopt; + return std::nullopt; } } diff --git a/unit/Makefile b/unit/Makefile index 208c3bc3a36..de364726e36 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -170,7 +170,6 @@ SRC += analyses/ai/ai.cpp \ util/lower_byte_operators.cpp \ util/memory_info.cpp \ util/message.cpp \ - util/optional.cpp \ util/optional_utils.cpp \ util/parse_options.cpp \ util/piped_process.cpp \ diff --git a/unit/util/optional.cpp b/unit/util/optional.cpp deleted file mode 100644 index bbaf6c6a97e..00000000000 --- a/unit/util/optional.cpp +++ /dev/null @@ -1,32 +0,0 @@ -/*******************************************************************\ - -Module: nonstd::optional unit tests - -Author: Diffblue Ltd. - -\*******************************************************************/ - -#include -#include - -TEST_CASE("Optional without a value", "[core][util][optional]") -{ - optionalt maybe_value; - REQUIRE(!maybe_value.has_value()); - REQUIRE_THROWS_AS(maybe_value.value(), bad_optional_accesst); -} - -TEST_CASE("Optional with a value", "[core][util][optional]") -{ - optionalt maybe_value=false; - REQUIRE(maybe_value.has_value()); - REQUIRE(!maybe_value.value()); -} - - -TEST_CASE("Optional with a value (operator access)", "[core][util][optional]") -{ - optionalt maybe_value=true; - REQUIRE(maybe_value.has_value()); - REQUIRE(*maybe_value); -} From 56046a5195fadfa824fe312f55e8628d1f2ff597 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 23 Mar 2022 23:46:16 +0000 Subject: [PATCH 2/7] Remove util_make_unique With the move to C++ 17 we can use std::make_unique instead. --- .../src/janalyzer/janalyzer_parse_options.cpp | 2 +- .../java_bytecode/java_bytecode_language.cpp | 2 +- .../java_bytecode/java_bytecode_language.h | 5 +- jbmc/src/java_bytecode/java_qualifiers.cpp | 4 +- jbmc/src/jbmc/jbmc_parse_options.cpp | 17 +++---- src/analyses/ai.h | 11 ++-- src/analyses/ai_domain.h | 7 ++- src/analyses/dependence_graph.cpp | 4 +- src/analyses/goto_rw.cpp | 5 +- src/analyses/invariant_propagation.cpp | 4 +- src/analyses/local_may_alias.h | 3 +- src/analyses/reaching_definitions.cpp | 11 ++-- .../abstract_value_object.cpp | 7 ++- .../abstract_value_object.h | 2 +- .../constant_abstract_value.cpp | 2 +- .../interval_abstract_value.cpp | 3 +- .../value_set_abstract_object.cpp | 5 +- .../variable_sensitivity_dependence_graph.cpp | 8 +-- .../variable_sensitivity_domain.h | 2 +- src/ansi-c/ansi_c_language.cpp | 2 +- src/ansi-c/ansi_c_language.h | 6 +-- src/ansi-c/c_qualifiers.cpp | 3 +- src/ansi-c/goto_check_c.cpp | 3 +- src/cbmc/cbmc_parse_options.cpp | 17 +++---- src/cpp/cpp_language.cpp | 2 +- src/cpp/cpp_language.h | 6 +-- src/goto-analyzer/build_analyzer.cpp | 36 ++++++------- src/goto-checker/bmc_util.cpp | 7 ++- .../single_path_symex_checker.cpp | 2 +- src/goto-checker/solver_factory.cpp | 51 +++++++++---------- .../function_call_harness_generator.cpp | 5 +- .../goto_harness_parse_options.cpp | 5 +- .../enumerating_loop_acceleration.h | 4 +- .../accelerate/scratch_program.h | 3 +- src/goto-instrument/cover.cpp | 43 +++++++--------- src/goto-instrument/cover.h | 3 +- .../generate_function_bodies.cpp | 13 +++-- src/goto-symex/path_storage.cpp | 5 +- src/goto-symex/symex_main.cpp | 3 +- src/goto-synthesizer/cegis_verifier.cpp | 2 +- src/jsil/jsil_language.cpp | 2 +- src/jsil/jsil_language.h | 6 +-- .../json_symtab_language.h | 5 +- src/libcprover-cpp/api.cpp | 14 ++--- src/libcprover-cpp/api_options.cpp | 3 +- src/libcprover-cpp/verification_result.cpp | 5 +- src/pointer-analysis/value_set_analysis.h | 2 +- src/solvers/sat/satcheck_glucose.cpp | 3 +- src/solvers/sat/satcheck_minisat2.cpp | 3 +- .../encoding/struct_encoding.cpp | 5 +- src/solvers/strings/string_dependencies.cpp | 21 ++++---- .../statement_list_language.cpp | 5 +- src/util/make_unique.h | 24 --------- src/util/piped_process.cpp | 3 +- src/util/range.h | 8 +-- src/util/sharing_node.h | 1 - src/util/ui_message.cpp | 3 +- .../smt2_incremental_decision_procedure.cpp | 3 +- 58 files changed, 188 insertions(+), 253 deletions(-) delete mode 100644 src/util/make_unique.h diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index aeabc8f7650..f43be1dca9e 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/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(lazy_goto_model.symbol_table); + std::make_unique(lazy_goto_model.symbol_table); log.status() << "Generating GOTO Program" << messaget::eom; lazy_goto_model.load_all_functions(); diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index dd19585c248..2b7cefc2abd 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -1517,7 +1517,7 @@ void java_bytecode_languaget::show_parse(std::ostream &out) std::unique_ptr new_java_bytecode_language() { - return util_make_unique(); + return std::make_unique(); } bool java_bytecode_languaget::from_expr( diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index 22189337dc1..a63a0572f1a 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H #include -#include #include #include // IWYU pragma: keep @@ -319,7 +318,9 @@ class java_bytecode_languaget:public languaget const namespacet &ns) override; std::unique_ptr new_language() override - { return util_make_unique(); } + { + return std::make_unique(); + } std::string id() const override { return "java"; } std::string description() const override { return "Java Bytecode"; } diff --git a/jbmc/src/java_bytecode/java_qualifiers.cpp b/jbmc/src/java_bytecode/java_qualifiers.cpp index 37b4b894b08..c462e5471f8 100644 --- a/jbmc/src/java_bytecode/java_qualifiers.cpp +++ b/jbmc/src/java_bytecode/java_qualifiers.cpp @@ -8,8 +8,6 @@ #include #include -#include - #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 java_qualifierst::clone() const { - auto other = util_make_unique(ns); + auto other = std::make_unique(ns); *other = *this; return std::move(other); } diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index ef776c63f3c..82d940222d1 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -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>( + std::make_unique>( 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>( options, ui_message_handler, *goto_model_ptr); } else { - verifier = util_make_unique< + verifier = std::make_unique< stop_on_fail_verifiert>( 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>( 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>( options, ui_message_handler, *goto_model_ptr); } else { - verifier = util_make_unique>( 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(lazy_goto_model.symbol_table); + std::make_unique(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(std::move(lazy_goto_model)); + std::make_unique(std::move(lazy_goto_model)); } log.status() << config.object_bits_info() << messaget::eom; diff --git a/src/analyses/ai.h b/src/analyses/ai.h index 090784f4759..a4f0bc34e69 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -50,7 +50,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -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>(), - util_make_unique>(), - util_make_unique(), + std::make_unique>(), + std::make_unique(), no_logging) { } explicit ait(std::unique_ptr &&df) : ai_recursive_interproceduralt( - util_make_unique< + std::make_unique< ai_history_factory_default_constructort>(), std::move(df), - util_make_unique(), + std::make_unique(), no_logging) { } diff --git a/src/analyses/ai_domain.h b/src/analyses/ai_domain.h index 13195ae052e..85d6dcb1dfb 100644 --- a/src/analyses/ai_domain.h +++ b/src/analyses/ai_domain.h @@ -41,7 +41,6 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_ANALYSES_AI_DOMAIN_H #include -#include #include #include "ai_history.h" @@ -206,7 +205,7 @@ class ai_domain_factoryt : public ai_domain_factory_baset std::unique_ptr copy(const statet &s) const override { - return util_make_unique(static_cast(s)); + return std::make_unique(static_cast(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 make(locationt l) const override { - auto d = util_make_unique(); + auto d = std::make_unique(); CHECK_RETURN(d->is_bottom()); return std::unique_ptr(d.release()); } @@ -246,7 +245,7 @@ class ai_domain_factory_location_constructort std::unique_ptr make(locationt l) const override { - auto d = util_make_unique(l); + auto d = std::make_unique(l); CHECK_RETURN(d->is_bottom()); return std::unique_ptr(d.release()); } diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index a95d0064a72..621dbdfeeb8 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -349,7 +349,7 @@ class dep_graph_domain_factoryt : public ai_domain_factoryt { auto node_id = dg.add_node(); dg.nodes[node_id].PC = l; - auto p = util_make_unique(node_id); + auto p = std::make_unique(node_id); CHECK_RETURN(p->is_bottom()); return std::unique_ptr(p.release()); @@ -360,7 +360,7 @@ class dep_graph_domain_factoryt : public ai_domain_factoryt }; dependence_grapht::dependence_grapht(const namespacet &_ns) - : ait(util_make_unique(*this)), + : ait(std::make_unique(*this)), ns(_ns), rd(ns) { diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index 0c75177dfda..0f81ecaf632 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -15,7 +15,6 @@ Date: April 2010 #include #include #include -#include #include #include #include @@ -528,7 +527,7 @@ void rw_range_sett::add( .first; if(entry->second==nullptr) - entry->second=util_make_unique(); + entry->second = std::make_unique(); static_cast(*entry->second).push_back( {range_start, range_end}); @@ -766,7 +765,7 @@ void rw_guarded_range_set_value_sett::add( .first; if(entry->second==nullptr) - entry->second=util_make_unique(); + entry->second = std::make_unique(); static_cast(*entry->second).insert( {range_start, {range_end, guard.as_expr()}}); diff --git a/src/analyses/invariant_propagation.cpp b/src/analyses/invariant_propagation.cpp index ff90f398e9b..a7cc24007b1 100644 --- a/src/analyses/invariant_propagation.cpp +++ b/src/analyses/invariant_propagation.cpp @@ -25,7 +25,7 @@ class invariant_set_domain_factoryt std::unique_ptr make(locationt l) const override { - auto p = util_make_unique( + auto p = std::make_unique( ip.value_sets, ip.object_store, ip.ns); CHECK_RETURN(p->is_bottom()); @@ -40,7 +40,7 @@ invariant_propagationt::invariant_propagationt( const namespacet &_ns, value_setst &_value_sets) : ait( - util_make_unique(*this)), + std::make_unique(*this)), ns(_ns), value_sets(_value_sets), object_store(_ns) diff --git a/src/analyses/local_may_alias.h b/src/analyses/local_may_alias.h index eb86ff93329..febc741dbae 100644 --- a/src/analyses/local_may_alias.h +++ b/src/analyses/local_may_alias.h @@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include "locals.h" #include "dirty.h" @@ -120,7 +119,7 @@ class local_may_alias_factoryt goto_functionst::function_mapt::const_iterator f_it2= goto_functions->function_map.find(fkt); CHECK_RETURN(f_it2 != goto_functions->function_map.end()); - return *(fkt_map[fkt]=util_make_unique(f_it2->second)); + return *(fkt_map[fkt] = std::make_unique(f_it2->second)); } local_may_aliast &operator()(goto_programt::const_targett t) diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index 0b2ccf42f68..5dc71d4aab4 100644 --- a/src/analyses/reaching_definitions.cpp +++ b/src/analyses/reaching_definitions.cpp @@ -16,7 +16,6 @@ Date: February 2013 #include "reaching_definitions.h" #include // IWYU pragma: keep -#include #include #include @@ -41,7 +40,7 @@ class rd_range_domain_factoryt : public ai_domain_factoryt std::unique_ptr make(locationt) const override { - auto p = util_make_unique(bv_container); + auto p = std::make_unique(bv_container); CHECK_RETURN(p->is_bottom()); return std::unique_ptr(p.release()); } @@ -53,7 +52,7 @@ class rd_range_domain_factoryt : public ai_domain_factoryt reaching_definitions_analysist::reaching_definitions_analysist( const namespacet &_ns) : concurrency_aware_ait( - util_make_unique(this)), + std::make_unique(this)), ns(_ns) { } @@ -734,13 +733,13 @@ const rd_range_domaint::ranges_at_loct &rd_range_domaint::get( void reaching_definitions_analysist::initialize( const goto_functionst &goto_functions) { - auto value_sets_=util_make_unique(ns); + auto value_sets_ = std::make_unique(ns); (*value_sets_)(goto_functions); value_sets=std::move(value_sets_); - is_threaded=util_make_unique(goto_functions); + is_threaded = std::make_unique(goto_functions); - is_dirty=util_make_unique(goto_functions); + is_dirty = std::make_unique(goto_functions); concurrency_aware_ait::initialize(goto_functions); } diff --git a/src/analyses/variable-sensitivity/abstract_value_object.cpp b/src/analyses/variable-sensitivity/abstract_value_object.cpp index b21130cdebf..aa4c94c21c9 100644 --- a/src/analyses/variable-sensitivity/abstract_value_object.cpp +++ b/src/analyses/variable-sensitivity/abstract_value_object.cpp @@ -9,7 +9,6 @@ #include #include #include -#include #include #include @@ -76,12 +75,12 @@ bool single_value_index_ranget::advance_to_next() index_range_implementation_ptrt make_empty_index_range() { - return util_make_unique(); + return std::make_unique(); } index_range_implementation_ptrt make_indeterminate_index_range() { - return util_make_unique(); + return std::make_unique(); } class single_value_value_ranget : public value_range_implementationt @@ -115,7 +114,7 @@ class single_value_value_ranget : public value_range_implementationt value_range_implementation_ptrt make_single_value_range(const abstract_object_pointert &value) { - return util_make_unique(value); + return std::make_unique(value); } static abstract_object_pointert constants_expression_transform( diff --git a/src/analyses/variable-sensitivity/abstract_value_object.h b/src/analyses/variable-sensitivity/abstract_value_object.h index 924fe76595c..1bd2f1dcff9 100644 --- a/src/analyses/variable-sensitivity/abstract_value_object.h +++ b/src/analyses/variable-sensitivity/abstract_value_object.h @@ -229,7 +229,7 @@ class empty_value_ranget : public value_range_implementationt } value_range_implementation_ptrt reset() const override { - return util_make_unique(); + return std::make_unique(); } private: diff --git a/src/analyses/variable-sensitivity/constant_abstract_value.cpp b/src/analyses/variable-sensitivity/constant_abstract_value.cpp index 0c59b7c796c..32d46f06f6f 100644 --- a/src/analyses/variable-sensitivity/constant_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/constant_abstract_value.cpp @@ -34,7 +34,7 @@ class constant_index_ranget : public single_value_index_ranget static index_range_implementation_ptrt make_constant_index_range(const exprt &val) { - return util_make_unique(val); + return std::make_unique(val); } constant_abstract_valuet::constant_abstract_valuet(const exprt &e) diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index 3931e12beb9..5f3c6affb4f 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -12,7 +12,6 @@ #include #include #include -#include #include #include "abstract_environment.h" @@ -72,7 +71,7 @@ static index_range_implementation_ptrt make_interval_index_range( const constant_interval_exprt &interval, const namespacet &n) { - return util_make_unique(interval, n); + return std::make_unique(interval, n); } static inline bool diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index cd78b90554f..5357fc3046a 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -10,7 +10,6 @@ /// Value Set Abstract Object #include -#include #include #include @@ -62,7 +61,7 @@ class value_set_index_ranget : public index_range_implementationt static index_range_implementation_ptrt make_value_set_index_range(const std::set &vals) { - return util_make_unique(vals); + return std::make_unique(vals); } static value_range_implementation_ptrt @@ -104,7 +103,7 @@ class value_set_value_ranget : public value_range_implementationt static value_range_implementation_ptrt make_value_set_value_range(const abstract_object_sett &vals) { - return util_make_unique(vals); + return std::make_unique(vals); } static abstract_object_sett diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp index df2bbc557ab..80afe243632 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp @@ -617,7 +617,7 @@ class variable_sensitivity_dependence_domain_factoryt { auto node_id = dg.add_node(); dg.nodes[node_id].PC = l; - auto p = util_make_unique( + auto p = std::make_unique( node_id, object_factory, configuration); CHECK_RETURN(p->is_bottom()); @@ -637,12 +637,12 @@ variable_sensitivity_dependence_grapht::variable_sensitivity_dependence_grapht( const vsd_configt &configuration, message_handlert &message_handler) : ai_three_way_merget( - util_make_unique>(), - util_make_unique( + std::make_unique>(), + std::make_unique( *this, object_factory, configuration), - util_make_unique(), + std::make_unique(), message_handler), goto_functions(goto_functions), ns(_ns) diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h index f2f54706011..707de155078 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h +++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h @@ -264,7 +264,7 @@ class variable_sensitivity_domain_factoryt std::unique_ptr make(locationt l) const override { - auto d = util_make_unique( + auto d = std::make_unique( object_factory, configuration); CHECK_RETURN(d->is_bottom()); return std::unique_ptr(d.release()); diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp index cf82835ceb8..4dea6f2642e 100644 --- a/src/ansi-c/ansi_c_language.cpp +++ b/src/ansi-c/ansi_c_language.cpp @@ -150,7 +150,7 @@ void ansi_c_languaget::show_parse(std::ostream &out) std::unique_ptr new_ansi_c_language() { - return util_make_unique(); + return std::make_unique(); } bool ansi_c_languaget::from_expr( diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h index db80e687549..5b7435e786f 100644 --- a/src/ansi-c/ansi_c_language.h +++ b/src/ansi-c/ansi_c_language.h @@ -12,8 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include - #include #include "ansi_c_parse_tree.h" @@ -101,7 +99,9 @@ class ansi_c_languaget:public languaget const namespacet &ns) override; std::unique_ptr new_language() override - { return util_make_unique(); } + { + return std::make_unique(); + } std::string id() const override { return "C"; } std::string description() const override { return "ANSI-C 99"; } diff --git a/src/ansi-c/c_qualifiers.cpp b/src/ansi-c/c_qualifiers.cpp index 78d178bc94c..780ec12be5c 100644 --- a/src/ansi-c/c_qualifiers.cpp +++ b/src/ansi-c/c_qualifiers.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "c_qualifiers.h" -#include #include c_qualifierst &c_qualifierst::operator=(const c_qualifierst &other) @@ -26,7 +25,7 @@ c_qualifierst &c_qualifierst::operator=(const c_qualifierst &other) std::unique_ptr c_qualifierst::clone() const { - auto other = util_make_unique(); + auto other = std::make_unique(); *other = *this; return std::move(other); } diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index 0d936ef0f03..59915865a0b 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -22,7 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -2022,7 +2021,7 @@ void goto_check_ct::goto_check( bool did_something = false; local_bitvector_analysis = - util_make_unique(goto_function, ns); + std::make_unique(goto_function, ns); goto_programt &goto_program = goto_function.body; diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index e310b2a623e..6f090945d35 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -641,13 +640,13 @@ int cbmc_parse_optionst::doit() { if(options.get_bool_option("stop-on-fail")) { - verifier = util_make_unique< + verifier = std::make_unique< stop_on_fail_verifiert>( options, ui_message_handler, goto_model); } else { - verifier = util_make_unique>( options, ui_message_handler, goto_model); } @@ -656,7 +655,7 @@ int cbmc_parse_optionst::doit() options.get_bool_option("stop-on-fail") && options.get_bool_option("paths")) { verifier = - util_make_unique>( + std::make_unique>( options, ui_message_handler, goto_model); } else if( @@ -666,13 +665,13 @@ int cbmc_parse_optionst::doit() if(options.get_bool_option("localize-faults")) { verifier = - util_make_unique>(options, ui_message_handler, goto_model); } else { verifier = - util_make_unique>( + std::make_unique>( options, ui_message_handler, goto_model); } } @@ -680,7 +679,7 @@ int cbmc_parse_optionst::doit() !options.get_bool_option("stop-on-fail") && options.get_bool_option("paths")) { - verifier = util_make_unique< + verifier = std::make_unique< all_properties_verifier_with_trace_storaget>( options, ui_message_handler, goto_model); } @@ -691,12 +690,12 @@ int cbmc_parse_optionst::doit() if(options.get_bool_option("localize-faults")) { verifier = - util_make_unique>(options, ui_message_handler, goto_model); } else { - verifier = util_make_unique< + verifier = std::make_unique< all_properties_verifier_with_trace_storaget>( options, ui_message_handler, goto_model); } diff --git a/src/cpp/cpp_language.cpp b/src/cpp/cpp_language.cpp index 2e2119d83c8..7b8880d824b 100644 --- a/src/cpp/cpp_language.cpp +++ b/src/cpp/cpp_language.cpp @@ -197,7 +197,7 @@ void cpp_languaget::show_parse( std::unique_ptr new_cpp_language() { - return util_make_unique(); + return std::make_unique(); } bool cpp_languaget::from_expr( diff --git a/src/cpp/cpp_language.h b/src/cpp/cpp_language.h index a2133f9cf95..12e48ecce19 100644 --- a/src/cpp/cpp_language.h +++ b/src/cpp/cpp_language.h @@ -16,8 +16,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include -#include // unique_ptr - #include #include "cpp_parse_tree.h" @@ -81,7 +79,9 @@ class cpp_languaget:public languaget const namespacet &ns) override; std::unique_ptr new_language() override - { return util_make_unique(); } + { + return std::make_unique(); + } std::string id() const override { return "cpp"; } std::string description() const override { return "C++"; } diff --git a/src/goto-analyzer/build_analyzer.cpp b/src/goto-analyzer/build_analyzer.cpp index 9d9e44e318a..1b110e78dba 100644 --- a/src/goto-analyzer/build_analyzer.cpp +++ b/src/goto-analyzer/build_analyzer.cpp @@ -45,17 +45,17 @@ std::unique_ptr build_analyzer( std::unique_ptr hf = nullptr; if(options.get_bool_option("ahistorical")) { - hf = util_make_unique< + hf = std::make_unique< ai_history_factory_default_constructort>(); } else if(options.get_bool_option("call-stack")) { - hf = util_make_unique( + hf = std::make_unique( options.get_unsigned_int_option("call-stack-recursion-limit")); } else if(options.get_bool_option("local-control-flow-history")) { - hf = util_make_unique( + hf = std::make_unique( options.get_bool_option("local-control-flow-history-forward"), options.get_bool_option("local-control-flow-history-backward"), options.get_unsigned_int_option("local-control-flow-history-limit")); @@ -65,17 +65,17 @@ std::unique_ptr build_analyzer( std::unique_ptr df = nullptr; if(options.get_bool_option("constants")) { - df = util_make_unique< + df = std::make_unique< ai_domain_factory_default_constructort>(); } else if(options.get_bool_option("intervals")) { - df = util_make_unique< + df = std::make_unique< ai_domain_factory_default_constructort>(); } else if(options.get_bool_option("vsd")) { - df = util_make_unique( + df = std::make_unique( vs_object_factory, vsd_config); } // non-null is not fully supported, despite the historical options @@ -86,11 +86,11 @@ std::unique_ptr build_analyzer( std::unique_ptr st = nullptr; if(options.get_bool_option("one-domain-per-history")) { - st = util_make_unique(); + st = std::make_unique(); } else if(options.get_bool_option("one-domain-per-location")) { - st = util_make_unique(); + st = std::make_unique(); } // Only try to build the abstract interpreter if all the parts have been @@ -99,7 +99,7 @@ std::unique_ptr build_analyzer( { if(options.get_bool_option("recursive-interprocedural")) { - return util_make_unique( + return std::make_unique( std::move(hf), std::move(df), std::move(st), mh); } else if(options.get_bool_option("three-way-merge")) @@ -107,7 +107,7 @@ std::unique_ptr build_analyzer( // Only works with VSD if(options.get_bool_option("vsd")) { - return util_make_unique( + return std::make_unique( std::move(hf), std::move(df), std::move(st), mh); } } @@ -118,33 +118,33 @@ std::unique_ptr build_analyzer( if(options.get_bool_option("constants")) { // constant_propagator_ait derives from ait - return util_make_unique( + return std::make_unique( goto_model.goto_functions); } else if(options.get_bool_option("dependence-graph")) { - return util_make_unique(ns); + return std::make_unique(ns); } else if(options.get_bool_option("dependence-graph-vs")) { - return util_make_unique( + return std::make_unique( goto_model.goto_functions, ns, vs_object_factory, vsd_config, mh); } else if(options.get_bool_option("vsd")) { - auto df = util_make_unique( + auto df = std::make_unique( vs_object_factory, vsd_config); - return util_make_unique>(std::move(df)); + return std::make_unique>(std::move(df)); } else if(options.get_bool_option("intervals")) { - return util_make_unique>(); + return std::make_unique>(); } #if 0 // Not actually implemented, despite the option... else if(options.get_bool_option("non-null")) { - return util_make_unique >(); + return std::make_unique >(); } #endif } @@ -156,7 +156,7 @@ std::unique_ptr build_analyzer( // 'non-revertable' and it has merge shared if(options.get_bool_option("dependence-graph")) { - return util_make_unique(ns); + return std::make_unique(ns); } #endif } diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index c99a6cfb423..b434a4d3a38 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -27,7 +27,6 @@ Author: Daniel Kroening, Peter Schrammel #include #include -#include #include #include "goto_symex_property_decider.h" @@ -165,11 +164,11 @@ get_memory_model(const optionst &options, const namespacet &ns) const std::string mm = options.get_option("mm"); if(mm.empty() || mm == "sc") - return util_make_unique(ns); + return std::make_unique(ns); else if(mm == "tso") - return util_make_unique(ns); + return std::make_unique(ns); else if(mm == "pso") - return util_make_unique(ns); + return std::make_unique(ns); else { throw "invalid memory model '" + mm + "': use one of sc, tso, pso"; diff --git a/src/goto-checker/single_path_symex_checker.cpp b/src/goto-checker/single_path_symex_checker.cpp index 13f4ce14acd..7b6e0b2078e 100644 --- a/src/goto-checker/single_path_symex_checker.cpp +++ b/src/goto-checker/single_path_symex_checker.cpp @@ -62,7 +62,7 @@ operator()(propertiest &properties) { update_properties(properties, result.updated_properties, path.equation); - property_decider = util_make_unique( + property_decider = std::make_unique( options, ui_message_handler, path.equation, ns); const auto solver_runtime = diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index 0dc0dffa550..c44842474a8 100644 --- a/src/goto-checker/solver_factory.cpp +++ b/src/goto-checker/solver_factory.cpp @@ -14,7 +14,6 @@ Author: Daniel Kroening, Peter Schrammel #include #include #include -#include #include #include #include @@ -192,14 +191,14 @@ template static std::unique_ptr make_satcheck_prop(message_handlert &message_handler, const optionst &options) { - auto satcheck = util_make_unique(message_handler); + auto satcheck = std::make_unique(message_handler); if(options.is_set("write-solver-stats-to")) { if( auto hardness_collector = dynamic_cast(&*satcheck)) { std::unique_ptr solver_hardness = - util_make_unique(); + std::make_unique(); solver_hardness->set_outfile(options.get_option("write-solver-stats-to")); hardness_collector->solver_hardness = std::move(solver_hardness); } @@ -345,7 +344,7 @@ std::unique_ptr solver_factoryt::get_default() bool get_array_constraints = options.get_bool_option("show-array-constraints"); - auto bv_pointers = util_make_unique( + auto bv_pointers = std::make_unique( ns, *sat_solver, message_handler, get_array_constraints); if(options.get_option("arrays-uf") == "never") @@ -355,7 +354,7 @@ std::unique_ptr solver_factoryt::get_default() set_decision_procedure_time_limit(*bv_pointers); - return util_make_unique( + return std::make_unique( std::move(bv_pointers), std::move(sat_solver)); } @@ -364,14 +363,14 @@ std::unique_ptr solver_factoryt::get_dimacs() no_beautification(); no_incremental_check(); - auto prop = util_make_unique(message_handler); + auto prop = std::make_unique(message_handler); std::string filename = options.get_option("outfile"); auto bv_dimacs = - util_make_unique(ns, *prop, message_handler, filename); + std::make_unique(ns, *prop, message_handler, filename); - return util_make_unique(std::move(bv_dimacs), std::move(prop)); + return std::make_unique(std::move(bv_dimacs), std::move(prop)); } std::unique_ptr solver_factoryt::get_external_sat() @@ -381,11 +380,11 @@ std::unique_ptr solver_factoryt::get_external_sat() std::string external_sat_solver = options.get_option("external-sat-solver"); auto prop = - util_make_unique(message_handler, external_sat_solver); + std::make_unique(message_handler, external_sat_solver); - auto bv_pointers = util_make_unique(ns, *prop, message_handler); + auto bv_pointers = std::make_unique(ns, *prop, message_handler); - return util_make_unique(std::move(bv_pointers), std::move(prop)); + return std::make_unique(std::move(bv_pointers), std::move(prop)); } std::unique_ptr solver_factoryt::get_bv_refinement() @@ -406,9 +405,9 @@ std::unique_ptr solver_factoryt::get_bv_refinement() info.refine_arithmetic = options.get_bool_option("refine-arithmetic"); info.message_handler = &message_handler; - auto decision_procedure = util_make_unique(info); + auto decision_procedure = std::make_unique(info); set_decision_procedure_time_limit(*decision_procedure); - return util_make_unique( + return std::make_unique( std::move(decision_procedure), std::move(prop)); } @@ -431,9 +430,9 @@ solver_factoryt::get_string_refinement() info.refine_arithmetic = options.get_bool_option("refine-arithmetic"); info.message_handler = &message_handler; - auto decision_procedure = util_make_unique(info); + auto decision_procedure = std::make_unique(info); set_decision_procedure_time_limit(*decision_procedure); - return util_make_unique( + return std::make_unique( std::move(decision_procedure), std::move(prop)); } @@ -445,7 +444,7 @@ std::unique_ptr open_outfile_and_check( if(filename.empty()) return nullptr; - auto out = util_make_unique(widen_if_needed(filename)); + auto out = std::make_unique(widen_if_needed(filename)); if(!*out) { @@ -483,7 +482,7 @@ solver_factoryt::get_incremental_smt2(std::string solver_command) on_std_out ? nullptr : open_outfile_and_check(outfile_arg, message_handler, "--outfile"); - solver_process = util_make_unique( + solver_process = std::make_unique( message_handler, on_std_out ? std::cout : *outfile, std::move(outfile)); } else @@ -492,15 +491,15 @@ solver_factoryt::get_incremental_smt2(std::string solver_command) // If no out_filename is provided `open_outfile_and_check` will return // `nullptr`, and the solver will work normally without any logging. - solver_process = util_make_unique( + solver_process = std::make_unique( std::move(solver_command), message_handler, open_outfile_and_check( out_filename, message_handler, "--dump-smt-formula")); } - return util_make_unique( - util_make_unique( + return std::make_unique( + std::make_unique( ns, std::move(solver_process), message_handler)); } @@ -521,7 +520,7 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver) "provide a filename with --outfile"); } - auto smt2_dec = util_make_unique( + auto smt2_dec = std::make_unique( ns, "cbmc", std::string("Generated by CBMC ") + CBMC_VERSION, @@ -533,11 +532,11 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver) smt2_dec->use_FPA_theory = true; set_decision_procedure_time_limit(*smt2_dec); - return util_make_unique(std::move(smt2_dec)); + return std::make_unique(std::move(smt2_dec)); } else if(filename == "-") { - auto smt2_conv = util_make_unique( + auto smt2_conv = std::make_unique( ns, "cbmc", std::string("Generated by CBMC ") + CBMC_VERSION, @@ -549,13 +548,13 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver) smt2_conv->use_FPA_theory = true; set_decision_procedure_time_limit(*smt2_conv); - return util_make_unique(std::move(smt2_conv)); + return std::make_unique(std::move(smt2_conv)); } else { auto out = open_outfile_and_check(filename, message_handler, "--outfile"); - auto smt2_conv = util_make_unique( + auto smt2_conv = std::make_unique( ns, "cbmc", std::string("Generated by CBMC ") + CBMC_VERSION, @@ -567,7 +566,7 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver) smt2_conv->use_FPA_theory = true; set_decision_procedure_time_limit(*smt2_conv); - return util_make_unique(std::move(smt2_conv), std::move(out)); + return std::make_unique(std::move(smt2_conv), std::move(out)); } } diff --git a/src/goto-harness/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp index f4100354a3a..d32e51bf6d5 100644 --- a/src/goto-harness/function_call_harness_generator.cpp +++ b/src/goto-harness/function_call_harness_generator.cpp @@ -11,7 +11,6 @@ Author: Diffblue Ltd. #include #include #include -#include #include #include #include @@ -95,7 +94,7 @@ struct function_call_harness_generatort::implt function_call_harness_generatort::function_call_harness_generatort( ui_message_handlert &message_handler) - : goto_harness_generatort{}, p_impl(util_make_unique()) + : goto_harness_generatort{}, p_impl(std::make_unique()) { p_impl->message_handler = &message_handler; } @@ -254,7 +253,7 @@ void function_call_harness_generatort::implt::generate( map_function_parameters_to_function_argument_names(); recursive_initialization_config.pointers_to_treat_as_cstrings = function_arguments_to_treat_as_cstrings; - recursive_initialization = util_make_unique( + recursive_initialization = std::make_unique( recursive_initialization_config, goto_model); generate_nondet_globals(function_body); diff --git a/src/goto-harness/goto_harness_parse_options.cpp b/src/goto-harness/goto_harness_parse_options.cpp index 56741e3e1d6..117e5661064 100644 --- a/src/goto-harness/goto_harness_parse_options.cpp +++ b/src/goto-harness/goto_harness_parse_options.cpp @@ -13,7 +13,6 @@ Author: Diffblue Ltd. #include #include #include -#include #include #include @@ -258,12 +257,12 @@ goto_harness_generator_factoryt goto_harness_parse_optionst::make_factory() { auto factory = goto_harness_generator_factoryt{}; factory.register_generator("call-function", [this]() { - return util_make_unique( + return std::make_unique( ui_message_handler); }); factory.register_generator("initialize-with-memory-snapshot", [this]() { - return util_make_unique( + return std::make_unique( ui_message_handler); }); diff --git a/src/goto-instrument/accelerate/enumerating_loop_acceleration.h b/src/goto-instrument/accelerate/enumerating_loop_acceleration.h index 83a4963746e..cea48a83d76 100644 --- a/src/goto-instrument/accelerate/enumerating_loop_acceleration.h +++ b/src/goto-instrument/accelerate/enumerating_loop_acceleration.h @@ -14,8 +14,6 @@ Author: Matt Lewis #include -#include - #include #include @@ -49,7 +47,7 @@ class enumerating_loop_accelerationt goto_functions, guard_manager), path_limit(_path_limit), - path_enumerator(util_make_unique( + path_enumerator(std::make_unique( message_handler, symbol_table, goto_functions, diff --git a/src/goto-instrument/accelerate/scratch_program.h b/src/goto-instrument/accelerate/scratch_program.h index cdc37eca0ef..36c44ad6a97 100644 --- a/src/goto-instrument/accelerate/scratch_program.h +++ b/src/goto-instrument/accelerate/scratch_program.h @@ -14,7 +14,6 @@ Author: Matt Lewis #include -#include #include #include @@ -73,7 +72,7 @@ class scratch_programt:public goto_programt path_storage(), options(get_default_options()), symex(mh, symbol_table, equation, options, path_storage, guard_manager), - satcheck(util_make_unique(mh)), + satcheck(std::make_unique(mh)), satchecker(ns, *satcheck, mh), z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3, mh), checker(&z3) // checker(&satchecker) diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index 1447191158c..96fb6020e22 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -14,7 +14,6 @@ Date: May 2016 #include "cover.h" #include -#include #include #include @@ -65,44 +64,40 @@ void cover_instrumenterst::add_from_criterion( switch(criterion) { case coverage_criteriont::LOCATION: - instrumenters.push_back( - util_make_unique( - symbol_table, goal_filters)); + instrumenters.push_back(std::make_unique( + symbol_table, goal_filters)); break; case coverage_criteriont::BRANCH: instrumenters.push_back( - util_make_unique(symbol_table, goal_filters)); + std::make_unique(symbol_table, goal_filters)); break; case coverage_criteriont::DECISION: - instrumenters.push_back( - util_make_unique( - symbol_table, goal_filters)); + instrumenters.push_back(std::make_unique( + symbol_table, goal_filters)); break; case coverage_criteriont::CONDITION: - instrumenters.push_back( - util_make_unique( - symbol_table, goal_filters)); + instrumenters.push_back(std::make_unique( + symbol_table, goal_filters)); break; case coverage_criteriont::PATH: instrumenters.push_back( - util_make_unique(symbol_table, goal_filters)); + std::make_unique(symbol_table, goal_filters)); break; case coverage_criteriont::MCDC: instrumenters.push_back( - util_make_unique(symbol_table, goal_filters)); + std::make_unique(symbol_table, goal_filters)); break; case coverage_criteriont::ASSERTION: - instrumenters.push_back( - util_make_unique( - symbol_table, goal_filters)); + instrumenters.push_back(std::make_unique( + symbol_table, goal_filters)); break; case coverage_criteriont::COVER: instrumenters.push_back( - util_make_unique(symbol_table, goal_filters)); + std::make_unique(symbol_table, goal_filters)); break; case coverage_criteriont::ASSUME: instrumenters.push_back( - util_make_unique(symbol_table, goal_filters)); + std::make_unique(symbol_table, goal_filters)); } } @@ -194,9 +189,9 @@ cover_configt get_cover_config( std::unique_ptr &goal_filters = cover_config.goal_filters; cover_instrumenterst &instrumenters = cover_config.cover_instrumenters; - function_filters.add(util_make_unique()); + function_filters.add(std::make_unique()); - goal_filters->add(util_make_unique()); + goal_filters->add(std::make_unique()); optionst::value_listt criteria_strings = options.get_list_option("cover"); @@ -227,11 +222,11 @@ cover_configt get_cover_config( if(!cover_include_pattern.empty()) { function_filters.add( - util_make_unique(cover_include_pattern)); + std::make_unique(cover_include_pattern)); } if(options.get_bool_option("no-trivial-tests")) - function_filters.add(util_make_unique()); + function_filters.add(std::make_unique()); cover_config.traces_must_terminate = options.get_bool_option("cover-traces-must-terminate"); @@ -265,13 +260,13 @@ cover_configt get_cover_config( { const symbolt &main_symbol = symbol_table.lookup_ref(main_function_id); cover_config.function_filters.add( - util_make_unique(main_symbol.name)); + std::make_unique(main_symbol.name)); } else if(cover_only == "file") { const symbolt &main_symbol = symbol_table.lookup_ref(main_function_id); cover_config.function_filters.add( - util_make_unique(main_symbol.location.get_file())); + std::make_unique(main_symbol.location.get_file())); } else if(!cover_only.empty()) { diff --git a/src/goto-instrument/cover.h b/src/goto-instrument/cover.h index 4d5026d3a9a..8cd756bc25d 100644 --- a/src/goto-instrument/cover.h +++ b/src/goto-instrument/cover.h @@ -16,7 +16,6 @@ Date: May 2016 #include "cover_filter.h" #include "cover_instrument.h" -#include "util/make_unique.h" class cmdlinet; class goto_modelt; @@ -64,7 +63,7 @@ struct cover_configt function_filterst function_filters; // cover instruments point to goal_filters, so they must be stored on the heap std::unique_ptr goal_filters = - util_make_unique(); + std::make_unique(); cover_instrumenterst cover_instrumenters; cover_instrumenter_baset::assertion_factoryt make_assertion = goto_programt::make_assertion; diff --git a/src/goto-instrument/generate_function_bodies.cpp b/src/goto-instrument/generate_function_bodies.cpp index 5098922a65a..3687fb65187 100644 --- a/src/goto-instrument/generate_function_bodies.cpp +++ b/src/goto-instrument/generate_function_bodies.cpp @@ -16,7 +16,6 @@ Author: Diffblue Ltd. #include #include -#include #include #include #include @@ -381,7 +380,7 @@ std::unique_ptr generate_function_bodies_factory( { if(options.empty() || options == "nondet-return") { - return util_make_unique( + return std::make_unique( std::vector{}, std::regex{}, object_factory_parameters, @@ -390,17 +389,17 @@ std::unique_ptr generate_function_bodies_factory( if(options == "assume-false") { - return util_make_unique(); + return std::make_unique(); } if(options == "assert-false") { - return util_make_unique(); + return std::make_unique(); } if(options == "assert-false-assume-false") { - return util_make_unique< + return std::make_unique< assert_false_then_assume_false_generate_function_bodiest>(); } @@ -477,13 +476,13 @@ std::unique_ptr generate_function_bodies_factory( } } if(param_numbers.empty()) - return util_make_unique( + return std::make_unique( std::move(globals_to_havoc), std::move(params_regex), object_factory_parameters, message_handler); else - return util_make_unique( + return std::make_unique( std::move(globals_to_havoc), std::move(param_numbers), object_factory_parameters, diff --git a/src/goto-symex/path_storage.cpp b/src/goto-symex/path_storage.cpp index 39134334753..3197de7b4cb 100644 --- a/src/goto-symex/path_storage.cpp +++ b/src/goto-symex/path_storage.cpp @@ -12,7 +12,6 @@ Author: Kareem Khazem #include #include -#include nondet_symbol_exprt symex_nondet_generatort:: operator()(typet type, source_locationt location) @@ -97,7 +96,7 @@ static const std::map< " last-in, first-out order. Explores\n" " the program tree depth-first.\n", []() { // NOLINT(whitespace/braces) - return util_make_unique(); + return std::make_unique(); }}}, {"fifo", {" fifo next instruction is pushed before\n" @@ -105,7 +104,7 @@ static const std::map< " first-in, first-out order. Explores\n" " the program tree breadth-first.\n", []() { // NOLINT(whitespace/braces) - return util_make_unique(); + return std::make_unique(); }}}}); std::string show_path_strategies() diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index a9c11fb982f..bc1d420f71b 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -21,7 +21,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -417,7 +416,7 @@ std::unique_ptr goto_symext::initialize_entry_point_state( auto *storage = &path_storage; // create and prepare the state - auto state = util_make_unique( + auto state = std::make_unique( symex_targett::sourcet(entry_point_id, start_function->body), symex_config.max_field_sensitivity_array_size, symex_config.simplify_opt, diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp index 97a0058ea9a..4b1090f07db 100644 --- a/src/goto-synthesizer/cegis_verifier.cpp +++ b/src/goto-synthesizer/cegis_verifier.cpp @@ -591,7 +591,7 @@ optionalt cegis_verifiert::verify() preprocess_goto_model(); std::unique_ptr< all_properties_verifier_with_trace_storaget> - checker = util_make_unique< + checker = std::make_unique< all_properties_verifier_with_trace_storaget>( options, ui_message_handler, goto_model); diff --git a/src/jsil/jsil_language.cpp b/src/jsil/jsil_language.cpp index 58caa64c018..1ad144c3ce1 100644 --- a/src/jsil/jsil_language.cpp +++ b/src/jsil/jsil_language.cpp @@ -101,7 +101,7 @@ void jsil_languaget::show_parse(std::ostream &out) std::unique_ptr new_jsil_language() { - return util_make_unique(); + return std::make_unique(); } bool jsil_languaget::from_expr( diff --git a/src/jsil/jsil_language.h b/src/jsil/jsil_language.h index 7138620118b..4d99beff857 100644 --- a/src/jsil/jsil_language.h +++ b/src/jsil/jsil_language.h @@ -14,8 +14,6 @@ Author: Michael Tautschnig, tautschn@amazon.com #include -#include - #include #include "jsil_parse_tree.h" @@ -53,7 +51,9 @@ class jsil_languaget:public languaget const namespacet &ns) override; std::unique_ptr new_language() override - { return util_make_unique(); } + { + return std::make_unique(); + } std::string id() const override { diff --git a/src/json-symtab-language/json_symtab_language.h b/src/json-symtab-language/json_symtab_language.h index cea1ceefb89..097daecfcab 100644 --- a/src/json-symtab-language/json_symtab_language.h +++ b/src/json-symtab-language/json_symtab_language.h @@ -12,7 +12,6 @@ Author: Chris Smowton, chris.smowton@diffblue.com #define CPROVER_JSON_SYMTAB_LANGUAGE_JSON_SYMTAB_LANGUAGE_H #include -#include #include #include @@ -55,7 +54,7 @@ class json_symtab_languaget : public languaget std::unique_ptr new_language() override { - return util_make_unique(); + return std::make_unique(); } bool generate_support_functions(symbol_table_baset &symbol_table) override @@ -75,7 +74,7 @@ class json_symtab_languaget : public languaget inline std::unique_ptr new_json_symtab_language() { - return util_make_unique(); + return std::make_unique(); } #endif diff --git a/src/libcprover-cpp/api.cpp b/src/libcprover-cpp/api.cpp index aeb3fd2d842..652478d57f9 100644 --- a/src/libcprover-cpp/api.cpp +++ b/src/libcprover-cpp/api.cpp @@ -36,7 +36,7 @@ extern configt config; std::unique_ptr api_sessiont::get_api_version() const { - return util_make_unique(std::string{CBMC_VERSION}); + return std::make_unique(std::string{CBMC_VERSION}); } struct api_session_implementationt @@ -51,10 +51,10 @@ api_sessiont::api_sessiont() : api_sessiont{api_optionst::create()} } api_sessiont::api_sessiont(const api_optionst &options) - : implementation{util_make_unique()} + : implementation{std::make_unique()} { implementation->message_handler = - util_make_unique(null_message_handlert{}); + std::make_unique(null_message_handlert{}); implementation->options = options.to_engine_options(); // Needed to initialise the language options correctly cmdlinet cmdline; @@ -130,13 +130,13 @@ void api_sessiont::set_message_callback( api_call_back_contextt context) { implementation->message_handler = - util_make_unique(callback, context); + std::make_unique(callback, context); } void api_sessiont::load_model_from_files( const std::vector &files) const { - implementation->model = util_make_unique(initialize_goto_model( + implementation->model = std::make_unique(initialize_goto_model( files, *implementation->message_handler, *implementation->options)); } @@ -161,7 +161,7 @@ void api_sessiont::read_goto_binary(std::string &file) const if(read_opt_val.has_value()) { implementation->model = - util_make_unique(std::move(read_opt_val.value())); + std::make_unique(std::move(read_opt_val.value())); } else { @@ -228,7 +228,7 @@ std::unique_ptr api_sessiont::run_verifier() const auto properties = verifier.get_properties(); result.set_properties(properties); - return util_make_unique(result); + return std::make_unique(result); } void api_sessiont::drop_unused_functions() const diff --git a/src/libcprover-cpp/api_options.cpp b/src/libcprover-cpp/api_options.cpp index d11e01785ac..c4d1839ddec 100644 --- a/src/libcprover-cpp/api_options.cpp +++ b/src/libcprover-cpp/api_options.cpp @@ -3,7 +3,6 @@ #include "api_options.h" #include -#include #include #include @@ -16,7 +15,7 @@ api_optionst api_optionst::create() static std::unique_ptr make_internal_default_options() { - std::unique_ptr options = util_make_unique(); + std::unique_ptr options = std::make_unique(); cmdlinet command_line; PARSE_OPTIONS_GOTO_CHECK(command_line, (*options)); parse_solver_options(command_line, *options); diff --git a/src/libcprover-cpp/verification_result.cpp b/src/libcprover-cpp/verification_result.cpp index f7d801f733a..fd18f7ef4a2 100644 --- a/src/libcprover-cpp/verification_result.cpp +++ b/src/libcprover-cpp/verification_result.cpp @@ -8,7 +8,6 @@ #include #include -#include #include @@ -61,7 +60,7 @@ verification_resultt::verification_result_implt::get_properties() // Verification_result verification_resultt::verification_resultt() - : _impl(util_make_unique()) + : _impl(std::make_unique()) { } @@ -70,7 +69,7 @@ verification_resultt::~verification_resultt() } verification_resultt::verification_resultt(const verification_resultt &other) - : _impl(util_make_unique(*other._impl)) + : _impl(std::make_unique(*other._impl)) { } diff --git a/src/pointer-analysis/value_set_analysis.h b/src/pointer-analysis/value_set_analysis.h index d917471be3d..4003ff47f05 100644 --- a/src/pointer-analysis/value_set_analysis.h +++ b/src/pointer-analysis/value_set_analysis.h @@ -33,7 +33,7 @@ class value_set_analysis_templatet : public value_setst, public ait typedef typename baset::locationt locationt; explicit value_set_analysis_templatet(const namespacet &_ns) - : baset(util_make_unique>()), + : baset(std::make_unique>()), ns(_ns) { } diff --git a/src/solvers/sat/satcheck_glucose.cpp b/src/solvers/sat/satcheck_glucose.cpp index 14bda00a080..d49b1a4d424 100644 --- a/src/solvers/sat/satcheck_glucose.cpp +++ b/src/solvers/sat/satcheck_glucose.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -254,7 +253,7 @@ void satcheck_glucose_baset::set_assignment(literalt a, bool value) template satcheck_glucose_baset::satcheck_glucose_baset( message_handlert &message_handler) - : cnf_solvert(message_handler), solver(util_make_unique()) + : cnf_solvert(message_handler), solver(std::make_unique()) { } diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp index 2c9799cc700..dc26882ad4b 100644 --- a/src/solvers/sat/satcheck_minisat2.cpp +++ b/src/solvers/sat/satcheck_minisat2.cpp @@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -325,7 +324,7 @@ template satcheck_minisat2_baset::satcheck_minisat2_baset( message_handlert &message_handler) : cnf_solvert(message_handler), - solver(util_make_unique()), + solver(std::make_unique()), time_limit_seconds(0) { } diff --git a/src/solvers/smt2_incremental/encoding/struct_encoding.cpp b/src/solvers/smt2_incremental/encoding/struct_encoding.cpp index 48ebcfa1a60..3a77517173c 100644 --- a/src/solvers/smt2_incremental/encoding/struct_encoding.cpp +++ b/src/solvers/smt2_incremental/encoding/struct_encoding.cpp @@ -6,7 +6,6 @@ #include #include #include -#include #include #include #include @@ -19,12 +18,12 @@ #include struct_encodingt::struct_encodingt(const namespacet &ns) - : boolbv_width{util_make_unique(ns)}, ns{ns} + : boolbv_width{std::make_unique(ns)}, ns{ns} { } struct_encodingt::struct_encodingt(const struct_encodingt &other) - : boolbv_width{util_make_unique(*other.boolbv_width)}, + : boolbv_width{std::make_unique(*other.boolbv_width)}, ns{other.ns} { } diff --git a/src/solvers/strings/string_dependencies.cpp b/src/solvers/strings/string_dependencies.cpp index bb7aeab4d9a..2a0ab220886 100644 --- a/src/solvers/strings/string_dependencies.cpp +++ b/src/solvers/strings/string_dependencies.cpp @@ -12,7 +12,6 @@ Author: Diffblue Ltd. #include #include #include -#include #include /// Applies `f` on all strings contained in `e` that are not if-expressions. @@ -34,38 +33,38 @@ static std::unique_ptr to_string_builtin_function( const irep_idt &id = name.get_identifier(); if(id == ID_cprover_string_insert_func) - return util_make_unique( + return std::make_unique( return_code, fun_app.arguments(), array_pool); if(id == ID_cprover_string_concat_func) - return util_make_unique( + return std::make_unique( return_code, fun_app.arguments(), array_pool); if(id == ID_cprover_string_concat_char_func) - return util_make_unique( + return std::make_unique( return_code, fun_app.arguments(), array_pool); if(id == ID_cprover_string_format_func) - return util_make_unique( + return std::make_unique( return_code, fun_app.arguments(), array_pool); if(id == ID_cprover_string_of_int_func) - return util_make_unique( + return std::make_unique( return_code, fun_app.arguments(), array_pool); if(id == ID_cprover_string_char_set_func) - return util_make_unique( + return std::make_unique( return_code, fun_app.arguments(), array_pool); if(id == ID_cprover_string_to_lower_case_func) - return util_make_unique( + return std::make_unique( return_code, fun_app.arguments(), array_pool); if(id == ID_cprover_string_to_upper_case_func) - return util_make_unique( + return std::make_unique( return_code, fun_app.arguments(), array_pool); - return util_make_unique( + return std::make_unique( return_code, fun_app, array_pool); } @@ -85,7 +84,7 @@ string_dependenciest::node_at(const array_string_exprt &e) const { const auto &it = node_index_pool.find(e); if(it != node_index_pool.end()) - return util_make_unique(string_nodes.at(it->second)); + return std::make_unique(string_nodes.at(it->second)); return {}; } diff --git a/src/statement-list/statement_list_language.cpp b/src/statement-list/statement_list_language.cpp index f9d7fe9be6b..28087cdb0b8 100644 --- a/src/statement-list/statement_list_language.cpp +++ b/src/statement-list/statement_list_language.cpp @@ -19,7 +19,6 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com #include #include #include -#include #include void statement_list_languaget::set_language_options(const optionst &options) @@ -144,12 +143,12 @@ std::set statement_list_languaget::extensions() const std::unique_ptr new_statement_list_language() { - return util_make_unique(); + return std::make_unique(); } std::unique_ptr statement_list_languaget::new_language() { - return util_make_unique(); + return std::make_unique(); } std::string statement_list_languaget::id() const diff --git a/src/util/make_unique.h b/src/util/make_unique.h deleted file mode 100644 index 0f4ba41ac3e..00000000000 --- a/src/util/make_unique.h +++ /dev/null @@ -1,24 +0,0 @@ -/*******************************************************************\ - -Module: Really simple unique_ptr utilities - -Author: Reuben Thomas, reuben.thomas@diffblue.com - -\*******************************************************************/ - -#ifndef CPROVER_UTIL_MAKE_UNIQUE_H -#define CPROVER_UTIL_MAKE_UNIQUE_H - -#include // unique_ptr - -// This is a stand-in for std::make_unique, which isn't part of the standard -// library until C++14. When we move to C++14, we should do a find-and-replace -// on this to use std::make_unique instead. - -template -std::unique_ptr util_make_unique(Ts &&... ts) -{ - return std::unique_ptr(new T(std::forward(ts)...)); -} - -#endif diff --git a/src/util/piped_process.cpp b/src/util/piped_process.cpp index f5b028ae2f6..a9427d7671e 100644 --- a/src/util/piped_process.cpp +++ b/src/util/piped_process.cpp @@ -79,7 +79,6 @@ # include "run.h" // for Windows arg quoting # include "unicode.h" // for widen function # include // library for _tcscpy function -# include # include #else # include // library for fcntl function @@ -213,7 +212,7 @@ piped_processt::piped_processt( } // Create the child process STARTUPINFOW start_info; - proc_info = util_make_unique(); + proc_info = std::make_unique(); ZeroMemory(proc_info.get(), sizeof(PROCESS_INFORMATION)); ZeroMemory(&start_info, sizeof(STARTUPINFOW)); start_info.cb = sizeof(STARTUPINFOW); diff --git a/src/util/range.h b/src/util/range.h index c714cdb0464..0e7242954ce 100644 --- a/src/util/range.h +++ b/src/util/range.h @@ -14,12 +14,12 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #ifndef CPROVER_UTIL_RANGE_H #define CPROVER_UTIL_RANGE_H +#include + #include +#include #include -#include -#include - /// Iterator which applies some given function \c f after each increment and /// returns its result on dereference. template @@ -349,7 +349,7 @@ struct zip_iteratort !same_size || ((first_begin == first_end) == (second_begin == second_end))); if(first_begin != first_end) - current = util_make_unique(*first_begin, *second_begin); + current = std::make_unique(*first_begin, *second_begin); } private: diff --git a/src/util/sharing_node.h b/src/util/sharing_node.h index fe7eb5f26fd..4caf809bb55 100644 --- a/src/util/sharing_node.h +++ b/src/util/sharing_node.h @@ -35,7 +35,6 @@ Author: Daniel Poetzl #include "as_const.h" #include "invariant.h" -#include "make_unique.h" #include "small_shared_n_way_ptr.h" #include "small_shared_ptr.h" diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp index 13204451ead..69302626dc7 100644 --- a/src/util/ui_message.cpp +++ b/src/util/ui_message.cpp @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "json.h" #include "json_irep.h" #include "json_stream.h" -#include "make_unique.h" #include "structured_data.h" #include "xml.h" #include "xml_irep.h" @@ -86,7 +85,7 @@ ui_message_handlert::ui_message_handlert( if(get_ui() == uit::PLAIN) { console_message_handler = - util_make_unique(always_flush); + std::make_unique(always_flush); message_handler = &*console_message_handler; } } diff --git a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index 05f9694b07b..57ffbc1fe8b 100644 --- a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -5,7 +5,6 @@ #include #include #include -#include #include #include #include @@ -120,7 +119,7 @@ struct decision_procedure_test_environmentt final smt_is_dynamic_objectt is_dynamic_object_function; smt2_incremental_decision_proceduret procedure{ ns, - util_make_unique( + std::make_unique( [&](const smt_commandt &smt_command) { this->send(smt_command); }, [&]() { return this->receive_response(); }), message_handler}; From 2d628714bc9a0e955f5db4188e6e1b174ce3a95b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 23 Mar 2022 23:51:25 +0000 Subject: [PATCH 3/7] Remove local declaration of void_t With the move to C++ 17 we can use std::void_t instead. --- src/solvers/smt2_incremental/ast/smt_terms.h | 3 +- src/solvers/smt2_incremental/type_traits.h | 37 -------------------- 2 files changed, 1 insertion(+), 39 deletions(-) delete mode 100644 src/solvers/smt2_incremental/type_traits.h diff --git a/src/solvers/smt2_incremental/ast/smt_terms.h b/src/solvers/smt2_incremental/ast/smt_terms.h index f69aadeffd6..c8b2d375a37 100644 --- a/src/solvers/smt2_incremental/ast/smt_terms.h +++ b/src/solvers/smt2_incremental/ast/smt_terms.h @@ -6,7 +6,6 @@ #include #include -#include #include "smt_index.h" #include "smt_sorts.h" @@ -150,7 +149,7 @@ class smt_function_application_termt : public smt_termt template struct has_indicest< functiont, - void_t().indices())>> : std::true_type + std::void_t().indices())>> : std::true_type { }; diff --git a/src/solvers/smt2_incremental/type_traits.h b/src/solvers/smt2_incremental/type_traits.h deleted file mode 100644 index ea928e1ddb7..00000000000 --- a/src/solvers/smt2_incremental/type_traits.h +++ /dev/null @@ -1,37 +0,0 @@ -// Author: Diffblue Ltd. - -/// \file -/// Back ports of utilities available in the `` library for C++14 -/// or C++17 to C++11. These can be replaced with the standard library versions -/// as and when we upgrade the version CBMC is compiled with. - -#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_TYPE_TRAITS_H -#define CPROVER_SOLVERS_SMT2_INCREMENTAL_TYPE_TRAITS_H - -#include - -namespace detail // NOLINT -{ -// Implementation detail of `void_t`. -template -struct make_voidt -{ - using type = void; -}; -} // namespace detail - -// The below definition is of a back-ported version of the C++17 STL -// `std::void_t` template. This makes this particular template available when -// compiling for the C++11 or C++14 standard versions. It will also compile -// as-is when targeting the C++17 standard. The back-ported version is not added -// to the `std` namespace as this would be undefined behaviour. However once we -// permanently move to the new standard the below code should be removed -// and `std::void_t` should be used directly, to avoid polluting the global -// namespace. For example - -// `void_t` -// should be updated to - -// `std::void_t` -template -using void_t = typename detail::make_voidt::type; - -#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_TYPE_TRAITS_H From 0c33e4142869b2d9ddb7595ee836d56677e7c861 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 24 Mar 2022 00:33:14 +0000 Subject: [PATCH 4/7] Replace file_util.{h,cpp} by std::filesystem With C++ 17 we can use the STL-provided implementation instead of rolling our own (platform-dependent) code. --- .../java_bytecode/java_class_loader_base.cpp | 15 +- .../java-testing-utils/load_java_class.cpp | 15 +- .../unreachable_instructions.cpp | 10 +- src/goto-cc/as_mode.cpp | 6 +- src/goto-cc/compile.cpp | 36 ++- src/goto-cc/gcc_mode.cpp | 6 +- src/goto-cc/hybrid_binary.cpp | 6 +- src/goto-cc/ld_mode.cpp | 14 +- src/goto-cc/ms_cl_mode.cpp | 10 +- src/goto-instrument/count_eloc.cpp | 11 +- src/util/Makefile | 1 - src/util/file_util.cpp | 274 ------------------ src/util/file_util.h | 50 ---- src/util/parser.h | 10 +- src/util/source_location.cpp | 17 +- src/util/tempdir.cpp | 59 +--- src/util/tempfile.cpp | 4 +- unit/Makefile | 1 - unit/util/file_util.cpp | 72 ----- 19 files changed, 103 insertions(+), 514 deletions(-) delete mode 100644 src/util/file_util.cpp delete mode 100644 src/util/file_util.h delete mode 100644 unit/util/file_util.cpp diff --git a/jbmc/src/java_bytecode/java_class_loader_base.cpp b/jbmc/src/java_bytecode/java_class_loader_base.cpp index 5a998bc4d63..2c395271910 100644 --- a/jbmc/src/java_bytecode/java_class_loader_base.cpp +++ b/jbmc/src/java_bytecode/java_class_loader_base.cpp @@ -8,15 +8,15 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_class_loader_base.h" -#include "jar_file.h" -#include "java_bytecode_parse_tree.h" -#include "java_bytecode_parser.h" - -#include #include #include #include +#include "jar_file.h" +#include "java_bytecode_parse_tree.h" +#include "java_bytecode_parser.h" + +#include #include 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)) { diff --git a/jbmc/unit/java-testing-utils/load_java_class.cpp b/jbmc/unit/java-testing-utils/load_java_class.cpp index e1f1fcf787b..b8568719dc5 100644 --- a/jbmc/unit/java-testing-utils/load_java_class.cpp +++ b/jbmc/unit/java-testing-utils/load_java_class.cpp @@ -8,19 +8,18 @@ Author: Diffblue Ltd. #include "load_java_class.h" -#include -#include -#include -#include - #include #include #include +#include #include +#include +#include +#include -#include -#include +#include +#include /// 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 diff --git a/src/goto-analyzer/unreachable_instructions.cpp b/src/goto-analyzer/unreachable_instructions.cpp index 6ff7822bed7..5fc03e49f91 100644 --- a/src/goto-analyzer/unreachable_instructions.cpp +++ b/src/goto-analyzer/unreachable_instructions.cpp @@ -13,7 +13,6 @@ Date: April 2016 #include "unreachable_instructions.h" -#include #include #include #include @@ -23,6 +22,8 @@ Date: April 2016 #include #include +#include + typedef std::map dead_mapt; static void unreachable_instructions( @@ -106,9 +107,10 @@ file_name_string_opt(const source_locationt &source_location) if(source_location.get_file().empty()) return {}; - return concat_dir_file( - id2string(source_location.get_working_directory()), - id2string(source_location.get_file())); + return std::filesystem::path( + id2string(source_location.get_working_directory())) + .append(id2string(source_location.get_file())) + .string(); } static void add_to_json( diff --git a/src/goto-cc/as_mode.cpp b/src/goto-cc/as_mode.cpp index d811a757bc2..fee687b2a9e 100644 --- a/src/goto-cc/as_mode.cpp +++ b/src/goto-cc/as_mode.cpp @@ -21,7 +21,6 @@ Author: Michael Tautschnig #include #include -#include #include #include #include @@ -31,6 +30,7 @@ Author: Michael Tautschnig #include "goto_cc_cmdline.h" #include "hybrid_binary.h" +#include #include // IWYU pragma: keep #include @@ -303,9 +303,9 @@ int as_modet::as_hybrid_binary(const compilet &compiler) std::string saved = output_file + ".goto-cc-saved"; try { - file_rename(output_file, saved); + std::filesystem::rename(output_file, saved); } - catch(const cprover_exception_baset &e) + catch(const std::filesystem::filesystem_error &e) { log.error() << "Rename failed: " << e.what() << messaget::eom; return 1; diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 7823142a6b7..54623f73135 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -15,7 +15,6 @@ Date: June 2006 #include #include -#include #include #include #include @@ -39,6 +38,7 @@ Date: June 2006 #include #include +#include #include #include @@ -217,11 +217,14 @@ bool compilet::add_files_from_archive( tstr = get_temporary_directory("goto-cc.XXXXXX"); tmp_dirs.push_back(tstr); - set_current_path(tmp_dirs.back()); + std::filesystem::current_path(tmp_dirs.back()); // unpack now - int ret = - run("ar", {"ar", "x", concat_dir_file(working_directory, file_name)}); + int ret = run( + "ar", + {"ar", + "x", + std::filesystem::path(working_directory).append(file_name).string()}); if(ret != 0) { log.error() << "Failed to extract archive " << file_name << messaget::eom; @@ -233,7 +236,9 @@ bool compilet::add_files_from_archive( temporary_filet tmp_file_out("", ""); int ret = run( "ar", - {"ar", "t", concat_dir_file(working_directory, file_name)}, + {"ar", + "t", + std::filesystem::path(working_directory).append(file_name).string()}, "", tmp_file_out(), ""); @@ -248,7 +253,7 @@ bool compilet::add_files_from_archive( while(!in.fail() && std::getline(in, line)) { - std::string t = concat_dir_file(tstr, line); + std::string t = std::filesystem::path(tstr).append(line).string(); if(is_goto_binary(t, log.get_message_handler())) object_files.push_back(t); @@ -258,7 +263,7 @@ bool compilet::add_files_from_archive( } if(!thin_archive) - set_current_path(working_directory); + std::filesystem::current_path(working_directory); return false; } @@ -272,7 +277,8 @@ bool compilet::find_library(const std::string &name) for(const auto &library_path : library_paths) { - library_file_name = concat_dir_file(library_path, "lib" + name + ".a"); + library_file_name = + std::filesystem::path(library_path).append("lib" + name + ".a").string(); std::ifstream in(library_file_name); @@ -280,7 +286,9 @@ bool compilet::find_library(const std::string &name) return !add_input_file(library_file_name); else { - library_file_name = concat_dir_file(library_path, "lib" + name + ".so"); + library_file_name = std::filesystem::path(library_path) + .append("lib" + name + ".so") + .string(); switch(detect_file_type(library_file_name, log.get_message_handler())) { @@ -409,7 +417,11 @@ optionalt compilet::compile() get_base_name(file_name, true) + "." + object_file_extension; if(!output_directory_object.empty()) - cfn = concat_dir_file(output_directory_object, file_name_with_obj_ext); + { + cfn = std::filesystem::path(output_directory_object) + .append(file_name_with_obj_ext) + .string(); + } else cfn = file_name_with_obj_ext; } @@ -648,7 +660,7 @@ compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror) mode=COMPILE_LINK_EXECUTABLE; echo_file_name=false; wrote_object=false; - working_directory=get_current_working_directory(); + working_directory = std::filesystem::current_path().string(); if(cmdline.isset("export-function-local-symbols")) { @@ -665,7 +677,7 @@ compilet::~compilet() // clean up temp dirs for(const auto &dir : tmp_dirs) - delete_directory(dir); + std::filesystem::remove_all(dir); } std::size_t compilet::function_body_count(const goto_functionst &functions) diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp index 5459ad361c1..0c9d6d50cbf 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/src/goto-cc/gcc_mode.cpp @@ -21,7 +21,6 @@ Author: CM Wintersteiger, 2006 #include #include -#include #include #include #include @@ -35,6 +34,7 @@ Author: CM Wintersteiger, 2006 #include "hybrid_binary.h" #include "linker_script_merge.h" +#include #include // IWYU pragma: keep #include #include @@ -1006,9 +1006,9 @@ int gcc_modet::gcc_hybrid_binary(compilet &compiler) try { - file_rename(*it, bin_name); + std::filesystem::rename(*it, bin_name); } - catch(const cprover_exception_baset &e) + catch(const std::filesystem::filesystem_error &e) { log.error() << "Rename failed: " << e.what() << messaget::eom; return 1; diff --git a/src/goto-cc/hybrid_binary.cpp b/src/goto-cc/hybrid_binary.cpp index 745fa3cd478..434c08c34d3 100644 --- a/src/goto-cc/hybrid_binary.cpp +++ b/src/goto-cc/hybrid_binary.cpp @@ -11,12 +11,12 @@ Author: Michael Tautschnig, 2018 #include "hybrid_binary.h" -#include #include #include #include #include +#include #if defined(__APPLE__) # include @@ -80,7 +80,7 @@ int hybrid_binary( } // delete the goto binary - bool remove_result = file_remove(goto_binary_file); + bool remove_result = std::filesystem::remove(goto_binary_file); if(!remove_result) { message.error() << "Remove failed: " << std::strerror(errno) @@ -140,7 +140,7 @@ int hybrid_binary( } // delete the goto binary - bool remove_result = file_remove(goto_binary_file); + bool remove_result = std::filesystem::remove(goto_binary_file); if(!remove_result) { message.error() << "Remove failed: " << std::strerror(errno) diff --git a/src/goto-cc/ld_mode.cpp b/src/goto-cc/ld_mode.cpp index b443a4ef033..bee843fa3fa 100644 --- a/src/goto-cc/ld_mode.cpp +++ b/src/goto-cc/ld_mode.cpp @@ -19,13 +19,8 @@ Author: CM Wintersteiger, 2006 #include #endif -#include -#include -#include - #include #include -#include #include #include @@ -34,6 +29,11 @@ Author: CM Wintersteiger, 2006 #include "hybrid_binary.h" #include "linker_script_merge.h" +#include +#include +#include +#include + static std::string linker_name(const cmdlinet &cmdline, const std::string &base_name) { @@ -183,9 +183,9 @@ int ld_modet::ld_hybrid_binary( try { - file_rename(output_file, goto_binary); + std::filesystem::rename(output_file, goto_binary); } - catch(const cprover_exception_baset &e) + catch(const std::filesystem::filesystem_error &e) { log.error() << "Rename failed: " << e.what() << messaget::eom; return 1; diff --git a/src/goto-cc/ms_cl_mode.cpp b/src/goto-cc/ms_cl_mode.cpp index ea9193a800b..bbc78a165b1 100644 --- a/src/goto-cc/ms_cl_mode.cpp +++ b/src/goto-cc/ms_cl_mode.cpp @@ -19,16 +19,16 @@ Author: CM Wintersteiger, 2006 #include #endif -#include - #include -#include #include #include #include "compile.h" #include "ms_cl_version.h" +#include +#include + static bool has_directory_suffix(const std::string &path) { // MS CL decides whether a parameter is a directory on the @@ -128,7 +128,7 @@ int ms_cl_modet::doit() { compiler.output_directory_object = Fo_value; - if(!is_directory(Fo_value)) + if(!std::filesystem::is_directory(Fo_value)) log.warning() << "not a directory: " << Fo_value << messaget::eom; } else @@ -154,7 +154,7 @@ int ms_cl_modet::doit() has_directory_suffix(compiler.output_file_executable) && cmdline.args.size() >= 1) { - if(!is_directory(compiler.output_file_executable)) + if(!std::filesystem::is_directory(compiler.output_file_executable)) { log.warning() << "not a directory: " << compiler.output_file_executable << messaget::eom; diff --git a/src/goto-instrument/count_eloc.cpp b/src/goto-instrument/count_eloc.cpp index 51bf3e825d4..a2185e2f9ab 100644 --- a/src/goto-instrument/count_eloc.cpp +++ b/src/goto-instrument/count_eloc.cpp @@ -13,10 +13,6 @@ Date: December 2012 #include "count_eloc.h" -#include -#include - -#include #include #include #include @@ -26,6 +22,10 @@ Date: December 2012 #include +#include +#include +#include + typedef std::unordered_set linest; typedef std::unordered_map filest; typedef std::unordered_map working_dirst; @@ -75,7 +75,8 @@ void list_eloc(const goto_modelt &goto_model) { std::string file=id2string(lines.first); if(!files.first.empty()) - file=concat_dir_file(id2string(files.first), file); + file = + std::filesystem::path(id2string(files.first)).append(file).string(); for(const irep_idt &line : lines.second) std::cout << file << ':' << line << '\n'; diff --git a/src/util/Makefile b/src/util/Makefile index 30452e2e302..1e33ebc73db 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -17,7 +17,6 @@ SRC = arith_tools.cpp \ expr_initializer.cpp \ expr_util.cpp \ exception_utils.cpp \ - file_util.cpp \ find_macros.cpp \ find_symbols.cpp \ fixedbv.cpp \ diff --git a/src/util/file_util.cpp b/src/util/file_util.cpp deleted file mode 100644 index d1cd3378a05..00000000000 --- a/src/util/file_util.cpp +++ /dev/null @@ -1,274 +0,0 @@ -/*******************************************************************\ - -Module: File Utilities - -Author: - -Date: January 2012 - -\*******************************************************************/ - -/// \file -/// File Utilities - -#include "file_util.h" - -#include "exception_utils.h" - -#include -#include - -#if defined(__linux__) || \ - defined(__FreeBSD_kernel__) || \ - defined(__GNU__) || \ - defined(__unix__) || \ - defined(__CYGWIN__) || \ - defined(__MACH__) -#include -#include -#include -#include -#include -#endif - -#ifdef _WIN32 -#include -#ifdef _MSC_VER -#pragma warning(disable:4668) - // using #if/#elif on undefined macro -#pragma warning(disable : 5039) -// pointer or reference to potentially throwing function passed to extern C -#endif -#include -#include -#include -#include -#define chdir _chdir -#include -#endif - -/// \return current working directory -std::string get_current_working_directory() -{ -#ifndef _WIN32 - errno=0; - char *wd=realpath(".", nullptr); - - if(wd == nullptr) - throw system_exceptiont( - std::string("realpath failed: ") + std::strerror(errno)); - - std::string working_directory=wd; - free(wd); -#else - TCHAR buffer[4096]; - DWORD retval=GetCurrentDirectory(4096, buffer); - if(retval == 0) - throw system_exceptiont("failed to get current directory of process"); - -# ifdef UNICODE - std::string working_directory(narrow(buffer)); -# else - std::string working_directory(buffer); -# endif - -#endif - - return working_directory; -} - -/// Set working directory. -/// \param path: New working directory to change to -void set_current_path(const std::string &path) -{ - if(chdir(path.c_str()) != 0) - throw system_exceptiont( - std::string("chdir failed: ") + std::strerror(errno)); -} - -/// deletes all files in 'path' and then the directory itself -#ifdef _WIN32 - -void delete_directory_utf16(const std::wstring &path) -{ - std::wstring pattern=path + L"\\*"; - // NOLINTNEXTLINE(readability/identifiers) - struct _wfinddata_t info; - intptr_t hFile=_wfindfirst(pattern.c_str(), &info); - if(hFile!=-1) - { - do - { - if(wcscmp(info.name, L".")==0 || wcscmp(info.name, L"..")==0) - continue; - std::wstring sub_path=path+L"\\"+info.name; - if(info.attrib & _A_SUBDIR) - delete_directory_utf16(sub_path); - else - DeleteFileW(sub_path.c_str()); - } - while(_wfindnext(hFile, &info)==0); - _findclose(hFile); - RemoveDirectoryW(path.c_str()); - } -} - -#endif - -void delete_directory(const std::string &path) -{ -#ifdef _WIN32 - delete_directory_utf16(utf8_to_utf16_native_endian(path)); -#else - DIR *dir=opendir(path.c_str()); - if(dir!=nullptr) - { - struct dirent *ent; - while((ent=readdir(dir))!=nullptr) - { - // Needed for Alpine Linux - if(strcmp(ent->d_name, ".")==0 || strcmp(ent->d_name, "..")==0) - continue; - - std::string sub_path=path+"/"+ent->d_name; - - struct stat stbuf; - int result=stat(sub_path.c_str(), &stbuf); - if(result!=0) - throw system_exceptiont( - std::string("Stat failed: ") + std::strerror(errno)); - - if(S_ISDIR(stbuf.st_mode)) - delete_directory(sub_path); - else - { - result=remove(sub_path.c_str()); - if(result!=0) - throw system_exceptiont( - std::string("Remove failed: ") + std::strerror(errno)); - } - } - closedir(dir); - } - rmdir(path.c_str()); -#endif -} - -/// \par parameters: directory name and file name -/// \return concatenation of directory and file, if the file path is relative -std::string concat_dir_file( - const std::string &directory, - const std::string &file_name) -{ -#ifdef _WIN32 - if( - file_name.size() > 1 && file_name[0] != '/' && file_name[0] != '\\' && - file_name[1] == ':') - { - return file_name; - } - else if( - !directory.empty() && (directory.back() == '/' || directory.back() == '\\')) - { - return directory + file_name; - } - else - return directory + '\\' + file_name; -#else - if(!file_name.empty() && file_name[0] == '/') - return file_name; - else if(!directory.empty() && directory.back() == '/') - return directory + file_name; - else - return directory + '/' + file_name; -#endif -} - -bool is_directory(const std::string &path) -{ - if(path.empty()) - return false; - -#ifdef _WIN32 - - auto attributes = ::GetFileAttributesW(widen(path).c_str()); - if (attributes == INVALID_FILE_ATTRIBUTES) - return false; - else - return (attributes & FILE_ATTRIBUTE_DIRECTORY) != 0; - -#else - - struct stat buf; - - if(stat(path.c_str(), &buf)!=0) - return false; - else - return (buf.st_mode & S_IFDIR) != 0; - -#endif -} - -bool create_directory(const std::string &path) -{ -#ifdef _WIN32 - return _mkdir(path.c_str()) == 0; -#else - // the umask matches what std::filesystem::create_directory does - return mkdir(path.c_str(), 0777) == 0; -#endif -} - -bool file_exists(const std::string &path) -{ -#ifdef _WIN32 - return _waccess(utf8_to_utf16_native_endian(path).c_str(), 0) == 0; -#else - return access(path.c_str(), F_OK) == 0; -#endif -} - -bool file_remove(const std::string &path) -{ -#ifdef _WIN32 - return _wunlink(utf8_to_utf16_native_endian(path).c_str()) == 0; -#else - return unlink(path.c_str()) == 0; -#endif -} - -void file_rename(const std::string &old_path, const std::string &new_path) -{ -#ifdef _WIN32 - if(is_directory(old_path)) - { - // rename() only renames directories, but does not move them. - // MoveFile is not atomic. - auto MoveFile_result = - MoveFileW(widen(old_path).c_str(), widen(new_path).c_str()); - - if(MoveFile_result == 0) - throw system_exceptiont("MoveFileW failed"); - } - else - { - // C++17 requires this to be atomic. - // MoveFile, MoveFileEx() or rename() do not guarantee this. - // Any existing file at new_path is to be overwritten. - // rename() does not do so on Windows. - auto MoveFileEx_result = MoveFileExW( - widen(old_path).c_str(), - widen(new_path).c_str(), - MOVEFILE_REPLACE_EXISTING); // flags - - if(MoveFileEx_result == 0) - throw system_exceptiont("MoveFileExW failed"); - } -#else - int rename_result = rename(old_path.c_str(), new_path.c_str()); - - if(rename_result != 0) - throw system_exceptiont( - std::string("rename failed: ") + std::strerror(errno)); -#endif -} diff --git a/src/util/file_util.h b/src/util/file_util.h deleted file mode 100644 index 0e749a889e0..00000000000 --- a/src/util/file_util.h +++ /dev/null @@ -1,50 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - - -#ifndef CPROVER_UTIL_FILE_UTIL_H -#define CPROVER_UTIL_FILE_UTIL_H - -#include - -// C++17 will allow us to use std::filesystem::path::remove_all -void delete_directory(const std::string &path); - -// C++17 will allow us to use std::filesystem::current_path (for both get and -// set) -std::string get_current_working_directory(); -void set_current_path(const std::string &path); - -// C++17 will allow us to use std::filesystem::path(dir).append(file) -std::string concat_dir_file(const std::string &directory, - const std::string &file_name); - -// C++17 will allow us to use std::filesystem::is_directory -bool is_directory(const std::string &path); - -/// Create a directory with given path -/// C++17 will allow us to use std::filesystem::create_directory -/// \return true iff the directory was created -bool create_directory(const std::string &path); - -/// Check whether file with given path exists. -/// C++17 will allow us to use std::filesystem::directory_entry(file).exists() -/// \return true iff the file exists -bool file_exists(const std::string &path); - -// Delete a file with given path -/// C++17 will allow us to use std::filesystem::remove -/// \return true if the file was deleted, false if it did not exist -bool file_remove(const std::string &path); - -/// Rename a file. -/// C++17 will allow us to use std::filesystem::rename -/// Throws an exception on failure. -void file_rename(const std::string &old_path, const std::string &new_path); - -#endif // CPROVER_UTIL_FILE_UTIL_H diff --git a/src/util/parser.h b/src/util/parser.h index 9fc1e3c577d..70a796ec4a9 100644 --- a/src/util/parser.h +++ b/src/util/parser.h @@ -12,14 +12,14 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_PARSER_H #define CPROVER_UTIL_PARSER_H +#include "expr.h" +#include "message.h" + +#include #include #include #include -#include "expr.h" -#include "message.h" -#include "file_util.h" - class parsert { public: @@ -86,7 +86,7 @@ class parsert { source_location.set_file(file); source_location.set_working_directory( - get_current_working_directory()); + std::filesystem::current_path().string()); } irep_idt get_file() const diff --git a/src/util/source_location.cpp b/src/util/source_location.cpp index 58897b858da..44656e09e4c 100644 --- a/src/util/source_location.cpp +++ b/src/util/source_location.cpp @@ -8,11 +8,11 @@ Author: Daniel Kroening, kroening@kroening.com #include "source_location.h" -#include - -#include "file_util.h" #include "prefix.h" +#include +#include + bool source_locationt::is_built_in(const std::string &s) { std::string built_in1 = ""; @@ -37,8 +37,11 @@ std::string source_locationt::as_string(bool print_cwd) const dest+=' '; dest+="file "; if(print_cwd) - dest+= - concat_dir_file(id2string(get_working_directory()), id2string(file)); + { + dest += std::filesystem::path(id2string(get_working_directory())) + .append(id2string(file)) + .string(); + } else dest+=id2string(file); } @@ -89,7 +92,9 @@ optionalt source_locationt::full_path() const if(file.empty() || is_built_in(file)) return {}; - return concat_dir_file(id2string(get_working_directory()), file); + return std::filesystem::path(id2string(get_working_directory())) + .append(file) + .string(); } std::ostream &operator << ( diff --git a/src/util/tempdir.cpp b/src/util/tempdir.cpp index b8b0a0fe78b..c957bd3c171 100644 --- a/src/util/tempdir.cpp +++ b/src/util/tempdir.cpp @@ -8,34 +8,23 @@ Author: CM Wintersteiger #include "tempdir.h" -#ifdef _WIN32 -#include -#ifdef _MSC_VER -#pragma warning(disable:4668) - // using #if/#elif on undefined macro -#pragma warning(disable : 5039) -// pointer or reference to potentially throwing function passed to extern C -#endif -#include -#include -#include -#include -#endif - -#include -#include -#include +#include // clang-format off +#ifndef _WIN32 #if defined(__FreeBSD_kernel__) || \ defined(__CYGWIN__) || \ defined(__MACH__) #include #endif + +#include +#include +#include +#endif // clang-format on #include "exception_utils.h" -#include "file_util.h" std::string get_temporary_directory(const std::string &name_template) { @@ -43,36 +32,14 @@ std::string get_temporary_directory(const std::string &name_template) #ifdef _WIN32 (void)name_template; // unused parameter - DWORD dwBufSize = MAX_PATH + 1; - char lpPathBuffer[MAX_PATH + 1]; - DWORD dwRetVal = GetTempPathA(dwBufSize, lpPathBuffer); - - if(dwRetVal > dwBufSize || (dwRetVal == 0)) + try { - throw system_exceptiont("Couldn't get temporary path"); + result = std::filesystem::temp_directory_path().string(); } - - // GetTempFileNameA produces \
.TMP
-  // where 
 = "TLO"
-  // Thus, we must make the buffer 1+3+4+1+3=12 characters longer.
-
-  char t[MAX_PATH];
-  UINT uRetVal = GetTempFileNameA(lpPathBuffer, "TLO", 0, t);
-  if(uRetVal == 0)
+  catch(const std::filesystem::filesystem_error &)
   {
-    throw system_exceptiont(
-      std::string("Couldn't get new temporary file name in directory") +
-      lpPathBuffer);
-  }
-
-  unlink(t);
-  if(_mkdir(t) != 0)
-  {
-    throw system_exceptiont(
-      std::string("Couldn't create temporary directory at ") + t);
+    throw system_exceptiont("Failed to create temporary directory");
   }
-  result = std::string(t);
-
 #else
   std::string prefixed_name_template = "/tmp/";
   const char *TMPDIR_env = getenv("TMPDIR");
@@ -110,12 +77,12 @@ temp_dirt::temp_dirt(const std::string &name_template)
 
 std::string temp_dirt::operator()(const std::string &file)
 {
-  return concat_dir_file(path, file);
+  return std::filesystem::path(path).append(file).string();
 }
 
 void temp_dirt::clear()
 {
-  delete_directory(path);
+  std::filesystem::remove_all(path);
 }
 
 temp_dirt::~temp_dirt()
diff --git a/src/util/tempfile.cpp b/src/util/tempfile.cpp
index 278c115d8a5..ad0e6dec577 100644
--- a/src/util/tempfile.cpp
+++ b/src/util/tempfile.cpp
@@ -33,9 +33,9 @@ Author: Daniel Kroening
 
 #include 
 #include 
+#include 
 
 #include "exception_utils.h"
-#include "file_util.h"
 
 #if defined(__linux__) || \
     defined(__FreeBSD_kernel__) || \
@@ -145,5 +145,5 @@ std::string get_temporary_file(
 temporary_filet::~temporary_filet()
 {
   if(!name.empty())
-    file_remove(name);
+    std::filesystem::remove(name);
 }
diff --git a/unit/Makefile b/unit/Makefile
index de364726e36..af2afbb0207 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -141,7 +141,6 @@ SRC += analyses/ai/ai.cpp \
        util/expr_initializer.cpp \
        util/expr.cpp \
        util/expr_iterator.cpp \
-       util/file_util.cpp \
        util/format.cpp \
        util/format_expr.cpp \
        util/format_number_range.cpp \
diff --git a/unit/util/file_util.cpp b/unit/util/file_util.cpp
deleted file mode 100644
index 93c03fcfa92..00000000000
--- a/unit/util/file_util.cpp
+++ /dev/null
@@ -1,72 +0,0 @@
-/*******************************************************************\
-
-Module: Unit tests for file_util.h
-
-Author: Daniel Kroening
-
-\*******************************************************************/
-
-#include  // IWYU pragma: keep
-#include 
-#include 
-
-#include 
-
-#ifdef _MSC_VER
-#  include 
-#endif
-
-#include 
-
-TEST_CASE("concat_dir_file functionality", "[core][util][file_util]")
-{
-  temp_dirt temp_dir("testXXXXXX");
-  const std::string path = concat_dir_file(temp_dir.path, "bla.txt");
-
-  REQUIRE(path.size() > temp_dir.path.size() + std::string("bla.txt").size());
-#ifdef _WIN32
-  REQUIRE(path.find('\\') != std::string::npos);
-#else
-  REQUIRE(path.find('/') != std::string::npos);
-#endif
-
-#ifdef _WIN32
-  const std::string qualified_path = "z:\\some\\path\\foo.txt";
-#else
-  const std::string qualified_path = "/some/path/foo.txt";
-#endif
-  const std::string path2 = concat_dir_file(temp_dir.path, qualified_path);
-  REQUIRE(path2 == qualified_path);
-}
-
-TEST_CASE("is_directory functionality", "[core][util][file_util]")
-{
-  temp_dirt temp_dir("testXXXXXX");
-
-#ifdef _MSC_VER
-  std::ofstream outfile(widen(temp_dir("file")));
-#else
-  std::ofstream outfile(temp_dir("file"));
-#endif
-
-  outfile.close();
-
-  REQUIRE(is_directory(temp_dir.path));
-  REQUIRE(is_directory(temp_dir.path+"/"));
-  REQUIRE(!is_directory(temp_dir("whatnot")));
-  REQUIRE(!is_directory(temp_dir("file")));
-  REQUIRE(!is_directory(""));
-}
-
-TEST_CASE("get/set working directory", "[core][util][file_util]")
-{
-  temp_dirt temp_dir("testXXXXXX");
-
-  std::string cwd = get_current_working_directory();
-  REQUIRE(cwd != temp_dir.path);
-  set_current_path(temp_dir.path);
-  REQUIRE(get_current_working_directory() == temp_dir.path);
-  REQUIRE_THROWS_AS(set_current_path("no-such-dir"), system_exceptiont);
-
-  set_current_path(cwd);
-}

From 130fd655e917980071fbea696f21122febef8332 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig 
Date: Mon, 13 Nov 2023 16:38:06 +0000
Subject: [PATCH 5/7] Fix invalid-escape-sequence warning

Python warns about the use of `\d`: we should use raw strings here as
that's not meant to be an escape sequence.
---
 .github/workflows/pull-request-check-rust-api.yaml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/pull-request-check-rust-api.yaml b/.github/workflows/pull-request-check-rust-api.yaml
index a3faf73c8eb..2877f9b279b 100644
--- a/.github/workflows/pull-request-check-rust-api.yaml
+++ b/.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
@@ -102,7 +102,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

From 7320b811919b826a7eed996f0e612003f462a8da Mon Sep 17 00:00:00 2001
From: Michael Tautschnig 
Date: Tue, 14 Nov 2023 12:08:16 +0000
Subject: [PATCH 6/7] Fix libstdc++-not-found error

See
https://github.com/diffblue/cbmc/actions/runs/6856483568/job/18643716705?pr=6749
for one example of the failure: cargo-induced clang runs (via the cc
crate) weren't finding the C++ library (which ought to be libc++ and not
libstdc++ on this MacOS target). This appears to be caused by the
minimum build target being too low (where the cc crate is the one
setting that minimum). Override that by setting an environment variable.
See
https://github.com/rust-lang/cc-rs/blob/2d6a3b2119cf5eacc01e1f2877e064a7aede7819/src/lib.rs#L3497C52-L3497C76
for the Rust code implementing the logic.
---
 .github/workflows/pull-request-check-rust-api.yaml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/pull-request-check-rust-api.yaml b/.github/workflows/pull-request-check-rust-api.yaml
index 2877f9b279b..c5ef1204165 100644
--- a/.github/workflows/pull-request-check-rust-api.yaml
+++ b/.github/workflows/pull-request-check-rust-api.yaml
@@ -102,6 +102,7 @@ jobs:
       # by the other jobs already present in `pull-request-checks.yaml`.
       - name: Run Rust API tests
         run: |
+          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;\

From 6e1615c79880dce38fc8ef56ca130cf9ded74282 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig 
Date: Tue, 14 Nov 2023 12:38:54 +0000
Subject: [PATCH 7/7] Fix ccache configuration of
 check-macos-12-cmake-clang-rust

The prefix lookup resulted in picking up the Release-Glucose cache from
check-macos-12-cmake-clang. This cache, however, was established with
Glucose as a SAT solver, which implies different compiler
command lines. Consequently, there would be 0 cache hits.
---
 .github/workflows/pull-request-check-rust-api.yaml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/pull-request-check-rust-api.yaml b/.github/workflows/pull-request-check-rust-api.yaml
index c5ef1204165..33ba405efe0 100644
--- a/.github/workflows/pull-request-check-rust-api.yaml
+++ b/.github/workflows/pull-request-check-rust-api.yaml
@@ -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