Folder goto-harness

goto-harness generates a proof harness for a function under test. It constructs functions that set up an appropriate environment before calling function. This is most useful when trying to analyze an isolated unit of a program.