diff --git a/infer/models/c/src/libc_basic.c b/infer/models/c/src/libc_basic.c index 75ef30d46..0b1ee8f43 100644 --- a/infer/models/c/src/libc_basic.c +++ b/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(); } diff --git a/infer/tests/codetoanalyze/c/errors/null_dereference/getc.c b/infer/tests/codetoanalyze/c/errors/null_dereference/getc.c new file mode 100644 index 000000000..0e40ed302 --- /dev/null +++ b/infer/tests/codetoanalyze/c/errors/null_dereference/getc.c @@ -0,0 +1,58 @@ +#include +#include + + + +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); + } +} + + diff --git a/infer/tests/endtoend/c/NullDereferenceTest.java b/infer/tests/endtoend/c/NullDereferenceTest.java index 73968d11b..08e405bfd 100644 --- a/infer/tests/endtoend/c/NullDereferenceTest.java +++ b/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; diff --git a/infer/tests/endtoend/c/NullDereferenceTest2.java b/infer/tests/endtoend/c/NullDereferenceTest2.java new file mode 100644 index 000000000..cb3fd60de --- /dev/null +++ b/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" + ) + ); + } + */ +}