Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
C Ruby Shell
branch: master

Fetching latest commit…

Cannot retrieve the latest commit at this time

Failed to load latest commit information.
part1
part2
ProjectDescription.pdf
README.md

README.md

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

Something went wrong with that request. Please try again.