ansi_c_entry_point: avoid magic number

regression/cbmc/argv2/main.i

@@ -0,0 +1,6 @@
+int main(int argc, char *argv[])
+{
+  __CPROVER_assert(
+    sizeof(char *) > sizeof(int) || argc < 0x7FFFFFFF,
+    "argc cannot reach INT_MAX on 32-bit systems");
+}

regression/cbmc/argv2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.i
+--32
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/multiple-goto-traces/test.desc

@@ -5,7 +5,7 @@ activate-multi-line-match
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED
-Trace for main\.assertion\.1:(\n.*){22}  assertion 4 \!= argc(\n.*){5}Trace for main\.assertion\.3:(\n.*){36}  assertion argc != 4(\n.*){5}Trace for main\.assertion\.4:(\n.*){50}  assertion argc \+ 1 != 5
+Trace for main\.assertion\.1:((\n.*){19}|(\n.*){22})  assertion 4 \!= argc(\n.*){5}Trace for main\.assertion\.3:((\n.*){33}|(\n.*){36})  assertion argc != 4(\n.*){5}Trace for main\.assertion\.4:((\n.*){47}|(\n.*){50})  assertion argc \+ 1 != 5
 \*\* 3 of 4 failed
 --
 ^warning: ignoring

src/ansi-c/ansi_c_entry_point.cpp

@@ -313,12 +313,10 @@ bool generate_ansi_c_start_function(
         init_code.add(code_assumet(std::move(ge)));
       }
 
+      if(config.ansi_c.max_argc.has_value())
       {
-        // assume argc is at most MAX/8-1
-        mp_integer upper_bound=
-          power(2, config.ansi_c.int_width-4);
-
-        exprt bound_expr=from_integer(upper_bound, argc_symbol.type);
+        exprt bound_expr =
+          from_integer(*config.ansi_c.max_argc, argc_symbol.type);
 
         binary_relation_exprt le(
           argc_symbol.symbol_expr(), ID_le, std::move(bound_expr));

src/util/config.cpp

@@ -1146,6 +1146,29 @@ bool configt::set(const cmdlinet &cmdline)
   if(cmdline.isset("cpp11"))
     cpp.set_cpp11();
 
+  // set the upper bound for argc
+  if(os == "windows")
+  {
+    // On Windows, CreateProcess accepts no more than 32767 characters, so make
+    // that a hard limit.
+    ansi_c.max_argc = mp_integer{32767};
+  }
+  else
+  {
+    // For other systems assume argc is no larger than the what would make argv
+    // consume all available memory space:
+    // 2^pointer_width / (pointer_width / char_width) is the maximum number of
+    // argv elements sysconf(ARG_MAX) is likely much lower than this, but we
+    // don't know that value for the verification target platform.
+    const auto pointer_bits_2log =
+      address_bits(ansi_c.pointer_width / ansi_c.char_width);
+    if(ansi_c.pointer_width - pointer_bits_2log <= ansi_c.int_width)
+    {
+      ansi_c.max_argc = power(2, config.ansi_c.int_width - pointer_bits_2log);
+    }
+    // otherwise we leave argc unconstrained
+  }
+
   return false;
 }
 

src/util/config.h

@@ -258,6 +258,11 @@ class configt
     malloc_failure_modet malloc_failure_mode = malloc_failure_mode_none;
 
     static const std::size_t default_object_bits = 8;
+
+    /// Maximum value of argc, which is operating-systems dependent: Windows
+    /// limits the number of characters accepte by CreateProcess, and Unix
+    /// systems have sysconf(ARG_MAX).
+    optionalt<mp_integer> max_argc;
   } ansi_c;
 
   struct cppt