`goto-as -Qy - -o bla.o` would previously fail with 1) an uninterpreted
option "-Qy" and 2) "Failed to open input source -". As stdin is
properly redirected to a file by goto_cc_cmdlinet, this file should be
used (and -Qy should be ignored).
Changes test.pl to name output *.out files after *.desc instead
of *.class files. Also updates failed-test-printer.pl to work with
those new *.out files and multiple *.desc files.
Only give warnings for namespaces with actual names, in accordance with
ad41375353.
This enables the use of anonymous namespaces without warnings.
Fixes: #932
Pointer dereferencing may yield objects that have meanwhile gone out of scope.
Assigning to them is unnecessary, and performing a merge on those would yield
inconsistent equations (as witnessed by the included regression test).
Filtering out the merge in phi nodes is not easily possible as there are several
cases where it is permissible that only one of the states entering the phi node
has an (L1) object, such as declarations only seen in one branch.
Fixes: #1115
A practical tutorial on getting started with CProver development is
added and linked to from the front page. The tutorial contains an
overview of the codebase and a few preliminary programming exercises,
intended to give would-be CProver contributors an introduction to the
key data structures used throughout the codebase.
This commit introduces a module.md file for several CProver directories.
Each of these is turned into a page under the Modules section in the
generated Doxygen documentation.
The intention is that developers wishing to contribute to one specific
aspect of CProver can get a high-level architectural overview of a
particular directory; the documentation describes the input to and
output from that directory, and introduces the main classes or entry
points.
By way of a "table of contents," the file cbmc/module.md contains a
diagram describing how each of the directories is invoked by CBMC in
order, and the nodes of the diagram hyperlink to the appropriate
documentation. The intention is that developers wishing to contribute to
CBMC as a whole can understand the entire process, from source files to
bug reports and counterexample production.
This documentation is derived from Mark Tuttle's notes on a talk given
by Michael Tautschnig.
Doxygen module groups that did not contain any documentation are removed
from the codebase. There are still a few module groups remaining, which
do contain useful content. This commit declutters the Doxygen Modules
section in preparation for a commit introducing per-directory module
documentation.
* The existing HTML documentation under doc/html-manual has been
converted to Markdown. This was done automatically using Pandoc, plus
some manual work to give identifiers to sections and changing internal
links to point to those sections with \ref.
* The Doxygen front page now contains some content: a link to the
doxygen-ated HTML manual, and a note about the API documentation. The
intention here is that the entire Doxygen site could be hosted
publicly, serving both users of and contributors to CBMC from a single
site.
* The doxyfile is updated to enable these changes.
goto-cc calls objcopy with a native prefix if GCC is being used to link
several object files, and the name of the compiler begins with some
native prefix (like arm-none-eabi-gcc).
Previously, goto-cc would only prepend a native prefix to objcopy if the
linker command had a native prefix. This commit causes goto-cc to work
on codebases that use GCC rather than LD to link, and that use a
cross-compiler with a native-prefixed name.
reuk