Fixed model for getc and fgetc

Author: ddino

infer/models/c/src/libc_basic.c

@@ -702,12 +702,16 @@ int fputs(const char *str, FILE *stream) {
 // return a nondeterministic value
 int getc(FILE *stream)
 {
+  FILE tmp;
+    tmp = *stream;
   return __infer_nondet_int();
 }
 
 // return a nondeterministic value
 int fgetc(FILE *stream)
 {
+  FILE tmp;
+  tmp = *stream;
   return __infer_nondet_int();
 }
 

infer/tests/codetoanalyze/c/errors/null_dereference/getc.c

@@ -0,0 +1,58 @@
+#include <stdio.h>
+#include <stdlib.h>
+
+
+
+void crashgetc() {
+
+    
+    FILE *f;
+    int i;
+    
+    f=fopen("this_file_doesnt_exists", "r");
+      i =getc(f);
+      printf("i =%i\n", i);
+    fclose(f);
+}
+
+void nocrashgetc() {
+    
+    
+    FILE *f;
+    int i;
+    
+    f=fopen("this_file_doesnt_exists", "r");
+    
+    
+    if (f) {
+      i =getc(f);
+      printf("i =%i\n", i);
+      fclose(f);
+    }
+}
+
+void crashfgetc() {
+
+    FILE *f;
+    int i;
+    
+    f=fopen("this_file_doesnt_exists", "r");
+    i =fgetc(f);
+    printf("i =%i\n", i);
+    fclose(f);
+}
+
+void nocrashfgetc() {
+
+    FILE *f;
+    int i;
+    
+    f=fopen("this_file_doesnt_exists", "r");
+    if (f) {
+      i =fgetc(f);
+      printf("i =%i\n", i);
+        fclose(f);
+    }
+}
+
+

infer/tests/endtoend/c/NullDereferenceTest.java

@@ -22,6 +22,7 @@ public class NullDereferenceTest {
   public static final String SOURCE_FILE =
       "null_dereference/null_pointer_dereference.c";
 
+
   public static final String NULL_DEREFERENCE = "NULL_DEREFERENCE";
 
   private static InferResults inferResults;

infer/tests/endtoend/c/NullDereferenceTest2.java

@@ -0,0 +1,64 @@
+/*
+ * Copyright (c) 2013- Facebook.
+ * All rights reserved.
+ */
+
+package endtoend.c;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static utils.matchers.ResultContainsErrorInMethod.contains;
+
+
+import org.junit.BeforeClass;
+import org.junit.Test;
+
+import java.io.IOException;
+
+import utils.InferException;
+import utils.InferResults;
+
+public class NullDereferenceTest2 {
+
+  public static final String SOURCE_FILE =
+      "null_dereference/get.c";
+
+
+  public static final String NULL_DEREFERENCE = "NULL_DEREFERENCE";
+
+  private static InferResults inferResults;
+
+  @BeforeClass
+  public static void runInfer() throws InterruptedException, IOException {
+    inferResults = InferResults.loadCInferResults(
+        NullDereferenceTest2.class,
+        SOURCE_FILE);
+  }
+
+  /*
+  @Test
+  public void nullDereferenceTest2() throws InterruptedException, IOException, InferException {
+    assertThat(
+        "Results should contain null pointer dereference error",
+        inferResults,
+        contains(
+            NULL_DEREFERENCE,
+            SOURCE_FILE,
+            "crashgetc"
+        )
+    );
+  }
+
+  @Test
+  public void nullDereferenceTest2_fgetc() throws InterruptedException, IOException, InferException {
+    assertThat(
+        "Results should contain null pointer dereference error",
+        inferResults,
+        contains(
+            NULL_DEREFERENCE,
+            SOURCE_FILE,
+            "crashfgetc"
+        )
+    );
+  }
+    */
+}