Skip to content

Commit

Permalink
Add separate tests for assert and __goblint_check
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Jul 28, 2022
1 parent fd52938 commit 52bdd5a
Show file tree
Hide file tree
Showing 2 changed files with 20 additions and 7 deletions.
14 changes: 7 additions & 7 deletions tests/regression/00-sanity/01-assert.c
Original file line number Diff line number Diff line change
@@ -1,15 +1,15 @@
// just a few sanity checks on the asserts
#include<assert.h>
// just a few sanity checks on asserts
#include <assert.h>

int main() {
int success = 1;
int silence = 1;
int fail = 0;
int unknown;
// TODO: change back to assert?
__goblint_check(success);
__goblint_check(fail); // FAIL!
__goblint_check(unknown == 4); // UNKNOWN!
// intentionally using assert, specific order to work with assert refine
assert(success);
assert(unknown == 4); // UNKNOWN!
assert(fail); // FAIL!
return 0;
__goblint_check(silence); // NOWARN!
assert(silence); // NOWARN!
}
13 changes: 13 additions & 0 deletions tests/regression/00-sanity/32-check.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
// just a few sanity checks on checks

int main() {
int success = 1;
int silence = 1;
int fail = 0;
int unknown;
__goblint_check(success);
__goblint_check(fail); // FAIL!
__goblint_check(unknown == 4); // UNKNOWN!
return 0;
__goblint_check(silence); // NOWARN!
}

0 comments on commit 52bdd5a

Please sign in to comment.