ansi_c_entry_point: avoid magic number

The code previously hard-coded an upper bound for argc that perhaps was
suitable for 32-bit systems (albeit even questionable for that case).
Replace this calculation by one that refers to configured bit widths.

Fixes: #1708

Author: tautschnig

regression/cbmc/argv2/main.c

@@ -0,0 +1,7 @@
+#include <assert.h>
+#include <limits.h>
+
+int main(int argc, char *argv[])
+{
+  assert(sizeof(char *) > sizeof(int) || argc < INT_MAX);
+}

regression/cbmc/argv2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--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,18 +313,42 @@ bool generate_ansi_c_start_function(
         init_code.add(code_assumet(std::move(ge)));
       }
 
+      // On Windows, CreateProcess accepts no more than 32767 characters, so
+      // make that a hard limit.
+      if(config.ansi_c.os == configt::ansi_ct::ost::OS_WIN)
       {
-        // 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(32767, argc_symbol.type);
 
         binary_relation_exprt le(
           argc_symbol.symbol_expr(), ID_le, std::move(bound_expr));
 
         init_code.add(code_assumet(std::move(le)));
       }
+      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(config.ansi_c.pointer_width / config.ansi_c.char_width);
+        if(
+          config.ansi_c.pointer_width - pointer_bits_2log <=
+          config.ansi_c.int_width)
+        {
+          mp_integer upper_bound =
+            power(2, config.ansi_c.int_width - pointer_bits_2log);
+
+          exprt bound_expr = from_integer(upper_bound, argc_symbol.type);
+
+          binary_relation_exprt le(
+            argc_symbol.symbol_expr(), ID_le, std::move(bound_expr));
+
+          init_code.add(code_assumet(std::move(le)));
+        }
+      }
 
       // record argc as an input
       init_code.add(code_inputt{"argc", argc_symbol.symbol_expr()});