Ease use of starter-kit for "hello world" type explorations

[jimgrundy]

Suppose I'm playing around with CBMC and starter-kit for perhaps the first time, evaluating it. Probably what I want to do is write and run a kind of "hello-world" type program, maybe, say, find the max of two numbers. In this case I probably haven't got a whole directory structure of source set up. I just want to instantiate the makefile templates, then go in and edit the a source file in that directory and go. Maybe even put my hello-world function in the harness.

But, if I try to avoid giving a source file location for the function I want to prove I get this:

What is the function name? bar
Enter path to source file defining bar: 
Traceback (most recent call last):
  File "/usr/local/bin/cbmc-starter-kit-setup-proof", line 8, in <module>
    sys.exit(main())
  File "/usr/local/Cellar/cbmc-starter-kit/2.4/libexec/lib/python3.8/site-packages/cbmc_starter_kit/setup_proof.py", line 67, in main
    source_file = util.ask_for_source_file(function)
  File "/usr/local/Cellar/cbmc-starter-kit/2.4/libexec/lib/python3.8/site-packages/cbmc_starter_kit/util.py", line 110, in ask_for_source_file
    raise UserWarning(f"Source file '{src}' does not exist")
UserWarning: Source file '/Users/jmgruj/tmp/cbmc/proofs' does not exist

I think I would want a different user experience for people just looking to try out CBMC.

[markrtuttle]

I don't know what the model of the user to use here is. Someone just trying out CBMC without any source code at all is probably going to want to invoke goto-cc and cbmc directly as in the tutorials on little examples. Someone with preexisting source code is probably going to have a directory with source code.

[jimgrundy]

Twice now I have settled down to write a collection of examples to explore CBMC performance issues starting from a blank slate. I've wanted the convenience of the starter-kit's make system and I've kind of had to hack my way past the initial setup expectations.