From a1798ed331d33d5f00065c0ee81c4060a597730f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 18 Aug 2015 12:18:33 -0700
Subject: [PATCH] test(tests/shared): add test for the options C API

---
 src/tests/shared/CMakeLists.txt |  6 +++
 src/tests/shared/name.c         | 12 +++++-
 src/tests/shared/options.c      | 75 +++++++++++++++++++++++++++++++++
 3 files changed, 91 insertions(+), 2 deletions(-)
 create mode 100644 src/tests/shared/options.c

diff --git a/src/tests/shared/CMakeLists.txt b/src/tests/shared/CMakeLists.txt
index 86462a61e..19301c43c 100644
--- a/src/tests/shared/CMakeLists.txt
+++ b/src/tests/shared/CMakeLists.txt
@@ -9,3 +9,9 @@ target_link_libraries(c_name_test ${EXTRA_LIBS} leanshared)
 add_test(NAME c_name_test
          WORKING_DIRECTORY "${LEAN_BINARY_DIR}"
          COMMAND "${CMAKE_CURRENT_BINARY_DIR}/c_name_test")
+
+add_executable(c_options_test options.c)
+target_link_libraries(c_options_test ${EXTRA_LIBS} leanshared)
+add_test(OPTIONS c_options_test
+         WORKING_DIRECTORY "${LEAN_BINARY_DIR}"
+         COMMAND "${CMAKE_CURRENT_BINARY_DIR}/c_options_test")
diff --git a/src/tests/shared/name.c b/src/tests/shared/name.c
index e8b09d6c9..ddf02b632 100644
--- a/src/tests/shared/name.c
+++ b/src/tests/shared/name.c
@@ -1,14 +1,22 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
 #include <stdlib.h>
 #include <stdio.h>
 #include "api/lean.h"
 
-void check(int v) {
+void check_core(int v, unsigned l) {
     if (!v) {
-        printf("test failed\n");
+        printf("Test failed at line %d\n", l);
         exit(1);
     }
 }
 
+#define check(v) check_core(v, __LINE__)
+
 void anonymous_unique() {
     lean_exception ex;
     lean_name a1, a2;
diff --git a/src/tests/shared/options.c b/src/tests/shared/options.c
new file mode 100644
index 000000000..e5f4cf30c
--- /dev/null
+++ b/src/tests/shared/options.c
@@ -0,0 +1,75 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <stdlib.h>
+#include <stdio.h>
+#include "api/lean.h"
+
+void check_core(int v, unsigned l) {
+    if (!v) {
+        printf("Test failed at line %d\n", l);
+        exit(1);
+    }
+}
+
+#define check(v) check_core(v, __LINE__)
+
+int main() {
+    lean_exception ex;
+    lean_name an, verbose, pp, pp_unicode, seed, output;
+    lean_options o1, o2, o3, o4, o5, o6;
+    char const * s1;
+    char const * s2;
+    lean_bool b; unsigned u;
+
+    check(lean_name_mk_anonymous(&an, &ex));
+    check(lean_name_mk_str(an, "verbose", &verbose, &ex));
+    check(lean_name_mk_str(an, "pp", &pp, &ex));
+    check(lean_name_mk_str(pp, "unicode", &pp_unicode, &ex));
+    check(lean_name_mk_str(an, "seed", &seed, &ex));
+    check(lean_name_mk_str(an, "output", &output, &ex));
+
+    check(lean_options_mk_empty(&o1, &ex));
+    check(lean_options_set_bool(o1, pp_unicode, lean_true, &o2, &ex));
+    check(lean_options_set_unsigned(o2, verbose, 10, &o3, &ex));
+    check(lean_options_set_double(o3, seed, 1.23, &o4, &ex));
+
+    check(lean_options_set_bool(o1, pp_unicode, lean_true, &o5, &ex));
+    check(lean_options_eq(o2, o5));
+
+    check(lean_options_to_string(o4, &s1, &ex));
+
+    printf("Lean options: %s\n", s1);
+
+    check(lean_options_get_bool(o3, pp_unicode, &b, &ex));
+    check(b == lean_true);
+
+    check(lean_options_get_unsigned(o4, verbose, &u, &ex));
+    check(u == 10);
+
+    check(lean_options_set_string(o4, output, "~/tmp/file.olean", &o6, &ex));
+
+    check(lean_options_get_string(o6, output, &s2, &ex));
+    check(strcmp("~/tmp/file.olean", s2) == 0);
+
+    lean_name_del(an);
+    lean_name_del(verbose);
+    lean_name_del(pp);
+    lean_name_del(pp_unicode);
+    lean_name_del(seed);
+    lean_name_del(output);
+
+    lean_options_del(o1);
+    lean_options_del(o2);
+    lean_options_del(o3);
+    lean_options_del(o4);
+    lean_options_del(o5);
+    lean_options_del(o6);
+
+    lean_string_del(s1);
+    lean_string_del(s2);
+    return 0;
+}