[c] setlocale(3) accepts NULL as second argument

Summary: fixes #498

Reviewed By: akotulski

Differential Revision: D4183433

fbshipit-source-id: e40fa55

infer/models/c/src/libc_basic.c

@@ -917,8 +917,14 @@ extern char* _locale_global;
 // return 0 or the allocated string _locale_global, nondeterministically
 char* setlocale(int category, const char* locale) {
   int nondet;
-  __require_allocated_array(locale);
+
   __require_allocated_array(_locale_global);
+
+  if (locale == NULL) {
+    return _locale_global;
+  }
+
+  __require_allocated_array(locale);
   nondet = __infer_nondet_int();
   if (nondet)
     return 0;

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

@@ -0,0 +1,20 @@
+/*
+ * Copyright (c) 2015 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+#include <locale.h>
+
+void nocrash_setlocale() {
+  if (setlocale(LC_ALL, NULL) == NULL) {
+    // cannot happen
+    int* p = NULL;
+    *p = 42;
+  }
+  setlocale(LC_ALL, "");
+  setlocale(LC_ALL, "C");
+}