about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2020-06-24slightly update ExecutionState, remove holes in structFrank Busse
2020-06-19Added test reported in https://github.com/klee/klee/issues/189 for byval ↵Cristian Cadar
variadic arguments
2020-06-19Renamed Vararg.c to VarArg.c for consistency with the other var arg tests ↵Cristian Cadar
and reformatted comments.
2020-06-19Added test checking for correct alignment of variadic argumentsCristian Cadar
2020-06-19Correctly copy variadic arguments with byval attributeCristian Cadar
2020-06-19Renamed loop index from "i" to "k" in executeCall() so that we can reuse ↵Cristian Cadar
"Instruction *i" declared at the beginning of the function. Reformatted this function.
2020-06-19Added test checking that KLEE correctly handles variadic arguments with the ↵Cristian Cadar
byval attribute
2020-06-17remove cmake warningFrank Busse
* rename SQLITE3 to SQLite3 CMake Warning (dev) at /usr/share/cmake-3.17/Modules/FindPackageHandleStandardArgs.cmake:272 (message): The package name passed to `find_package_handle_standard_args` (SQLITE3) does not match the name of the calling package (SQLite3). This can lead to problems in calling code that expects `find_package` result variables (e.g., `_FOUND`) to follow a certain pattern. Call Stack (most recent call first): cmake/modules/FindSQLite3.cmake:26 (FIND_PACKAGE_HANDLE_STANDARD_ARGS) CMakeLists.txt:430 (find_package) This warning is for project developers. Use -Wno-dev to suppress it.
2020-06-06[Module] Add testcase for inline asm liftingMartin Nowack
2020-06-06[Module] Disable lifting for inline asm resembling memory fences with return ↵Martin Nowack
values Inline asm used for memory barriers might use their operands and propagate them as return value. This is currently not supported. Tighten check for this condition and do not to lift those inline asm instructions. Fixes #1252
2020-05-01Add test case from #1257 to reproduce behaviourMartin Nowack
2020-05-01[Solver:STP] Fix handling of array namesMartin Nowack
Array names used for STP queries used to be restricted to 32 characters, with the last characters replaced by a unique number. Similarly, an array is made unique by `klee_make_symbolic`. Unfortunately, both combined can lead to the generation of the same STP array name for different arrays. This leads to wrong queries with invalid results. This is more likely be triggered with longer names for `klee_make_symbolic` Fixes #1257
2020-04-30docker: install KLEE headers in system include pathXiao Liang
Co-authored with @MartinNowack
2020-04-30Moved header files that were placed directly in include/klee/ into ↵Cristian Cadar
appropriate existing directories and a new directory Statistics; a few missing renames.
2020-04-30Removed include/klee/util and moved header files to appropriate placesCristian Cadar
2020-04-30Created include/klee/Core directory and moved appropriate files direc\Cristian Cadar
tly in lib/Core
2020-04-30Move header files from lib/Expr to include/klee/Expr to eliminate includes ↵Cristian Cadar
using "../"
2020-04-30Removed the Internal directory from include/kleeCristian Cadar
2020-04-20Consistently define variable using notation VAR=value; fixed comment placementCristian Cadar
2020-04-20Named jobs in Travis CI for better visualization of resultsCristian Cadar
2020-04-09[posix-runtime] Improve model to handle full-path symbolic filesTimotej Kapus
2020-04-09[posix-runtime] Add test for full path consistency for symbolic filesTimotej Kapus
2020-04-08readStringAtAddress: support pointer into objectsMarek Chalupa
The code assumed that the passed pointer points at the beginning of the object. Remove this assumption and support any (constant) pointer. The string is read util either the end of the object is hit (in which case a warning is issued as the string was not zero terminated) or until the terminating zero is found.
2020-04-08test: add a new test for readStringAtAddressMarek Chalupa
Read strings from different parts of objects.
2020-04-08readStringAtAddress: use stringstream to obtain the stringMarek Chalupa
The code is simpler and more in the spirit of C++.
2020-04-08stats: rename QueriesConstructs to QueryConstructsFrank Busse
2020-04-08Statistic: slightly modernise class definitionFrank Busse
2020-04-08stats: remove queryConstructTime (unused)Frank Busse
2020-04-07Add unit test for Z3Solver::getConstraintLogDaniel Grumberg
2020-04-05Run "pkg update -f" before installing dependencies on FreeBSDCristian Cadar
2020-03-31Don't search for CryptoMiniSAT when configuring STPCristian Cadar
2020-03-31Fixed some messages, particularly Klee -> KLEECristian Cadar
2020-03-27Ensure that temp_builder is used when adding constant array value assertion ↵Daniel Grumberg
constraints
2020-03-22StatsTracker: remove NumObjects, fix assignment of and always write ↵Frank Busse
ArrayHashTime * fix binding order for assignments when KLEE_ARRAY_DEBUG enabled * always write ArrayHashTime column to run.stats, assign -1 when KLEE_ARRAY_DEBUG disabled * remove unused NumObjects column from run.stats * remove NumObjects panel from Grafana
2020-03-22[posix-runtime] Simple GET/SET_LK modelTimotej Kapus
2020-03-19Additional test for dealing with vector instructionsCristian Cadar
2020-03-18Added another `ScalarizerLegacyPass` run to remove vectorized code ↵Frederic Kehrein
introduced during the optimization step
2020-03-17Fixed compiler warning when printing variable of type off_tCristian Cadar
2020-03-17stat64 is deprecated on macOS; use stat insteadCristian Cadar
2020-03-10Use -snap VMs on Cirrus for FreeBSDCristian Cadar
2020-03-06Updating KLEE's version post-releaseCristian Cadar
2020-03-03Release notes for 2.1 v2.1 2.1.xCristian Cadar
2020-03-03Set version to 2.1Cristian Cadar
2020-03-02fix lit.cfg: numerical comparison of LLVM version numbersJulian Büning
2020-03-02travis: add LLVM 10.0Julian Büning
2020-03-02test/lit.cfg: add LLVM 10.0Julian Büning
2020-03-02stats: enforce table creationFrank Busse
2020-03-01[klee-stats] Grafana: Limit number of entries to query for column namesMartin Nowack
2020-03-01[klee-stats] Use the last row inserted instead of the row with highest ↵Martin Nowack
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.
2020-03-01[klee-stats] Refactor preparing and printing the tableMartin Nowack
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
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-07-15 22:55:42 +0000