umount-test-opts

 1#include <assert.h>
 2#include <ctype.h>
 3#include <string.h>
 4#include <stdio.h>
 5
 6#include "busybox.h"
 7#include "util-linux.h"
 8
 9#include <klee/klee.h>
10
11int
12main(int argc, char **argv)
13{
14	char options[8];
15	char pattern[8];
16
17	klee_make_symbolic(&options, sizeof(options), "options");
18	for (int i = 0; i < sizeof(options) - 1; i++)
19		klee_assume(isalpha(options[i]) || options[i] == ',' || options[i] == '+');
20	klee_assume(options[sizeof(options) - 1] == '\0');
21
22	klee_make_symbolic(&pattern, sizeof(pattern), "pattern");
23	for (int i = 0; i < sizeof(pattern) - 1; i++)
24		klee_assume(isalpha(pattern[i]) || pattern[i] == ',' || pattern[i] == '+');
25	klee_assume(pattern[sizeof(pattern) - 1] == '\0');
26
27#if 0
28	printf("options: %s\n", options);
29	printf("pattern: %s\n", pattern);
30#endif
31
32	assert(mnt_match_options(options, pattern) == fsopts_matches(options, pattern));
33	return 0;
34}