search

ApproxSymate / klee

KLEE Symbolic Virtual Machine for Numerical Precision Analysis
Other
0 stars 0 forks source link

Implement Loop breaking #12

Closed domainexpert closed 7 years ago

domainexpert commented 7 years ago

Loop breaking is needed as example programs are highly iterative.

domainexpert commented 7 years ago

To compute error expression only for loops for which we have the trip count.

domainexpert commented 7 years ago

@Himeshi We are currently using LLVM 3.4.2, but newer LLVM releases may have stronger and better loop trip count computation mechanisms, including predicated loop trip counts. See the discussions here: http://lists.llvm.org/pipermail/llvm-dev/2017-May/113267.html http://lists.llvm.org/pipermail/llvm-dev/2017-May/113192.html

Predicated loop trip count is not available using opt -analyze -scalar-evolution with LLVM 3.4.2.

domainexpert commented 7 years ago

Resolved via #13 .