Age | Commit message (Collapse) | Author | |
---|---|---|---|
2020-04-30 | Removed the Internal directory from include/klee | Cristian Cadar | |
2020-04-20 | Consistently define variable using notation VAR=value; fixed comment placement | Cristian Cadar | |
2020-04-20 | Named jobs in Travis CI for better visualization of results | Cristian Cadar | |
2020-04-09 | [posix-runtime] Improve model to handle full-path symbolic files | Timotej Kapus | |
2020-04-09 | [posix-runtime] Add test for full path consistency for symbolic files | Timotej Kapus | |
2020-04-08 | readStringAtAddress: support pointer into objects | Marek 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-08 | test: add a new test for readStringAtAddress | Marek Chalupa | |
Read strings from different parts of objects. | |||
2020-04-08 | readStringAtAddress: use stringstream to obtain the string | Marek Chalupa | |
The code is simpler and more in the spirit of C++. | |||
2020-04-08 | stats: rename QueriesConstructs to QueryConstructs | Frank Busse | |
2020-04-08 | Statistic: slightly modernise class definition | Frank Busse | |
2020-04-08 | stats: remove queryConstructTime (unused) | Frank Busse | |
2020-04-07 | Add unit test for Z3Solver::getConstraintLog | Daniel Grumberg | |
2020-04-05 | Run "pkg update -f" before installing dependencies on FreeBSD | Cristian Cadar | |
2020-03-31 | Don't search for CryptoMiniSAT when configuring STP | Cristian Cadar | |
2020-03-31 | Fixed some messages, particularly Klee -> KLEE | Cristian Cadar | |
2020-03-27 | Ensure that temp_builder is used when adding constant array value assertion ↵ | Daniel Grumberg | |
constraints | |||
2020-03-22 | StatsTracker: 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 model | Timotej Kapus | |
2020-03-19 | Additional test for dealing with vector instructions | Cristian Cadar | |
2020-03-18 | Added another `ScalarizerLegacyPass` run to remove vectorized code ↵ | Frederic Kehrein | |
introduced during the optimization step | |||
2020-03-17 | Fixed compiler warning when printing variable of type off_t | Cristian Cadar | |
2020-03-17 | stat64 is deprecated on macOS; use stat instead | Cristian Cadar | |
2020-03-10 | Use -snap VMs on Cirrus for FreeBSD | Cristian Cadar | |
2020-03-06 | Updating KLEE's version post-release | Cristian Cadar | |
2020-03-03 | Release notes for 2.1 v2.1 2.1.x | Cristian Cadar | |
2020-03-03 | Set version to 2.1 | Cristian Cadar | |
2020-03-02 | fix lit.cfg: numerical comparison of LLVM version numbers | Julian Büning | |
2020-03-02 | travis: add LLVM 10.0 | Julian Büning | |
2020-03-02 | test/lit.cfg: add LLVM 10.0 | Julian Büning | |
2020-03-02 | stats: enforce table creation | Frank Busse | |
2020-03-01 | [klee-stats] Grafana: Limit number of entries to query for column names | Martin 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 table | Martin 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 well | Martin Nowack | |
2020-03-01 | [klee-stats] Do not crash if tabulate is not installed but requested | Martin Nowack | |
2020-03-01 | [klee-stats] Refactor writing table into own function | Martin Nowack | |
2020-03-01 | [klee-stats] Refactor CSV printout in own function | Martin Nowack | |
2020-03-01 | [klee-stats] Check if stats file exist before trying to open it | Martin Nowack | |
Providing a list of directories might sometimes not contain the stats file. Check its existence before trying to access it. | |||
2020-02-24 | Add leading zeros to genbout | Timotej Kapus | |
2020-02-24 | fix p-llvm.inc: invocation for monorepo directory layout | Julian Büning | |
2020-02-24 | find_llvm.cmake: enable parsing for git version | Julian Büning | |
2020-02-23 | Use FreeBSD 11.3-STABLE instead of EoLed 11.2. | Gleb Popov | |
2020-02-23 | Workaround `pkg` breakage on FreeBSD CI. | Gleb Popov | |
2020-02-19 | Use `ref<>` for MemoryObject handling | Martin Nowack | |
This uses the `ref<>`-based memory handling of MemoryObjects. This makes it explicit that references are held in: - ExecutionState::symbolics - ObjectState | |||
2020-02-19 | Use `ref<>` for UpdateNode | Martin Nowack | |
Remove additional reference counting as part of UpdateNodeList and UpdateNode. Simplifies code. | |||
2020-02-19 | Clean-up header files | Martin Nowack | |
* Replace c header with c++ header * remove unneeded header file | |||
2020-02-19 | Add move assignment operator and move construct for `ref` class. | Martin Nowack | |
2020-02-19 | Add `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-19 | Fix ptr reference invalidation if last reference gets freed before new ↵ | Martin Nowack | |
reference assigned. | |||
2020-02-13 | Use call-by-reference for hash-function invocation | Martin Nowack | |