aboutsummaryrefslogtreecommitdiff
path: root/test/symbolic/klee/viml_expressions_lexer.c
diff options
context:
space:
mode:
authorZyX <kp-pav@yandex.ru>2017-09-28 00:40:25 +0300
committerZyX <kp-pav@yandex.ru>2017-10-08 22:25:08 +0300
commit9fa8f7fc0a24371f7956450d840bdae8a2fc9a51 (patch)
treec561ac7b67b68a811873834fafa4fa5f423fd384 /test/symbolic/klee/viml_expressions_lexer.c
parent0987d3b10f36202e9f0289b50298e69aaf2fa4d2 (diff)
downloadrneovim-9fa8f7fc0a24371f7956450d840bdae8a2fc9a51.tar.gz
rneovim-9fa8f7fc0a24371f7956450d840bdae8a2fc9a51.tar.bz2
rneovim-9fa8f7fc0a24371f7956450d840bdae8a2fc9a51.zip
viml/parser/expressions: Add a way to adjust lexer
It also adds support for kExprLexOr which for some reason was forgotten. It was only made sure that KLEE test compiles in non-KLEE mode, not that something works or that KLEE is able to run tests.
Diffstat (limited to 'test/symbolic/klee/viml_expressions_lexer.c')
-rw-r--r--test/symbolic/klee/viml_expressions_lexer.c24
1 files changed, 19 insertions, 5 deletions
diff --git a/test/symbolic/klee/viml_expressions_lexer.c b/test/symbolic/klee/viml_expressions_lexer.c
index e3b5aa80cc..67f3eb7faa 100644
--- a/test/symbolic/klee/viml_expressions_lexer.c
+++ b/test/symbolic/klee/viml_expressions_lexer.c
@@ -34,13 +34,20 @@ int main(const int argc, const char *const *const argv,
{
char input[INPUT_SIZE];
uint8_t shift;
- const bool peek = false;
+ int flags;
avoid_optimizing_out = argc;
+#ifndef USE_KLEE
+ sscanf(argv[2], "%d", &flags);
+#endif
+
#ifdef USE_KLEE
klee_make_symbolic(input, sizeof(input), "input");
klee_make_symbolic(&shift, sizeof(shift), "shift");
+ klee_make_symbolic(&flags, sizeof(flags), "flags");
klee_assume(shift < INPUT_SIZE);
+ klee_assume(flags <= (kELFlagPeek|kELFlagAllowFloat|kELFlagForbidEOC
+ |kELFlagForbidScope|kELFlagIsNotCmp));
#endif
ParserLine plines[] = {
@@ -79,8 +86,15 @@ int main(const int argc, const char *const *const argv,
};
kvi_init(pstate.reader.lines);
- LexExprToken token = viml_pexpr_next_token(&pstate, peek);
- assert((pstate.pos.line == 0)
- ? (pstate.pos.col > 0)
- : (pstate.pos.line == 1 && pstate.pos.col == 0));
+ allocated_memory_limit = 0;
+ LexExprToken token = viml_pexpr_next_token(&pstate, flags);
+ if (flags & kELFlagPeek) {
+ assert(pstate.pos.line == 0 && pstate.pos.col == 0);
+ } else {
+ assert((pstate.pos.line == 0)
+ ? (pstate.pos.col > 0)
+ : (pstate.pos.line == 1 && pstate.pos.col == 0));
+ }
+ assert(allocated_memory == 0);
+ assert(ever_allocated_memory == 0);
}