Squashed 'cbmc/' changes from 5d3ea03..4f5e148

4f5e148 Merge pull request diffblue#2713 from thk123/dump/expr2c-configuration
01b7418 Merge pull request diffblue#2710 from thomasspriggs/tas/struct_component
b763877 Merge pull request diffblue#2737 from diffblue/remove-appveyor
9c3fd45 Add AWS CodeBuild badges
4261fd8 Remove appveyor badge
fe23db7 Remove appveyor.yml
21857a7 Add support for getting components by name to `struct_exprt`
05993f4 Merge pull request diffblue#2727 from tautschnig/fptr-debug
0ecd008 Merge pull request diffblue#2701 from antlechner/antonia/enum-constants
159bf15 Merge pull request diffblue#2205 from diffblue/rename_symbol_type
5ca6cd2 Restrict new clinit_wrapper calls to enum types
6e04213 Reformatting the structs to aid readability
0cfacb8 Add type2c conversion for specifying a type name
c3fef70 Add a clean configuration for expr2c
3a40db1 Make expr2ct configurable in a number of ways
097cf71 Merge pull request diffblue#2731 from diffblue/increase-version
170c1ea Merge pull request diffblue#2730 from diffblue/parent-child-invariant
c9e46ae Temporarily remove new UNREACHABLE statements
03e3877 Add tests for nondet initialization of enums
3e32140 CI lazy methods: load clinit for all param types
5542c54 Move nondet enum initialization to new function
6ecf4f9 Nondet-init enums by assigning them to a constant
6c84caa Refactor logic for generating a nondet int
07d1e44 Always run clinit_wrapper before nondet object init
3be826f Add some documentation to java_object_factory
5e80310 add invariant on parent-child class relationship
2cf1931 Merge pull request diffblue#2661 from jeannielynnmoulton/jeannie/JavaMethodType
c6acc9c increased version number in preparation for release 5.10
0ee4178 Merge pull request diffblue#2729 from tautschnig/add-sub-conflict
f5aff56 Merge pull request diffblue#2705 from danpoe/feature/replace-function-calls
89048e6 Function-pointer remvoval: print human-friendly debug messages
1fc3118 Use pointer difference type when adding to pointer
072b592 Merge pull request diffblue#2726 from tautschnig/java-loc
4dca215 Goto program should not use java_method_typet
273fff4 Add can_cast_type and precondition.
6cb7e5d Reinstate require_code and add require_java_method
78f7cb7 Refactor constructors for java_method_typet
6cefc61 Unit tests conversion from code_typet to java_method_typet
c3b8b5a Update tag in to_java_method_type
972315a Update docs on java_method_typet constructor
211931c Add tag for java_method_type
551df9c Update unit tests to use java_method_typet
da18c9f Change variables named code_type to method_type
f1bd41e Change code_typet to java_method_typet in jbmc
be3c4c6 Merge pull request diffblue#2430 from tautschnig/vs-function-id
03fa885 Replace function calls
c4d79ab Java string preprocessing: use provided source location
fb0c552 Java string preprocessing: use and document parameter function_id
c31edca Merge pull request diffblue#2725 from tautschnig/replace-symbolt-code-type
2c1fc06 Merge pull request diffblue#2721 from tautschnig/replace_symbol-cleanup2
8211a78 Merge pull request diffblue#2722 from tautschnig/cleanup-valuest
30bc071 Add "// empty last line" to options list in goto_instrument_parse_options.h
8c8801c List source files in goto-programs/Makefile in lexicographic order
40d28ae replace_symbolt: report replacements in code_typet::return_type
4b9df3b Revert "Ignore return value"
e39ea2e Merge pull request diffblue#2683 from karkhaz/kk-continue-unsafe
424ab4f --stop-on-fail now stops on failed path
545bff8 Add clear() to path exploration worklist
95d8d0f Generalise option setting from strategy unit tests
e85fb77 Cleanup constant_propagator_domaint::valuest
18d08bf Merge pull request diffblue#2719 from tautschnig/quiet-unit-tests
30d557a Constant propagation: Check type consistency before adding to replacement map
a5ce621 Make unit tests quiet
61b3086 Merge pull request diffblue#2468 from tautschnig/vs-names
7bfd36b Merge pull request diffblue#2714 from diffblue/msvc-asm
3785941 Remove names of unused parameters
af79cb9 add support for Visual Studio style inline assembler
254b4d4 Merge pull request diffblue#2642 from diffblue/remove_asm_fix
26009a3 remove_asm now guarantees that functions called exist
9c10f38 Merge pull request diffblue#2716 from tautschnig/fix-buildspec
c3b2beb Merge pull request diffblue#2635 from qaphla/move_is_lvalue
e247a29 CodeBuild: Remove empty artifact stanza
756018d Merge pull request diffblue#2709 from owen-jones-diffblue/doc/how-to-run-tests
bba5dea Merge pull request diffblue#2699 from diffblue/goto-cc-clang
355fbd2 avoid assert()
6178908 bump goto binary version
f93deec type symbols now use ID_symbol_type
22b755a Merge pull request diffblue#2711 from diffblue/mode-gcc-asm-functions
cf75535 Merge pull request diffblue#2702 from owen-jones-diffblue/doc/minor-fixes-to-cprover-developer-documentation
5c06786 set mode for functions added by remove_asm
ef53b65 Update description of regression test framework
312ca1d Add section to documentation about running tests
d7ddf59 Merge pull request diffblue#2700 from romainbrenguier/clean-up/side-effect-location
119e88b Pass location around for nondet initialization
50660db Specify source location for nondet expressions
d1f2ad9 Replace -> with →
e448db6 Merge pull request diffblue#2708 from owen-jones-diffblue/coding-standard-class-comments
519370d State that identifiers should be good
30d29b9 Replace unicode arrows → with ascii ones ->
611374f Document classes and member variables unless obvious
adb7ef0 Minor fixes to documentation outline
fd4f563 Add side_effect_exprt constructor with location
98657d8 Merge pull request diffblue#2668 from diffblue/expose_remove_preconditions
6a36fa4 Merge pull request diffblue#2615 from owen-jones-diffblue/doc/cbmc-developer-guide
61a8c30 Merge pull request diffblue#2666 from NlightNFotis/invariant_changes
c0bcce7 use clang as native compiler for goto-clang
1f19e23 goto-cc: use result of our native compiler detection
d9d9e2a Merge pull request diffblue#2692 from diffblue/follow-tags
f94d5e2 follow union, struct and enum tags
99e33bd fix typo in comments for struct_tag_typet
1f53246 expose remove_preconditions
f212505 Avoids using expr.op0 when type is known
7b36ca2 Moves is_lvalue to expr_util.c
4782b48 Fix invariant regression tests
efb1c40 Refactor invariant_failedt definition.
515f050 Pass the condition to the invariant_failedt constructor.
bf6dd9e Added extra use-case hints to the already present invariant definitions.
612b4f8 Address review comments
7233f92 Rearrange everything into separate pages
1cb3cdd Move other tools into a separate file
82eefb7 Fix links between files
d9e690b Move folder walkthrough to a separate file
2939db4 Address review comments
8d5cbcb Create CBMC developer guide documentation

