null function pointer

NULL_fctn_pointer/.classpath

+<?xml version="1.0" encoding="UTF-8"?>
+<classpath>
+	<classpathentry kind="src" path="src"/>
+	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.7"/>
+	<classpathentry kind="output" path="bin"/>
+</classpath>

NULL_fctn_pointer/.project

+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+	<name>NULL_fctn_pointer</name>
+	<comment></comment>
+	<projects>
+	</projects>
+	<buildSpec>
+		<buildCommand>
+			<name>org.eclipse.jdt.core.javabuilder</name>
+			<arguments>
+			</arguments>
+		</buildCommand>
+	</buildSpec>
+	<natures>
+		<nature>org.eclipse.jdt.core.javanature</nature>
+	</natures>
+</projectDescription>

NULL_fctn_pointer/.settings/org.eclipse.jdt.core.prefs

+eclipse.preferences.version=1
+org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
+org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.7
+org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve
+org.eclipse.jdt.core.compiler.compliance=1.7
+org.eclipse.jdt.core.compiler.debug.lineNumber=generate
+org.eclipse.jdt.core.compiler.debug.localVariable=generate
+org.eclipse.jdt.core.compiler.debug.sourceFile=generate
+org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
+org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
+org.eclipse.jdt.core.compiler.source=1.7

NULL_fctn_pointer/src/Config.java

+public class Config {
+	// http://vbdb.itu.dk/#bug/linux/f7ab9b4
+	boolean CONFIG_TMPFS = true;
+	boolean CONFIG_DRM_I915 = true;
+
+	//@requires CONFIG_TMPFS;
+	boolean CONFIG_SHMEM;
+
+	static Object filler_t;
+	static int f = 0;
+
+	int some_fun(int n) {
+		return n;
+	}
+
+	protected void fill_the_filler() {
+		if (CONFIG_TMPFS) {
+			f = fill_the_f();
+			filler_t = some_fun(f);
+		} else
+			filler_t = null;
+	}
+
+	protected int fill_the_f() {
+		if (CONFIG_SHMEM) {
+			filler_t = shmem_get_inode();
+			f = (int) filler_t;
+			return f;
+		} else {
+			filler_t = ramfs_get_inode();
+			f = (int) filler_t;
+			return some_fun(f);
+		}
+
+	}
+
+	private Object ramfs_get_inode() {
+		// TODO
+		f = 7;
+		return null;
+	}
+
+	private Object shmem_get_inode() {
+		// TODO
+		f = 5;
+		return null;
+	}
+
+	static Object filler(int i) {
+		//@requires CONFIG_TMPFS;
+		return 0;
+	}
+
+	int drm_gem_object_init(Object filler_t, int readpage) {
+		readpage = shmem_file_setup(); // (9)
+		return 0;
+	}
+
+	private int shmem_file_setup() {
+		// TODO Auto-generated method stub
+		return 0;
+	}
+
+	void i915_gem_alloc_object(Object filler_t, int readpage) {
+		if (drm_gem_object_init(filler_t, readpage) != 0) // (8)
+			;
+	}
+
+	private static void do_read_cache_page(Object filler_t, Object filler) {
+		filler = filler(0);
+	}
+
+	static void read_cache_page_gfp(Object filler_t, int readpage) {
+		filler_t = (Object) readpage;
+		Object filler = filler(readpage);
+		do_read_cache_page(filler_t, filler);
+	}
+
+
+	static int i915_gem_object_get_pages_gtt(Object filler_t, int readpage) {
+		read_cache_page_gfp(filler_t, readpage);
+		return 0;
+	}
+
+
+	static int i915_gem_object_bind_to_gtt(Object filler_t, int readpage) {
+		return i915_gem_object_get_pages_gtt(filler_t, readpage); // (14)
+	}
+
+
+	static int i915_gem_object_pin(Object filler_t, int readpage) {
+		return i915_gem_object_bind_to_gtt(filler_t, readpage); // (13)
+	}
+
+
+	static int intel_init_ring_buffer(Object filler_t, int readpage) {
+		i915_gem_alloc_object(readpage); // (7) *readpage = NULL
+		return i915_gem_object_pin(filler_t, readpage); // (12)
+	}
+
+
+	private static int i915_gem_alloc_object(int readpage) {
+		return readpage = 0;
+	}
+
+
+	static int intel_init_render_ring_buffer(Object filler_t, int readpage) {
+		return intel_init_ring_buffer(filler_t, readpage); // (6)
+	}
+
+
+	static int i915_gem_init_ringbuffer(Object filler_t, int readpage) {
+		return intel_init_render_ring_buffer(filler_t, readpage); // (5)
+	}
+
+
+	static int i915_load_modeset_init(Object filler_t, int readpage) {
+		return i915_gem_init_ringbuffer(filler_t, readpage); // (4)
+	}
+
+	static int i915_driver_load() {
+		int readpage = (int) filler_t;
+		return i915_load_modeset_init(filler_t, readpage); // (3)
+	}
+	
+	//@requires CONFIG_DRM_I915;
+	public static void main(String[] args) {
+		i915_driver_load();
+	}
+
+}

NULL_fctn_pointer/stubs/java/io/IOException.java

