| Age | Commit message (Collapse) | Author |
|---|
|
runAndGetCexForked())
|
|
|
|
|
|
Fix `-Wmisleading-indentation` warning and also correctly set the `dirty` flag
|
|
`dirty` flag if we remove `llvm.trap` from the module.
|
|
|
|
Don't build KLEE's runtime with any sanitizers.
|
|
remove mimic_stp option and the associated ITE chain construction for variable shift operations
|
|
built with them because KLEE can't handle this.
|
|
* Add unittest to check that the `Assignment` class can evaluate
expressions containing a `NotOptimizedExpr`.
* Fix the `AssignmentTest.FoldNotOptimized` unit test by
teaching the `ExprEvaluator` to fold `NotOptimizedExpr` nodes.
|
|
configure: add option to enable timestamping and disabled it by default
|
|
operators
|
|
The previous change altered .ac files, regenerate the scripts.
Signed-off-by: Jiri Slaby <jslaby@suse.cz>
|
|
It is pain for build systems to see __DATE__ or __TIME__ in sources as
the build is not reproducible. So disable the timestamping by default
and add an option to enable it if somebody is really after it.
Signed-off-by: Jiri Slaby <jslaby@suse.cz>
|
|
Fixed the description of -posix-runtime option
|
|
In the description, --sym-argv and --sym-argvs should have instead been --sym-arg and --sym-args
|
|
Refactoring logging information
|
|
klee_warning, and klee_error
|
|
Extended support for assembler raising
|
|
function) (#455)
|
|
Allow cross checking of solvers
|
|
`-debug-crosscheck-core-solver` as requested by Cristian
|
|
functions.
|
|
with another solver. For example the core solver can be STP and the
cross checking solver can be Z3.
Unfortunately a few fragile tests don't pass when actually using this
option.
|
|
|
|
POSIX runtime. If the check fails, exit with an error. (#457)
|
|
Try to unbreak the TravisCI and Docker builds.
|
|
GTest has moved from googlecode to GitHub so update URL and directory
name used in source archive as appropriate.
|
|
Document -save-all-writes to klee_init_env help message
|
|
|
|
[Klee Web] Link libkleeRuntest library to fix coverage report
|
|
|
|
Improved support for assembler handling.
Providing additional triple information
to raise assembler for supported architectures
only.
Implemented support for raising full assembly
memory fence.
Added initial support for memory fences in Executor.
|
|
Fix to PTree pointer use-after-delete
|
|
|
|
Fix for klee_get_obj_size() crashing on 64-bit, resolves #446
|
|
|
|
Fix to #449 by using sys::StrError(errno) to print error messages.
|
|
|
|
Fix to #445
|
|
|
|
add --exit-on-error-type option
|
|
It allows stopping the execution on some conditions like assertions.
The use is like:
klee -exit-on-error-type=Assert -exit-on-error-type=External file.llvm
This is especially useful in the SV-COMP.
A test to cover the new parameter was added too.
Signed-off-by: Jiri Slaby <jslaby@suse.cz>
|
|
fprintf: convert to klee_warning
|
|
In some Solver sources, some error outputs were missing \n. Instead of
adding a new line to all of them, convert the fprintf's to
klee_warning which adds \n automatically.
ErrorHandling.h had to be included in MetaSMTSolver.cpp to have
klee_warning declared there.
Signed-off-by: Jiri Slaby <jslaby@suse.cz>
|
|
MemoryUsage: handle ill-designed mallinfo
|
|
The mallinfo() interface is ill-designed. It returns 'int' as occupied
memory. This means at most 2G. This causes troubles when capping the
memory to 3G by -max-memory=3000 for example.
We cannot fix the interface, but we can at least extend the space to
4G. So cast those 'int's to 'unsigned int's to avoid sign extension.
Then do the addition on 'size_t' to count on 64bit values (on 64 bit).
Apart from that, the original 'int' + 'int' led to overflow which is
undefined on 'signed int's in C.
Also, when klee is run under valgrind, generic.current_allocated_bytes
from gperftools does not touch the passed pointer and in that case, we
return garbage from GetTotalMallocUsage. So initialize 'value' to 0 to
avoid the problem.
And since GetNumericProperty accepts 'size_t', let's define 'value' as
such. It was 'uint64_t' previously and they differ on 32 bit.
Signed-off-by: Jiri Slaby <jslaby@suse.cz>
|
|
Added test case exposing division by zero failure reported by @kren1 and made division total in STP to fix it.
|
|
|
|
Executor: do not crash on non-sized globals
|