git-subtree-dir: cbmc
git-subtree-split: 4f5e148

Author: Owen Jones

CODING_STANDARD.md

@@ -59,12 +59,13 @@ Formatting is enforced using clang-format. For more information about this, see
   ```
   Note that the `\file` tag must be immediately followed by a newline in order
   for Doxygen to relate the comment to the current file.
-- Each function should be preceded by a Doxygen comment describing that
-  function. The format should match the [LLVM
+- Each class, member variable and function should be preceded by a Doxygen
+  comment describing it when it is not immediately obvious what it does. The
+  format should match the [LLVM
   guidelines](http://llvm.org/docs/CodingStandards.html#doxygen-use-in-documentation-comments),
-  with one extension: `\param` and `\return` comments longer than a single line
-  should have subsequent lines indented by two spaces, so that the tags stand
-  out. An example:
+  with one extension: for functions, `\param` and `\return` comments longer than
+  a single line should have subsequent lines indented by two spaces, so that the
+  tags stand out. An example:
   ```c++
   /// This sentence, until the first dot followed by whitespace, becomes
   /// the brief description. More detailed text follows. Feel free to
@@ -93,6 +94,7 @@ Formatting is enforced using clang-format. For more information about this, see
 - Use #ifdef DEBUG to guard debug code
 
 # Naming
+- Identifiers should make clear the purpose of the thing they are naming. 
 - Identifiers may use the characters `[a-z0-9_]` and should start with a
   lower-case letter (parameters in constructors may start with `_`).
 - Omit names of parameters or exception objects when they are not used. If

README.md

