[sledge] Add definitions to llair_intrinsics for assert

Summary:
This diff `#define`s the functions to which `assert` compiles to
`abort`. This enables the analyzer to report assertion violations, and
is independent of platform.

Also add a simple test to check that it is detected correctly.

Reviewed By: ngorogiannis

Differential Revision: D27564870

fbshipit-source-id: 5517ca910

sledge/model/llair_intrinsics.h

@@ -23,6 +23,12 @@ __attribute__((noreturn)) void __llair_throw(void* thrown_exception);
 /* executions that call __llair_unreachable are assumed to be impossible */
 __attribute__((noreturn)) void __llair_unreachable();
 
+/* glibc version */
+#define __assert_fail(assertion, file, line, function) abort()
+
+/* macos version */
+#define __assert_rtn(function, file, line, assertion) abort()
+
 #ifdef __cplusplus
 }
 #endif

sledge/test/analyze/assert.c

@@ -0,0 +1,13 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+#include <assert.h>
+
+void main() {
+  int x, y;
+  assert(x != y);
+}