| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
this function can be used to modify the control flow of the program
on different paths, enabling self-modifying code.
|
|
|
|
|
|
|
|
|
|
Improves querying of the .stats file, reduces its size, speeds up reads and
writes and has better defined fail behaviour.
|
|
|
|
|
|
* Added handling of --sym-arg
* Resolved the crash when minimum and maximum number of arguments for --sym-args are equal
* Replaced "range" with "n_args" produced by --sym-args
* Added model_version variable (constrained to 1), to prevent klee complaining about insufficient input
* Allow a single dash to prefix an option
* Arrange the elements in the correct order: command-line arguments, files, stdin, stdout
* Added test/Runtime/POSIX/GenRandomBout.c test, with a substitution for %gen-random-bout in test/lit.cfg
|
|
|
|
|
|
|
|
|
|
Compilers are allowed to hoist function calls and do GVE.
This is currently done even without `--optimization` enabled.
This is unfortunate in the context of KLEE function calls that might
depend on specific code position without direct control flow
dependencies. In such cases, function calls can be hoisted.
To circumvent this, disallow to optimise functions that contain such
calls by default. This might reduce optimisation for some functions
containing such function calls but still allows it for all others.
This patch adds an additional pass, that detects all functions starting with a
prefix `klee_` and disable optimisations for functions containing such
calls.
This is enabled by default but can be disabled by
`--klee-call-optimisation=false`.
|
|
|
|
* remove wrapper script invocation and script
* add build instruction to test cases
* added additional checks
* add check to avoid execution of tests if KLEE is not compiled with
libc++
|
|
|
|
placed them in the seeding category. Moved options and option categories in Executor.cpp to the klee namespace.
|
|
category (with --write-cov, --write-cvcs etc.)
|
|
|
|
|
|
|
|
function and updated some .ll tests to use --optimize=false instead of --disable-opt
|
|
|
|
|
|
|
|
|
|
|
|
* switch to Python 3
* add file encoding
* some PEP8 reformatting
* fix TOCTOU for open
* replace trimZeros() with rstrip
* remove unused pos/args variables
* remove --write-ints (print by default)
* remove progname section (unused)
* added/modified output rows
- "data:" now shows the Python representation (for use in scripts)
- "hex :" shows the hex representation
- "text:" shows ASCII, all out-of-range/non-printable characters are replaced by a dot
- "int :"/"uint:" print (unsigned) 8/16/32/64 bit integers
* reduce width for object counter to needed minimum instead of 4
* refactor printing into function
|
|
original --run-in option to --running-dir
|
|
|
|
|
|
`-O0` has to be used in conjunction with, not instead of
`-Xclang -disable-O0-optnone`
|
|
|
|
Check if a state reaches the maximum number of stack frames allowed.
To be performant, the number of stack frames are checked.
In comparison, native execution checks the size of the stack.
Still, this is good enough to find possible stack overflows.
The limit can be changed with `-max-stack-frames`. The current
default is 8192 frames.
|
|
|
|
--external-calls, updated tests accordingly, and improved documentation on external calls
|
|
|
|
|
|
concrete arguments and files.
* Sample use cases:
* Using an interesting input as a seed, such as a crashing input.
* Analyzing the path condition of a crashing input.
* Also added the test: test/Runtime/POSIX/GenBout.c
|
|
Otherwise optimizations done in klee won't have any effect.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
@llvm.objectsize has now three aguments, so fix the tests accordingly.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Validate non-optimised and optimised variant of added checks.
|
|
Check that only important div instructions are annotated.
Check the optimized case as well: the call to the validating function
might not be part of the code anymore but already inlined - make sure
the instruction still has the metadata attached.
|
|
|
|
|
|
|
|
|