@@ -1,4 +1,6 @@
-[![Build Status][travis_img]][travis] [![Build Status][appveyor_img]][appveyor]
+[![Build Status][travis_img]][travis]
+![Build Status][codebuild_img]
+![Build Status][codebuild_windows_img]
 [![Build Status][coverity_img]][coverity]
 
 [CProver Wiki](http://www.cprover.org/wiki)
@@ -49,7 +51,7 @@ License
 
 [travis]: https://travis-ci.org/diffblue/cbmc
 [travis_img]: https://travis-ci.org/diffblue/cbmc.svg?branch=master
-[appveyor]: https://ci.appveyor.com/project/diffblue/cbmc/
-[appveyor_img]: https://ci.appveyor.com/api/projects/status/github/diffblue/cbmc?svg=true&branch=master
+[codebuild_img]: https://codebuild.us-east-1.amazonaws.com/badges?uuid=eyJlbmNyeXB0ZWREYXRhIjoieVl4UDBKaVU2NEZIeE9GKzhMVWJUQ1RORXRZeGFEdm9LZnhvbWt4Q3oxb29uOTdWZDhZUkUvK2Z0eTBndU5pWkcyUXFZb1pDRVpBNXVob3R0R2tYZkdFPSIsIml2UGFyYW1ldGVyU3BlYyI6IkZ0TzR2a21XbHFkWnlYMkwiLCJtYXRlcmlhbFNldFNlcmlhbCI6MX0%3D&branch=develop
+[codebuild_windows_img]: https://codebuild.us-east-1.amazonaws.com/badges?uuid=eyJlbmNyeXB0ZWREYXRhIjoiTFQ4Q0lCSEc1Rk5NcmlzaFZDdU44Vk8zY0c1VCtIVWMwWnJMRitmVFI5bE94Q3dhekVPMWRobFU2Q0xTTlpDSWZUQ3J1eksrWW1rSll1OExXdll2bExZPSIsIml2UGFyYW1ldGVyU3BlYyI6InpqcloyaEdxbjBiQUtvNysiLCJtYXRlcmlhbFNldFNlcmlhbCI6MX0%3D&branch=develop
 [coverity]: https://scan.coverity.com/projects/diffblue-cbmc
 [coverity_img]: https://scan.coverity.com/projects/13552/badge.svg

appveyor.yml

@@ -80,9 +80,6 @@ phases:
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
         cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C jbmc/unit test BUILD_ENV=MSVC" '
 
-artifacts:
-  files:
-
 cache:
   paths:
     - 'c:\clcache\**\*'

buildspec-windows.yml

@@ -27,8 +27,6 @@ phases:
       - make -C jbmc/unit test
       - make -C jbmc/regression test
       - echo Build completed on `date`
-artifacts:
-  files:
 cache:
   paths:
     - '/var/cache/apt/**/*'

buildspec.yml

@@ -0,0 +1,32 @@
+\ingroup module_hidden 
+\page background-concepts Background Concepts
+
+\author Martin Brain, Peter Schrammel
+
+# Representations #
+
+## AST: types, globals, variables, functions, code blocks, language primitives, assignments, expressions, variables ##
+
+To be documented.
+
+## CFG ##
+
+To be documented.
+
+## SSA ##
+
+To be documented.
+
+# Analysis techniques #
+
+## Bounded model checking ##
+
+To be documented (can copy from the CBMC manual).
+
+## SAT and SMT ##
+
+To be documented.
+
+## Static analysis ##
+
+To be documented.

doc/architectural/background-concepts.md

@@ -0,0 +1,8 @@
+\ingroup module_hidden 
+\page bmct-class Bmct class
+
+\author
+
+## equation ##
+
+To be documented.

doc/architectural/bmct-class.md

@@ -0,0 +1,94 @@
+\ingroup module_hidden 
+\page cbmc-architecture CBMC Architecture
+
+\author Martin Brain, Peter Schrammel
+
+This section provides a graphical overview of how CBMC fits together.
+CBMC takes C code or a goto-binary as input and tries to emit traces
+of executions that lead to crashes or undefined behaviour. The diagram
+below shows the intermediate steps in this process.
+
+\dot
+digraph G {
+
+  rankdir="TB";
+  node [shape=box, fontcolor=blue];
+
+  subgraph top {
+    rank=same;
+    1 -> 2 -> 3 -> 4;
+  }
+
+  subgraph bottom {
+    rank=same;
+    5 -> 6 -> 7 -> 8 -> 9;
+  }
+
+  /* shift bottom subgraph over */
+  9 -> 1 [color=white];
+
+  4 -> 5;
+
+  1 [label="command line\nparsing" URL="\ref cbmc_parse_optionst"];
+  2 [label="preprocessing,\nparsing" URL="\ref preprocessing"];
+  3 [label="language\ntype-checking" URL="\ref type-checking"];
+  4 [label="goto\nconversion" URL="\ref goto-conversion"];
+  5 [label="instrumentation" URL="\ref instrumentation"];
+  6 [label="symbolic\nexecution" URL="\ref symbolic-execution"];
+  7 [label="SAT/SMT\nencoding" URL="\ref sat-smt-encoding"];
+  8 [label="decision\nprocedure" URL="\ref decision-procedure"];
+  9 [label="counter example\nproduction" URL="\ref counter-example-production"];
+}
+\enddot
+
+The \ref cbmc-user-manual "CBMC User Manual" describes CBMC from a user
+perspective. Each node in the diagram above links to the appropriate
+class or module documentation, describing that particular stage in the
+CBMC pipeline.
+CPROVER is structured in a similar fashion to a compiler. It has
+language specific front-ends which perform limited syntactic analysis
+and then convert to an intermediate format. The intermediate format can
+be output to files (this is what `goto-cc` does) and are (informally)
+referred to as “goto binaries” or “goto programs”. The back-end are
+tools process this format, either directly from the front-end or from
+it’s saved output. These include a wide range of analysis and
+transformation tools (see \ref section-other-tools).
+
+# Concepts #
+## {C, java bytecode} → Parse tree → Symbol table → GOTO programs → GOTO program transformations → BMC → counterexample (goto_tracet) → printing ##
+
+To be documented.
+
+## Instrumentation: goto functions → goto functions ##
+
+To be documented.
+
+## Goto functions → BMC → Counterexample (trace) ##
+
+To be documented.
+
+## Trace → interpreter → memory map ##
+
+To be documented.
+
+## Goto functions → abstract interpretation ##
+
+To be documented.
+
+## Executables (flow of transformations): ##
+
+### goto-cc ###
+
+To be documented.
+
+### goto-instrument ###
+
+To be documented.
+
+### cbmc ###
+
+To be documented.
+
+### goto-analyzer ###
+
+To be documented.

doc/architectural/cbmc-architecture.md

@@ -0,0 +1,82 @@
+\ingroup module_hidden 
+\page compilation-and-development Compilation and Development
+
+\author Martin Brain, Peter Schrammel
+
+## Makefiles ##
+
+First off, read the \ref cbmc-user-manual "CBMC User Manual". It describes
+how to get, build and use CBMC. This document covers the
+internals of the system and how to get started on development.
+
+## CMake files ##
+
+To be documented.
+
+## Personal configuration: config.inc, macro DEBUG ##
+
+To be documented.
+
+## Running tests ##
+
+### Regression tests ###
+
+The regression tests are contained in the `regression/` folder.
+They are grouped into directories for each of the tools/modules.
+Each of these contains multiple directories, each of which contains
+input files and one or more`.desc` files that describe what command
+to run, what output is expected and so on. There is a Perl script,
+`test.pl` that is used to invoke the tests as:
+
+    ../test.pl -c PATH_TO_CBMC
+
+The `–help` option gives instructions for use and the
+format of the description files.
+
+To be documented further.
+
+### Unit tests ###
+
+To be documented.
+
+## Documentation ##
+
+Apart from the (user-orientated) CBMC user manual and this document, most
+of the rest of the documentation is inline in the code as `doxygen` and
+some comments. A man page for CBMC, goto-cc and goto-instrument is
+contained in the `doc/` directory and gives some options for these
+tools. All of these could be improved and patches are very welcome. In
+some cases the algorithms used are described in the relevant papers.
+
+## Accessing doxygen documentation ##
+
+The doxygen documentation can be [accessed online](http://cprover.diffblue.com).
+To build it locally, run `doxygen` in `/src`. HTML output will be created in
+`/doc/html`. The index page is `/doc/html/index.html`.
+
+## Coding standards ##
+
+See <a
+href="https://github.com/diffblue/cbmc/blob/master/CODING_STANDARD.md">
+`CODING_STANDARD.md`</a> file in the root of the CBMC repository.
+
+CPROVER is written in a fairly minimalist subset of C++; templates and
+meta-programming are avoided except where necessary.
+External library dependencies are avoided (only STL and a SAT solver
+are required). Boost is not used. The `util` directory contains many
+utilities that are not (yet) in the standard library.
+
+Patches should be formatted so that code is indented with two space
+characters, not tab and wrapped to 80 columns. Headers for doxygen
+should be given (and preferably filled!) and the author will be the
+person who first created the file. Add doxygen comments to
+undocumented functions as you touch them. Coding standards
+and doxygen comments are enforced by CI before a patch can be
+merged by running `clang-format` and `cpplint`.
+
+Identifiers should be lower case with underscores to separate words.
+Types (classes, structures and typedefs) names must end with a `t`.
+Types that model types (i.e. C types in the program that is being
+interpreted) are named with `_typet`. For example `ui_message_handlert`
+rather than `UI_message_handlert` or `UIMessageHandler` and
+`union_typet`.