about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
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
2020-03-01[klee-stats] Check for existence of stats file for Grafana as wellMartin Nowack
2020-03-01[klee-stats] Do not crash if tabulate is not installed but requestedMartin Nowack
2020-03-01[klee-stats] Refactor writing table into own functionMartin Nowack
2020-03-01[klee-stats] Refactor CSV printout in own functionMartin Nowack
2020-03-01[klee-stats] Check if stats file exist before trying to open itMartin Nowack
Providing a list of directories might sometimes not contain the stats file. Check its existence before trying to access it.
2020-02-24Add leading zeros to genboutTimotej Kapus
2020-02-24fix p-llvm.inc: invocation for monorepo directory layoutJulian Büning
2020-02-24find_llvm.cmake: enable parsing for git versionJulian Büning
2020-02-23Use FreeBSD 11.3-STABLE instead of EoLed 11.2.Gleb Popov
2020-02-23Workaround `pkg` breakage on FreeBSD CI.Gleb Popov
2020-02-19Use `ref<>` for MemoryObject handlingMartin Nowack
This uses the `ref<>`-based memory handling of MemoryObjects. This makes it explicit that references are held in: - ExecutionState::symbolics - ObjectState
2020-02-19Use `ref<>` for UpdateNodeMartin Nowack
Remove additional reference counting as part of UpdateNodeList and UpdateNode. Simplifies code.
2020-02-19Clean-up header filesMartin Nowack
* Replace c header with c++ header * remove unneeded header file
2020-02-19Add move assignment operator and move construct for `ref` class.Martin Nowack
2020-02-19Add `ReferenceCounter` struct utilized by ref<>Martin Nowack
Using KLEE's `ref<>` shared ptr requires the referenced object to contain a reference counter to be added and initialised to 0 as part of the constructor. To support better reuse of the `ref<>` ptr add a `ReferenceCounter` struct. Just adding this struct to a new class/struct as member enables reference counting with `ref<>` - no additional counter management needed.
2020-02-19Fix ptr reference invalidation if last reference gets freed before new ↵Martin Nowack
reference assigned.
2020-02-13Use call-by-reference for hash-function invocationMartin Nowack
2020-02-13Replace old TR1 implementations of unordered_map/set with std::* versionsMartin Nowack
TR1 implementation got replaced by the std::* equivalents with C++11. Start to use the standard versions instead of the old ones.
2020-02-13Use a newer Ubuntu 18.04 from the year 2020 to build KLEE DockerimageMartin Nowack
2020-02-13Use a newer Ubuntu 18.04 from the year 2020 to build KLEEMartin Nowack