umount-test-opts

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