From 6ed08c11c6feeabf4749573fdee2e9835d1eb6d2 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Wed, 19 Sep 2018 12:55:26 +0100 Subject: Add checks for correct usage of the POSIX model, together with an associated test. --- runtime/POSIX/klee_init_env.c | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'runtime/POSIX') diff --git a/runtime/POSIX/klee_init_env.c b/runtime/POSIX/klee_init_env.c index 265c3bfd..511a926c 100644 --- a/runtime/POSIX/klee_init_env.c +++ b/runtime/POSIX/klee_init_env.c @@ -144,6 +144,9 @@ usage: (klee_init_env) [options] [program arguments]\n\ max_argvs = __str_to_int(argv[k++], msg); max_len = __str_to_int(argv[k++], msg); + if ( (min_argvs > max_argvs) || (min_argvs == 0 && max_argvs == 0) ) + __emit_error("Invalid range to --sym-args"); + n_args = klee_range(min_argvs, max_argvs+1, "n_args"); for (i=0; i < n_args; i++) { sym_arg_name[3] = '0' + sym_arg_num++; @@ -157,11 +160,20 @@ usage: (klee_init_env) [options] [program arguments]\n\ if (k+2 >= argc) __emit_error(msg); + + if (sym_files != 0) + __emit_error("Multiple --sym-files are not allowed.\n"); k++; sym_files = __str_to_int(argv[k++], msg); sym_file_len = __str_to_int(argv[k++], msg); + if (sym_files == 0) + __emit_error("The first argument to --sym-files (number of files) cannot be 0\n"); + + if (sym_file_len == 0) + __emit_error("The second argument to --sym-files (file size) cannot be 0\n"); + } else if (__streq(argv[k], "--sym-stdin") || __streq(argv[k], "-sym-stdin")) { const char *msg = -- cgit 1.4.1