| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
... as running a bitcode with a different target triple may result in
unexpected crashes or assertion violations.
|
|
stats when not dumping states
|
|
Only absolute times were displayed, and were marked as %.
Fixes CexCacheTime, ForkTime and ResolveTime columns.
|
|
Increase the size of the buffer to PATH_MAX in create_link as that is the
maximal possible length of fname and check whether output truncation occurred.
Fixes:
tools/klee-replay/file-creator.c: In function 'create_file':
tools/klee-replay/file-creator.c:55:31: warning: '%s' directive output may be truncated writing up to 4095 bytes into a region of size 64 [-Wformat-truncation=]
55 | snprintf(buf, sizeof(buf), "%s.lnk", fname);
| ^~
......
344 | target = tmpname;
| ~~~~~~~
In file included from /usr/include/stdio.h:866,
from tools/klee-replay/file-creator.c:16:
/usr/include/bits/stdio2.h:70:10: note: '__snprintf_chk' output between 5 and 4100 bytes into a destination of size 64
70 | return __builtin___snprintf_chk (__s, __n, __USE_FORTIFY_LEVEL - 1,
| ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
71 | __bos (__s), __fmt, __va_arg_pack ());
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
otherwise, it is hard to tell whether EH support is available or not
|
|
restoring old behavior without EH support
|
|
|
|
CallBase::getCalledValue has been deprecated by getCalledOperand since LLVM 8
and has been removed in LLVM 11
See: https://reviews.llvm.org/D78882
|
|
The same applies to SmallString.
See: llvm/llvm-project@777180a#diff-497ba4c0c527a125d382b51a34f32542
|
|
|
|
|
|
used.
|
|
|
|
Currently, only 32bit vs. 64bit is supported.
|
|
|
|
We implement the Itanium ABI unwinding base-API, and leave the
C++-specific parts to libcxxabi.
Co-authored-by: Lukas Wölfer <lukas.woelfer@rwth-aachen.de>
|
|
* fill missing columns in rows with None
* fill previous rows with None if new column encountered
* error for --to-csv when more than one input directory given
|
|
|
|
klee-zesti takes concrete arguments, files and stdin of the program under tests
converts them to a seed and then runs klee with that seed. This emulates the interface of ZESTI.
|
|
outputting wrong data.
When KLEE crashes, it produces an empty info file, so it is not enough to check for the existence of an info file.
Previously, table columns would mismatch and return data labeled with the wrong directory names.
|
|
|
|
Changes:
- IntrinsicCleaner accepts fshr/fshl as accepted intrinsics
- Executor::executeCall converts fshr/fshl to urem/zext/concat/shift/extract
- Klee/main suppresses warnings about externals that are LLVM reserved
(i.e., begin with "llvm.")
- New test exercises 32 and 7 bit versions including oversize shift values
Test values are based on LLVM's test for fshl/fshr
- Changes that depend on existence of fshr/fshl are guarded by
#if LLVM_VERSION_CODE >= LLVM_VERSION(7, 0)
or
; REQUIRES: geq-llvm-7.0
|
|
appropriate existing directories and a new directory Statistics; a few missing renames.
|
|
tly in lib/Core
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Instructions
Last `Instructions` is not a good identifier to retrieve the correct row.
For the default setup, KLEE will generate two entries with the same last instruction.
One before clean-up and one after clean-up (i.e. if states are terminated on halt).
Using `rowid` will select the last line.
|
|
The number and order of statistics in klee-stats is hard coded.
Moreover, adding new statistics to KLEE lead to crashes.
Rewriting that part of the script generalises and streamlines the process.
List of changes:
* Extend legend: this is used for known columns to provide shorter names
* simplify sqlite handling and make it more robust and reading of data
* select columns based on internal KLEE names
* streamline addition of artificial columns and make it robust
* handle the case if different runs should be compared but not all have the same statistics
* fix calculation of summary row:
- avg of column if column is showing a relative value or avg value
- max of column if column is showing a max value
- sum of column entries, else
|
|
|
|
|
|
|
|
|
|
Providing a list of directories might sometimes not contain the stats file.
Check its existence before trying to access it.
|
|
|
|
|
|
Added units for some of the data and
modified klee-stats source code to provide solver time
as a fraction of walltime along with fork, resolve
and cexcache time.
|
|
Currently, arbitrary *.bc files or archives containing .bc files (.bca or .a) can
be linked using `--link-llvm-lib`. Change documentation of command line argument to make this clear.
This feature is useful to keep avoid linking the bitcode libraries with the application as bitcode file in the first place.
Fix error message in case library could not be loaded
|
|
|
|
|
|
|
|
|
|
|
|
that klee-replay creates a temporary directory for replay
|
|
|