+package java.io;
+
+/**
+ * @generated
+ */
+public class IOException extends java.lang.Exception {
+   /**
+    * @generated
+    */
+   /*@ public behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   public IOException();
+
+   /**
+    * @generated
+    */
+   /*@ public behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   public IOException(java.lang.String param0);
+
+   /**
+    * @generated
+    */
+   /*@ public behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   public IOException(java.lang.String param0, java.lang.Throwable param1);
+
+   /**
+    * @generated
+    */
+   /*@ public behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   public IOException(java.lang.Throwable param0);
+}
\ No newline at end of file

NULL_fctn_pointer/stubs/java/io/Serializable.java

+package java.io;
+
+/**
+ * @generated
+ */
+public interface Serializable {
+}
\ No newline at end of file

NULL_fctn_pointer/stubs/java/lang/AbstractStringBuilder.java

+package java.lang;
+
+/**
+ * @generated
+ */
+abstract class AbstractStringBuilder extends java.lang.Object implements java.lang.Appendable, java.lang.CharSequence {
+}
\ No newline at end of file

NULL_fctn_pointer/stubs/java/lang/Appendable.java

+package java.lang;
+
+/**
+ * @generated
+ */
+public interface Appendable {
+}
\ No newline at end of file

NULL_fctn_pointer/stubs/java/lang/ArithmeticException.java

+package java.lang;
+
+/**
+ * @generated
+ */
+public class ArithmeticException extends java.lang.RuntimeException {
+   /**
+    * @generated
+    */
+   /*@ public behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   public ArithmeticException();
+
+   /**
+    * @generated
+    */
+   /*@ public behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   public ArithmeticException(java.lang.String param0);
+}
\ No newline at end of file

NULL_fctn_pointer/stubs/java/lang/ArrayIndexOutOfBoundsException.java

+package java.lang;
+
+/**
+ * @generated
+ */
+public class ArrayIndexOutOfBoundsException extends java.lang.IndexOutOfBoundsException {
+   /**
+    * @generated
+    */
+   /*@ public behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   public ArrayIndexOutOfBoundsException();
+
+   /**
+    * @generated
+    */
+   /*@ public behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   public ArrayIndexOutOfBoundsException(int param0);
+
+   /**
+    * @generated
+    */
+   /*@ public behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   public ArrayIndexOutOfBoundsException(java.lang.String param0);
+}
\ No newline at end of file

NULL_fctn_pointer/stubs/java/lang/ArrayStoreException.java

+package java.lang;
+
+/**
+ * @generated
+ */
+public class ArrayStoreException extends java.lang.RuntimeException {
+   /**
+    * @generated
+    */
+   /*@ public behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   public ArrayStoreException();
+
+   /**
+    * @generated
+    */
+   /*@ public behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   public ArrayStoreException(java.lang.String param0);
+}
\ No newline at end of file

NULL_fctn_pointer/stubs/java/lang/AssertionError.java

+package java.lang;
+
+/**
+ * @generated
+ */
+public class AssertionError extends java.lang.Error {
+   /**
+    * @generated
+    */
+   /*@ public behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   public AssertionError();
+
+   /**
+    * @generated
+    */
+   /*@ public behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   public AssertionError(java.lang.Object param0);
+
+   /**
+    * @generated
+    */
+   /*@ public behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   public AssertionError(boolean param0);
+
+   /**
+    * @generated
+    */
+   /*@ public behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   public AssertionError(char param0);
+
+   /**
+    * @generated
+    */
+   /*@ public behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   public AssertionError(int param0);
+
+   /**
+    * @generated
+    */
+   /*@ public behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   public AssertionError(long param0);
+}
\ No newline at end of file

NULL_fctn_pointer/stubs/java/lang/CharSequence.java

+package java.lang;
+
+/**
+ * @generated
+ */
+public interface CharSequence {
+}
\ No newline at end of file

NULL_fctn_pointer/stubs/java/lang/Character.java

+package java.lang;
+
+/**
+ * @generated
+ */
+public final class Character extends java.lang.Object implements java.io.Serializable, java.lang.Comparable {
+   /**
+    * @generated
+    */
+   /*@ public behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   public static int digit(char param0, int param1);
+}
\ No newline at end of file

NULL_fctn_pointer/stubs/java/lang/Class.java

+package java.lang;
+
+/**
+ * @generated
+ */
+public final class Class extends java.lang.Object implements java.io.Serializable, java.lang.reflect.GenericDeclaration, java.lang.reflect.Type, java.lang.reflect.AnnotatedElement {
+   /**
+    * @generated
+    */
+   /*@ private behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   private Class();
+}
\ No newline at end of file

NULL_fctn_pointer/stubs/java/lang/ClassCastException.java

+package java.lang;
+
+/**
+ * @generated
+ */
+public class ClassCastException extends java.lang.RuntimeException {
+   /**
+    * @generated
+    */
+   /*@ public behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   public ClassCastException();
+
+   /**
+    * @generated
+    */
+   /*@ public behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   public ClassCastException(java.lang.String param0);
+}
\ No newline at end of file

NULL_fctn_pointer/stubs/java/lang/CloneNotSupportedException.java

+package java.lang;
+
+/**
+ * @generated
+ */
+public class CloneNotSupportedException extends java.lang.Exception {
+   /**
+    * @generated
+    */
+   /*@ public behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   public CloneNotSupportedException();
+
+   /**
+    * @generated
+    */
+   /*@ public behavior
+     @ requires true;
+     @ ensures true;
+     @ assignable \everything;
+     @*/
+   public CloneNotSupportedException(java.lang.String param0);
+}
\ No newline at end of file

NULL_fctn_pointer/stubs/java/lang/Cloneable.java

+package java.lang;
+
+/**
+ * @generated
+ */
+public interface Cloneable {
+}
\ No newline at end of file

NULL_fctn_pointer/stubs/java/lang/Comparable.java

+package java.lang;
+
+/**
+ * @generated
+ */
+public interface Comparable {
+}
\ No newline at end of file