From 83f236451db313eddac09e1a418b27642f5b6110 Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Wed, 16 Nov 2016 03:04:24 -0800
Subject: [PATCH] [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               |  8 +++++++-
 .../c/errors/null_dereference/setlocale.c     | 20 +++++++++++++++++++
 2 files changed, 27 insertions(+), 1 deletion(-)
 create mode 100644 infer/tests/codetoanalyze/c/errors/null_dereference/setlocale.c

diff --git a/infer/models/c/src/libc_basic.c b/infer/models/c/src/libc_basic.c
index 293b14501..6f2911bc0 100644
--- a/infer/models/c/src/libc_basic.c
+++ b/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;
diff --git a/infer/tests/codetoanalyze/c/errors/null_dereference/setlocale.c b/infer/tests/codetoanalyze/c/errors/null_dereference/setlocale.c
new file mode 100644
index 000000000..cf9f28a3e
--- /dev/null
+++ b/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");
+}