KLEEDynamicTesting
Author: Jun Yan Ma (ma23@purdue.edu)
Project Description: ProjectDescription.pdf (http://www.cs.purdue.edu/homes/kim1051/cs490/proj3/description.html)
Part 1.1
Set of paths covered by KLEE with symbolic variable 'a': /part1/p1a.c
Set of paths covered by KLEE with symbolic variable 'b': /part1/p1b.c
Set of paths covered by KLEE with symbolic variable 'c': /part1/p1c.c
Set of paths covered by KLEE with all symbolic variables including infeasible path: /part1/p1.c
Part 1.2
Directory containing abort.err.file, .ktest file and content of symbolic file in the test case that causes a bug: /part1/gnupg-buggy/test_case_with_bug
Script to initialize coverage, run g10/gpg and generate coverage report: part1/gnupg-buggy/run-test-case-script.rb
Directory containing overall coverage report in HTML is not submitted as it is large in size. Instead overall coverage rate is shown below. A screenshot is also provided at: /part1/gnupg-buggy/CoverageReport.png
Report: Hit Total Coverage Lines: 1473 23915 6.2% Functions: 106 1176 9.0%
Directory containing all the test cases generated by KLEE: /part1/gnupg-buggy/klee-out-0
Part 2.1
Modified code using singly linked list to track my_malloc and my_free: /part2/malloc.c and /part2/malloc.h
Running KLEE using one symbolic file of size 6 bytes and marking option and newKey as symbolic variables, we can find a test case that causes a memory leak. Running KLEE using symbolic file of size 7 bytes yield same reults. Directory containing abort.err.file and .ktest file: /part2/test_case_with_memory_leak.
Part 2.2
One of KLEE's limitations is that KLEE cannot handle symbolic floating points. As a result, I have modified p1.c from part1, using float in place of int. Running KLEE generates only 1 test case. KLEE did not manage to cover all feasible paths. Directory containing modified p1.c: /part2/cannot_cover_all_feasible_paths