Small fixes

will be squashed.

Author: petr-bauch

regression/cbmc/string-refinement-strchr1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 test.c
 --refine-strings --max-nondet-string-length 10
 ^EXIT=10$

regression/cbmc/string-refinement-strchr2/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 test.c
 --refine-strings
 ^EXIT=10$

src/goto-programs/string_instrumentation.cpp

@@ -201,7 +201,7 @@ void string_instrumentation(
   message_handlert &message_handler,
   const std::string &maybe_max_nondet_string_length_string)
 {
-  size_t max_nondet_string_length = 1000; //default
+  size_t max_nondet_string_length = 1000; // default
   if(!maybe_max_nondet_string_length_string.empty())
   {
     auto maybe_max_nondet_string_length =

src/solvers/strings/string_constraint_generator_indexof.cpp

@@ -128,8 +128,8 @@ string_constraint_generatort::add_axioms_for_c_index_of(
   constraints.existential.push_back(a2);
 
   const exprt lower_bound(zero_if_negative(from_index));
-  // make sure that terminating zero exists (and is the smallest index after from
-  //  that has a 0 character)
+  // make sure that terminating zero exists (and is the smallest index after
+  // from that has a 0 character)
   constraints.existential.push_back(
     equal_exprt{str[terminating_zero], from_integer(0, c.type())});
   symbol_exprt k = fresh_symbol("QA_index_of", index_type);

src/util/pointer_offset_size.cpp

@@ -632,6 +632,17 @@ optionalt<exprt> get_subexpression_at_offset(
     return typecast_exprt(expr, target_type_raw);
   }
 
+  if(
+    offset_bytes == 0 && expr.type().id() == ID_pointer &&
+    target_type_raw.id() == ID_array)
+  {
+    // subexpression at offset zero is the whole thing even for arrays
+    return byte_extract_exprt{byte_extract_id(),
+                              expr,
+                              from_integer(offset_bytes, index_type()),
+                              target_type_raw};
+  }
+
   const typet &source_type = ns.follow(expr.type());
   const auto target_size_bits = pointer_offset_bits(target_type_raw, ns);
   if(!target_size_bits.has_value())