From 057e4da613ccafa5b5f7da5f5038e1dfa7eddbbb Mon Sep 17 00:00:00 2001
From: Antonia Lechner <antonia.lechner@diffblue.com>
Date: Tue, 2 Jul 2019 15:27:57 +0100
Subject: [PATCH] Do not store duplicates of inherited static fields

In the tests for static-values, we previously stored the value for an
inherited static field twice, when it fact it is only needed in its
declaring class.
---
 .../deterministic_assignments_json/clinit-state.json  |  4 ----
 .../src/main/java/org/cprover/JsonGenerator.java      | 11 ++---------
 2 files changed, 2 insertions(+), 13 deletions(-)

diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/clinit-state.json b/jbmc/regression/jbmc/deterministic_assignments_json/clinit-state.json
index 8d341195fa4..9d0f8e61e60 100644
--- a/jbmc/regression/jbmc/deterministic_assignments_json/clinit-state.json
+++ b/jbmc/regression/jbmc/deterministic_assignments_json/clinit-state.json
@@ -313,10 +313,6 @@
       "@type":"java.lang.Long",
       "value":"9223372036854775807"
     },
-    "inheritedStatic":{
-      "@type":"java.lang.Integer",
-      "value":10
-    },
     "interfaceContainerFirst":{
       "@type":"MyInterfaceContainerA",
       "field":{
diff --git a/jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/JsonGenerator.java b/jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/JsonGenerator.java
index 88ce6c71669..3a96dd748d0 100644
--- a/jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/JsonGenerator.java
+++ b/jbmc/regression/jbmc/deterministic_assignments_json/src/main/java/org/cprover/JsonGenerator.java
@@ -73,7 +73,7 @@ public static String classNameFromFile(File file) {
 
   public static StaticFieldMap<Object> staticFieldMap(Class<?> clazz) {
     StaticFieldMap<Object> staticFields = new StaticFieldMap<>();
-    for (Field field : getAllStaticFields(clazz)) {
+    for (Field field : getDeclaredStaticFields(clazz)) {
       field.setAccessible(true);
       try {
         if (!field.getName().equals("$assertionsDisabled")) {
@@ -88,20 +88,13 @@ public static StaticFieldMap<Object> staticFieldMap(Class<?> clazz) {
     return staticFields;
   }
 
-  public static List<Field> getAllStaticFields(Class<?> clazz) {
+  public static List<Field> getDeclaredStaticFields(Class<?> clazz) {
     List<Field> fields = new ArrayList<>();
-    if (clazz == null) {
-      return fields;
-    }
     for (Field field : clazz.getDeclaredFields()) {
       if ((field.getModifiers() & Modifier.STATIC) == Modifier.STATIC) {
         fields.add(field);
       }
     }
-    fields.addAll(getAllStaticFields(clazz.getSuperclass()));
-    for (Class<?> interfaze : clazz.getInterfaces()) {
-      fields.addAll(getAllStaticFields(interfaze));
-    }
     return fields;
   }
 }