CHC: Close POs that refer to argv[0]

We already had some logic to deal with this but not for all pointer cases.
I copy/pasted that logic over to the cases where the current version of CHC
complains for a simple hello world program that passes argv[0] to printf.

There's still an open issue where there's a precondition for 'initialized(*argv)'
that I have not addressed

Author: waskyo

CodeHawk/CHC/cchpre/cCHCheckValid.ml

@@ -1510,6 +1510,11 @@ let check_ppo_validity
        | _ -> ()
      end
 
+  | PPtrUpperBound (_, _, e, _) when is_program_name e ->
+     make
+       ("validity of pointer to program name is guaranteed by the "
+        ^ "operating system")
+
   | PPtrUpperBound (_, _, e, _) when is_null_pointer e ->
      make ("not-null of first argument is checked separately")
 
@@ -2062,6 +2067,11 @@ let check_ppo_validity
   | PInitialized (Mem e, NoOffset) when is_constant_string e ->
      make ("constant string is guaranteed to have at least one character")
 
+  | PInitializedRange (e, _) when is_program_name e ->
+     make
+       ("validity of pointer to program name is guaranteed by the "
+        ^ "operating system")
+
   | PInitializedRange (e, _) when is_null_pointer e ->
      make "null pointer does have any range, so this is trivially valid"
 
@@ -2150,6 +2160,11 @@ let check_ppo_validity
   | PNullTerminated (Const (CWStr _))
     | PNullTerminated (CastE (_, Const (CWStr _))) -> make "wide string literal"
 
+  | PNullTerminated e when is_program_name e ->
+     make
+       ("validity of pointer to program name is guaranteed by the "
+        ^ "operating system")
+
   | PNullTerminated e when is_null_pointer e ->
     make "null pointer is not subject to null-termination"