tracer-x TracerX issues

tracer-x / TracerX

TracerX Symbolic Virtual Machine

https://tracer-x.github.io/

Other

31 stars 11 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Added actual check for existential variable in the lhs of equalities …

#312 domainexpert closed 7 years ago
1
Over-subsumption with queens.c

#311 domainexpert closed 7 years ago
1
Fix to assertion failure crash with statemate.c

#310 domainexpert closed 7 years ago
0
Corrected the logic in SubsumptionTableEntry::makeConstraint()

#309 domainexpert closed 7 years ago
0
Simplifications to memory bounds computation

#308 domainexpert closed 7 years ago
0
Correction to the construction of existentially-quantified formula for Z3

#307 domainexpert closed 7 years ago
0
Added -subsumed-test option to generate tests from subsumed paths

#306 domainexpert closed 7 years ago
0
Incremental building of state for subsumption check

#305 domainexpert closed 6 years ago
1
Subsumption interpolation accuracy correction

#304 domainexpert closed 7 years ago
0
Resolution to Missing Error Report

#303 domainexpert closed 7 years ago
1
Added simplification of and expression in SubsumptionTableEntry::subs…

#302 domainexpert closed 7 years ago
0
Use pointer lower bound for memory violation interpolation

#301 domainexpert closed 4 years ago
0
Resolution to masked error problem

#300 domainexpert closed 7 years ago
3
Handling of switch instruction

#299 domainexpert closed 7 years ago
1
Differentiate memory bound from left and right subtree

#298 domainexpert closed 7 years ago
3
Compression of dependency paths

#297 domainexpert closed 7 years ago
0
Prevent computing pointer bound when better bound already computed

#296 domainexpert closed 7 years ago
1
Skipping entries with depth larger than the current store

#295 domainexpert closed 7 years ago
0
Implementation of non-storing of unused constraint on path condition

#294 domainexpert closed 7 years ago
0
Over-marking of path condition

#293 domainexpert closed 7 years ago
1
Remove quantification in case the body of a quantified query expression has no constraint with both bound and non-bound variables

#292 domainexpert closed 7 years ago
0
WP: Feasible false branch not captured

#291 rasoolmaghareh closed 7 years ago
2
WP: Instructions not marked correctly in reverse traversal

#290 rasoolmaghareh closed 7 years ago
2
More precise subsumption check

#289 domainexpert closed 7 years ago
0
Reduction in subsumption count

#288 domainexpert closed 7 years ago
0
Timed out basic benchmarks

#287 domainexpert closed 7 years ago
1
Possibility of removing Dependency::valuesMap by using Cell

#286 domainexpert closed 4 years ago
0
Reimplementation of memory domination

#285 domainexpert closed 7 years ago
2
Reimplementation of symbolic heap

#284 domainexpert closed 7 years ago
1
WIP: Weakest Precondition

#283 rasoolmaghareh closed 5 years ago
9
Solver simplification fix

#282 domainexpert closed 7 years ago
0
WIP: Reimplementation of symbolic heap

#281 domainexpert closed 7 years ago
3
Give up on subsumption check if existential quantification exists in the query

#280 domainexpert closed 4 years ago
0
Trivial fixes

#279 domainexpert closed 7 years ago
1
Reimplementation of symbolic heap

#278 domainexpert closed 7 years ago
1
Adding no-compression command line argument

#277 rasoolmaghareh closed 7 years ago
13
Added TxTree::blockCount to count all Basic Blocks including merged BBs

#276 rasoolmaghareh closed 7 years ago
6
Count-nodes missing some nodes

#275 rasoolmaghareh closed 7 years ago
1
WIP: Weakest Precondition

#274 rasoolmaghareh closed 7 years ago
0
Corrected value print in TxInterpolantValue::print

#273 domainexpert closed 7 years ago
0
WIP: Witness

#272 rasoolmaghareh closed 7 years ago
0
More efficient unsat core interpolation

#271 domainexpert closed 4 years ago
0
Unsat core for FastCexSolver::propogateValues needs to be implemented

#270 domainexpert closed 4 years ago
0
Corrected comment in TxPrintUtil.h

#269 domainexpert closed 7 years ago
0
Fix to over-subsumption

#268 domainexpert closed 7 years ago
10
Improvements on the tree DOT output

#267 domainexpert closed 7 years ago
0
Correctly hande the case when memory bound check fails under Tracer-X

#266 domainexpert closed 7 years ago
2
Memory domination not working

#265 domainexpert closed 7 years ago
3
Fix to assertion failure due to Tracer-X conservative validity check

#264 domainexpert closed 7 years ago
2
Correction to the semantics of getelementptr with negative index

#263 domainexpert closed 7 years ago
0

Previous Next