Java bytecode front-end: fix static field is_static_lifetime flag

jbmc/regression/jbmc/static_field_missing_class/a.java

@@ -0,0 +1,5 @@
+class a  {
+  public static void fun() {
+    assert b.x > 0;
+  }
+}

jbmc/regression/jbmc/static_field_missing_class/test.desc

@@ -0,0 +1,7 @@
+CORE
+a.class
+--function a.fun --show-symbol-table
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

jbmc/src/java_bytecode/java_bytecode_typecheck.cpp

@@ -26,6 +26,16 @@ std::string java_bytecode_typecheckt::to_string(const typet &type)
 void java_bytecode_typecheckt::typecheck_non_type_symbol(symbolt &symbol)
 {
   PRECONDITION(!symbol.is_type);
+
+  // Static fields should be marked with is_static_lifetime.
+  // In case the symbol was created without this flag (e.g., through stubbing),
+  // ensure it's set correctly based on whether this is a static field.
+  // Static fields have ID_C_field set on their type.
+  if(symbol.type.find(ID_C_field).is_not_nil() && !symbol.is_static_lifetime)
+  {
+    symbol.is_static_lifetime = true;
+  }
+
   typecheck_type(symbol.type);
   typecheck_expr(symbol.value);
 }

jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp

@@ -71,10 +71,19 @@ void java_bytecode_typecheckt::typecheck_expr_symbol(symbol_exprt &expr)
 
   // the java_bytecode_convert_class and java_bytecode_convert_method made sure
   // "identifier" exists in the symbol table
-  const symbolt &symbol = symbol_table.lookup_ref(identifier);
+  symbolt &symbol = symbol_table.get_writeable_ref(identifier);
 
   INVARIANT(!symbol.is_type, "symbol identifier should not be a type");
 
+  // Static fields should be marked with is_static_lifetime.
+  // In case the symbol was created without this flag (e.g., through stubbing),
+  // ensure it's set correctly based on whether this is a static field.
+  // Static fields have ID_C_field set on their type.
+  if(symbol.type.find(ID_C_field).is_not_nil() && !symbol.is_static_lifetime)
+  {
+    symbol.is_static_lifetime = true;
+  }
+
   // type the expression
   expr.type() = symbol.type;
 }