Merge pull request #329 from thk123/patch-1

Make the compiling steps a little more explicit

Author: martin-cs

gnat2goto/COMPILING.md

@@ -12,7 +12,7 @@ Note: you will *not* be able to build using the debian/ubuntu gnat and gprbuild,
 For **Debian**, install the following debian packages:
   - build-essential
 
-For **Mac OSX**, you will need the XCode Command Line tools, which require XCode itself and then a 
+For **Mac OSX**, you will need the XCode Command Line tools, which require XCode itself and then a
 ```
 xcode-select --install
 ```
@@ -27,7 +27,7 @@ select your platform and then 2016 (in that order). Download
   * gnatcoll-gpl-2016
 
 
-The following assumes you installed GNAT GPL 2016 into /opt/gnat using the doinstall script.
+Install the GNAT GPL Ada 2016 using the `doinstall` script inside the zip. The following instructions assume you picked `/opt/gnat` as the install destination.
 
 Install GNATCOLL GPL 2016:
   - `$ export PATH=/opt/gnat/bin:${PATH}`
@@ -38,7 +38,7 @@ Install GNATCOLL GPL 2016:
 
 # Building gnat2goto
 
-Assuming that you've built the dependencies as per the above instructions
+Assuming that you've built the dependencies as per the above instructions, do the following from within `gnat2goto`.
 
   - `$ export PATH=/opt/gnat/bin:${PATH}`
   - `$ export GPR_PROJECT_PATH=/opt/gnat/lib/gnat`
@@ -48,6 +48,8 @@ This should build into install/bin. You can test if it works by calling:
 
 ` $ install/bin/gnat2goto examples/foo.adb`
 
+If it has worked, you should have two files: `foo.ali` and `foo.json_symtab`.
+
 # Building and running gnat2goto unit tests
 
 gnat2goto includes a selection of unit tests. These are built as a seperate
@@ -66,7 +68,7 @@ In addition to the unit tests, gnat2goto also includes end-to-end regression
 tests. These tests aim to test the full pipeline from Ada source code input
 through to final analysis by CBMC.
 
-Instructions for running the regression test suite are described in [testsuite/gnat2goto/README.md](testsuite/gnat2goto/README.md)
+Instructions for running the regression test suite are described in [testsuite/gnat2goto/README.md](../testsuite/gnat2goto/README.md)
 
 # Running and updating missing features tests
 
@@ -93,7 +95,7 @@ one file per project. Simply copy the '<project>-summary.txt' file from
 
 # Updating the CBMC submodule
 
-As described in [testsuite/gnat2goto/README.md](testsuite/gnat2goto/README.md)
+As described in [testsuite/gnat2goto/README.md](../testsuite/gnat2goto/README.md)
 gnat2goto includes a GIT submodule for CBMC. In most cases this should not need
 changing, but if you are developing gnat2goto features or fixes that require a
 different version of CBMC then you will need to update the CBMC submodule

testsuite/gnat2goto/README.md

@@ -89,6 +89,34 @@ Requirements
 
 Running tests
 -------------
+
+Ensure that both gnat2goto and cbmc are on the path:
+
+```
+export PATH=${PATH}:/path/to/gnat2goto/lib/cbmc/path/to/cbmc:/path/to/gnat2goto/gnat2goto/install
+```
+
+_Note for `make` users `/path/to/cbmc` will point to `lib/cbmc/src/cbmc`. For
+`cmake` it will be something like `lib/cbmc/build/bin`._
+
+From within [gnat2goto/testsuite/gnat2goto](.) run:
+
+```
+$ ./testsuite.py -j 4 --timeout 60 --enable-color
+```
+where ```-j``` sets the number of tests to run in parallel (default is 1).
+
+`--timeout` will limit how long a test can run
+
+`--enable-color` will enable color printing in the output.
+
+This will output which tests pass and fail. If a test fails, you can inspect the output
+inside `out`. Each test will produce a file called `test_name.diff` which contains a git
+diff between the expected an actual output.
+
+Alternatively, `--diffs` can be turned on to see the difference between the expected
+and actual outputs for all of `XFAIL`, `FAIL`, or `UPASS` results.
+
 For the gnat2goto test suite each test subdirectory has a file test.py.
   In this file is a call to a subprogram prove.  This subprogram has an
   optional parameter, debug <prove (debug=True>),
@@ -98,6 +126,12 @@ For the gnat2goto test suite each test subdirectory has a file test.py.
   of course this will cause a DIFF to be reported between actual and
   expected output.  By default debug=False.
 
+Updating Expected Results
+-------------------------
+
+Sometimes the tests will need to be updated for the new behaviour. This can be done
+using [`./update-expected-outputs`](update-expected-outputs).
+
 WARNING running ./update-expected outputs will replace all test.out
 	(expected result) files with the actual results.
 	A summary of the diffs between expected and actual results,
@@ -108,11 +142,6 @@ WARNING running ./update-expected outputs will replace all test.out
 	revert all the changed test.out files, i.e.,
 	git checkout -- tests/<test-dir>/test.out for each changed test.out).
 
-* To run test suite:
-```
-$ ./testsuite.py -j 4
-```
-where ```-j``` sets the number of tests to run in parallel (default is 1).
 
 * then, optionally