Open
Description
Steps to reproduce:
- Create a.java:
class a { public static void fun() { assert(b.x > 5); } }
- Create b.java:
public class b { static int x =5; }
- Compile a.java, which also compiles b.java:
javac a.java
- Rename b.class:
mv b.class b.class.bak
- Run cbmc on a.class with the flags
--function a.fun --cover branch --show-goto-functions
and observe that b.x is used without ever being initialised to a NONDET(int). - Run cbmc on a.class with the flags
--function a.fun --cover branch --show-symbol-table
and observe that b.x is in the symbol table but not marked as is_static_lifetime.
I believe the problem is that typecheck_expr_symbol() in java_bytecode/java_bytecode_typecheck_expr.cpp isn't passed any information about whether the symbol is static, even if we know it's called with getstatic.
Activity