michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(tests/shared/name.c): test exception

Browse source
This commit is contained in:
Leonardo de Moura 2015-08-17 18:22:59 -07:00
parent 9d486a4e88
commit 549eec8a06
2 changed files with 9 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/name.cpp
View file

@ -57,7 +57,7 @@ lean_bool lean_get_name_prefix(lean_name n, lean_name * r, lean_exception * ex)
LEAN_TRY;
check_nonnull(n);
if (to_name_ref(n).is_anonymous())
throw lean::exception("invalid argument, anonymous names does not have a prefix");
throw lean::exception("invalid argument, argument is an anonymous name");
else if (to_name_ref(n).is_atomic())
*r = of_name(new name());
else

10
src/tests/shared/name.c
View file

@ -10,12 +10,13 @@ void check(int v) {
}
int main() {
printf("Started name test\n");
lean_exception ex;
lean_name a, n1, n2, n3, n4;
lean_name a, n1, n2, n3, n4, n5;
char const * s1;
char const * s2;
char const * s3;
unsigned idx;
printf("Started name test\n");
check(lean_mk_anonymous_name(&a, &ex));
check(lean_is_anonymous_name(a));
check(lean_mk_str_name(a, "foo", &n1, &ex));
@ -33,6 +34,9 @@ int main() {
check(lean_name_eq(n2, n4));
check(lean_get_name_idx(n3, &idx, &ex));
check(idx == 1);
check(!lean_get_name_prefix(a, &n5, &ex));
s3 = lean_get_exception_message(ex);
printf("Lean exception: %s\n", s3);
lean_del_name(a);
lean_del_name(n1);
lean_del_name(n2);
@ -40,5 +44,7 @@ int main() {
lean_del_name(n4);
lean_del_string(s1);
lean_del_string(s2);
lean_del_string(s3);
lean_del_exception(ex);
return 0;
}