Merge pull request #1179 from smowton/smowton/feature/well_known_globals_non_null

Mark well-known globals System.out and System.err non-null

Author: smowton

regression/cbmc-java/basic1/helloworld.class

@@ -4,7 +4,14 @@
 /* Hello World Java Program */
 class helloworld  {
     public static void main(String[] args) {
+        assert(System.out != null);
         System.out.println("Hello World!");
+        assert(System.err != null);
+        System.err.println("Hello World!");
+        assert(System.in != null);
+        try {
+          int avail = System.in.available();
+        }
+        catch(java.io.IOException e) {}
     }
 }
-

regression/cbmc-java/basic1/helloworld.java

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <algorithm>
 #include <set>
+#include <unordered_set>
 #include <iostream>
 
 #include <util/arith_tools.h>
@@ -62,7 +63,6 @@ static void create_initialize(symbol_tablet &symbol_table)
     throw "failed to add "+std::string(INITIALIZE);
 }
 
-
 static bool should_init_symbol(const symbolt &sym)
 {
   if(sym.type.id()!=ID_code &&
@@ -75,6 +75,17 @@ static bool should_init_symbol(const symbolt &sym)
   return is_java_string_literal_id(sym.name);
 }
 
+static bool is_non_null_library_global(const irep_idt &symbolid)
+{
+  static const std::unordered_set<irep_idt, irep_id_hash> non_null_globals=
+  {
+    "java::java.lang.System.out",
+    "java::java.lang.System.err",
+    "java::java.lang.System.in"
+  };
+  return non_null_globals.count(symbolid);
+}
+
 void java_static_lifetime_init(
   symbol_tablet &symbol_table,
   const source_locationt &source_location,
@@ -111,6 +122,8 @@ void java_static_lifetime_init(
             allow_null=false;
           if(allow_null && is_java_string_literal_id(nameid))
             allow_null=false;
+          if(allow_null && is_non_null_library_global(nameid))
+            allow_null=false;
         }
         auto newsym=object_factory(
           sym.type,