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.

Author: tautschnig

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

@@ -311,10 +311,18 @@ bool generate_ansi_c_start_function(
         init_code.add(code_assumet(std::move(ge)));
       }
 
+      // 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
+      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)
       {
-        // assume argc is at most MAX/8-1
-        mp_integer upper_bound=
-          power(2, config.ansi_c.int_width-4);
+        mp_integer upper_bound =
+          power(2, config.ansi_c.int_width - pointer_bits_2log);
 
         exprt bound_expr=from_integer(upper_bound, argc_symbol.type);