1184c6242SDominic Chen // RUN: %clang_analyze_cc1 -analyzer-checker=core -analyzer-config faux-bodies=true,model-path=%S/Inputs/Models -analyzer-output=plist-multi-file -verify %s -o %t
2*61c848d2SHubert Tong // RUN: %normalize_plist <%t | diff -ub %S/Inputs/expected-plists/model-file.cpp.plist -
3eeccb30bSTed Kremenek 
4eeccb30bSTed Kremenek typedef int* intptr;
5eeccb30bSTed Kremenek 
6eeccb30bSTed Kremenek // This function is modeled and the p pointer is dereferenced in the model
7eeccb30bSTed Kremenek // function and there is no function definition available. The modeled
8eeccb30bSTed Kremenek // function can use any types that are available in the original translation
9eeccb30bSTed Kremenek // unit, for example intptr in this case.
10eeccb30bSTed Kremenek void modeledFunction(intptr p);
11eeccb30bSTed Kremenek 
12eeccb30bSTed Kremenek // This function is modeled and returns true if the parameter is not zero
13eeccb30bSTed Kremenek // and there is no function definition available.
14eeccb30bSTed Kremenek bool notzero(int i);
15eeccb30bSTed Kremenek 
16eeccb30bSTed Kremenek // This functions is not modeled and there is no function definition.
17eeccb30bSTed Kremenek // available
18eeccb30bSTed Kremenek bool notzero_notmodeled(int i);
19eeccb30bSTed Kremenek 
main()20eeccb30bSTed Kremenek int main() {
21eeccb30bSTed Kremenek   // There is a nullpointer dereference inside this function.
22eeccb30bSTed Kremenek   modeledFunction(0);
23eeccb30bSTed Kremenek 
24eeccb30bSTed Kremenek   int p = 0;
25eeccb30bSTed Kremenek   if (notzero(p)) {
26eeccb30bSTed Kremenek    // It is known that p != 0 because of the information provided by the
27eeccb30bSTed Kremenek    // model of the notzero function.
28eeccb30bSTed Kremenek     int j = 5 / p;
29eeccb30bSTed Kremenek   }
30eeccb30bSTed Kremenek 
31eeccb30bSTed Kremenek   if (notzero_notmodeled(p)) {
32eeccb30bSTed Kremenek    // There is no information about the value of p, because
33eeccb30bSTed Kremenek    // notzero_notmodeled is not modeled and the function definition
34eeccb30bSTed Kremenek    // is not available.
35eeccb30bSTed Kremenek     int j = 5 / p; // expected-warning {{Division by zero}}
36eeccb30bSTed Kremenek   }
37eeccb30bSTed Kremenek 
38eeccb30bSTed Kremenek   return 0;
39eeccb30bSTed Kremenek }
40eeccb30bSTed Kremenek 
41