In subsection "Running regression tests directly with `test.pl`", for
the first `test.pl`, it is not said `regression/test.pl` to clarify the
location of the file.
In subsection "Running regression tests with ctest", build directory was not wrapped by ``. To make
consistent expression with the rest of the document, it was changed from
build to `build/`.
Check which version of doxygen is being used in
./scripts/run_doxygen.sh, and add a sentence to the documentation about
using the correct version.
The warnings produced by doxygen are different for different versions
of doxygen, so it is important, when comparing a list of expected
warnings, to use the right version of doxygen.
Remove the version of the user manual published at
http://cprover.diffblue.com/cbmc-user-manual.html
and link to http://www.cprover.org/cprover-manual/ instead, in order to
make a clearer separation between the _user_ and _developer_
documentation.
There is updated source intended for the user manual, with almost
identical contents to the removed cbmc-user-manual.md, in the
doc/cprover-manual folder.
Add a list of expected warnings from Doxygen, a Python script to
filter out those warnings from the output from Doxygen, and a simple
bash script to run doxygen using this filter.
In some cases, it would be relatively easy to fix the Doxygen
documentation so that we don't get these warnings. However, in other
cases there are bugs in Doxygen where the code and documentation are
perfectly valid, and Doxygen gives an erroneous warning message.
Currently, CI uses another script to filter out warnings related to
lines of code which have not been changed. However, this doesn't work
well because the line number reported for a warning is often not the
line where the problem lies.
The new script should be useful for CI, and also for checking changes
locally before running CI.
As witnessed by the prior commit, errors in the instructions had to be
updated in multiple places. Also removing the Makefile-based build rules
for IPASIR as those would only work for outdated solvers.
Two functional differences:
* you can now link to these sections
* on the website the sections and subsections appear in the hierarchy
and can be viewed on their own
There was already a small amount of information about running the
regression tests in the folder walkthrough, which I've moved to the new
Running Tests section. The folder walkthrough now links to that section.
Also added the `unit/` folder to the folder walkthrough.
johnnonweiler