diff --git a/regression/cbmc/object-bits-parsing/non_numeric.desc b/regression/cbmc/object-bits-parsing/non_numeric.desc new file mode 100644 index 00000000000..ca52caf9c89 --- /dev/null +++ b/regression/cbmc/object-bits-parsing/non_numeric.desc @@ -0,0 +1,10 @@ +CORE +test.c +--object-bits foobar +Value of "foobar" given for object-bits is not a valid unsigned integer. +object-bits must be positive and less than the pointer width +^EXIT=1$ +^SIGNAL=0$ +-- +-- +Test parsing of an invalid non numeric object-bits setting. diff --git a/regression/cbmc/object-bits-parsing/test.c b/regression/cbmc/object-bits-parsing/test.c new file mode 100644 index 00000000000..ab41fe78143 --- /dev/null +++ b/regression/cbmc/object-bits-parsing/test.c @@ -0,0 +1,8 @@ + +#include +#include + +int main(int argc, char **argv) +{ + void *p = malloc(1); +} diff --git a/regression/cbmc/object-bits-parsing/too_large.desc b/regression/cbmc/object-bits-parsing/too_large.desc new file mode 100644 index 00000000000..4bf82c9dc95 --- /dev/null +++ b/regression/cbmc/object-bits-parsing/too_large.desc @@ -0,0 +1,10 @@ +CORE +test.c +--object-bits 65 +Value of "65" given for object-bits is out of range. +object-bits must be positive and less than the pointer width +^EXIT=1$ +^SIGNAL=0$ +-- +-- +Test parsing of a too large object-bits setting. diff --git a/regression/cbmc/object-bits-parsing/valid.desc b/regression/cbmc/object-bits-parsing/valid.desc new file mode 100644 index 00000000000..6cf345f5522 --- /dev/null +++ b/regression/cbmc/object-bits-parsing/valid.desc @@ -0,0 +1,8 @@ +CORE +test.c +--object-bits 8 +^EXIT=0$ +^SIGNAL=0$ +-- +-- +Test parsing of a valid object-bits setting. diff --git a/regression/cbmc/object-bits-parsing/zero.desc b/regression/cbmc/object-bits-parsing/zero.desc new file mode 100644 index 00000000000..4471b3c7337 --- /dev/null +++ b/regression/cbmc/object-bits-parsing/zero.desc @@ -0,0 +1,10 @@ +CORE +test.c +--object-bits 0 +Value of "0" given for object-bits is out of range. +object-bits must be positive and less than the pointer width +^EXIT=1$ +^SIGNAL=0$ +-- +-- +Test parsing of a too small object-bits setting. diff --git a/src/util/config.cpp b/src/util/config.cpp index 889b48b984e..8c2db0d4bb6 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -765,16 +765,42 @@ void configt::set_arch(const irep_idt &arch) } } +/// \brief Parses the `object_bits` argument from the command line arguments. +/// \param argument The command line argument to parse the `object_bits` from. +/// \param pointer_width The width of a pointer in bits. This is used to check +/// the value of object_bits is within the valid range. +/// \return A `bv_encodingt` on successful parsing. In the case where an invalid +/// argument is specified, an `invalid_command_line_argument_exceptiont` will +/// be thrown. +configt::bv_encodingt parse_object_bits_encoding( + const std::string &argument, + const std::size_t pointer_width) +{ + const auto throw_for_reason = [&](const std::string &reason) { + throw invalid_command_line_argument_exceptiont( + "Value of \"" + argument + "\" given for object-bits is " + reason + + ". object-bits must be positive and less than the pointer width (" + + std::to_string(pointer_width) + ") ", + "--object_bits"); + }; + const auto object_bits = string2optional(argument); + if(!object_bits) + throw_for_reason("not a valid unsigned integer"); + if(*object_bits == 0 || *object_bits >= pointer_width) + throw_for_reason("out of range"); + + configt::bv_encodingt bv_encoding; + bv_encoding.object_bits = *object_bits; + bv_encoding.is_object_bits_default = false; + return bv_encoding; +} + bool configt::set(const cmdlinet &cmdline) { // defaults -- we match the architecture we have ourselves cpp.cpp_standard=cppt::default_cpp_standard(); - bv_encoding.object_bits=bv_encoding.default_object_bits; - // This will allow us to override by language defaults later. - bv_encoding.is_object_bits_default=true; - ansi_c.single_precision_constant=false; ansi_c.for_has_scope=true; // C99 or later ansi_c.ts_18661_3_Floatn_types=false; @@ -1078,19 +1104,8 @@ bool configt::set(const cmdlinet &cmdline) if(cmdline.isset("object-bits")) { - bv_encoding.object_bits= - unsafe_string2unsigned(cmdline.get_value("object-bits")); - - if(!(0 -optionalt string2optional(const std::string &str, int base) +optionalt string2optional(const std::string &str, int base = 10) { return wrap_string_conversion([&]() { return narrow_or_throw_out_of_range(string2optional_base(str, base));