Squashed 'cbmc/' changes from 4f5e148..b0a0002

b0a0002 Merge pull request diffblue#2751 from diffblue/unicode-format
9d8abbf Merge pull request diffblue#2846 from peterschrammel/jbmc-no-cover-tests
86aea9b use status() to output VCCs
f2fa169 draw Gentzen turnstile using Unicode
e152c92 JBMC tests should not use --cover
d33bd22 Merge pull request diffblue#2839 from diffblue/java_class_loader_base
f8ef8dc Merge pull request diffblue#2842 from diffblue/cbmc-help
12637a4 Merge pull request diffblue#2843 from diffblue/split_string_cleanup
049dd2f Merge pull request diffblue#2795 from thomasspriggs/tas/doxygen_styling
646a9d8 use split_string that returns its result
0b9b01a Move `.css` file into `doc` directory
30f055b help: --drop-unused-functions belongs with the transformation
5513c79 remove help for --smt1 option
708acf4 missing newline in help
0881bf2 split_string with return value now also has 'strip' and 'remove_empty'
0a53059 factor out classpath functionality into separate class
f0221b8 Merge pull request diffblue#2782 from mgudemann/doc/doc-20/document-class-files
a6da811 Merge pull request diffblue#2834 from diffblue/protect-exprt-methods
4bfbb48 Correct section entries
3bc445e Merge pull request diffblue#2788 from johnnonweiler/doc/update-folder-walkthrough
b38b671 Merge pull request diffblue#2837 from diffblue/type-convert_dowhile
2e3fd61 Merge pull request diffblue#2832 from diffblue/stack-trace
56c7da7 add typing for convert_dowhile
a594f9f cbmc can now print stack traces
cbe16b3 Merge pull request diffblue#2833 from diffblue/object_descriptor_exprt-root_object
2542c8e Merge pull request diffblue#2835 from johnnonweiler/bugfix/janalyzer_module_dependencies
47c741c Add directory dependencies diagram
d4c4298 Merge pull request diffblue#2816 from smowton/smowton/feature/json-symbol-table
278d2ff Remove jdiff from janalyzer/module_dependencies.txt
84f09a9 move object_descriptor_exprt::root_object into .cpp
68f95d2 add protection to internal methods of exprt
0f0d50b Merge pull request diffblue#2766 from diffblue/jar_index
20e5d89 Implement --show-symbol-table in JSON-UI mode
c5901e0 JSON stream: support streaming a key-value pair to an object
8d2a748 removed jar_indext types and data structures
27d0ae0 java_class_loadert::load_entire_jar now returns the classes loaded
7797757 Merge pull request diffblue#2828 from diffblue/cpp-constructor-optional
f7fc6a9 Merge pull request diffblue#2790 from allredj/doc_exprt
0d5e588 Clean up show_symbol_table
da6e5d7 cpp_typecheckt::cpp_destructor now returns optionalt<codet> instead of an expression
fd5c528 rewrite a no-op
e7d1180 cpp_typecheckt::cpp_constructor now returns optionalt<codet> instead of an expression
d68708f Merge pull request diffblue#2658 from svorenova/bugfix_tg4365
6749aaf Merge pull request diffblue#2670 from mgudemann/feature/multi_object_input_parameter
9dc1f0e Document util/expr.{cpp,h}
4ed36c6 Fix naming in variables for non-deterministic values
f623c0b Simplify code for alternative parameter types
6e96333 Change from optional set to simply set
d2bc012 Allow multi object type parameter in entry point function call
cb0f310 Add nondet.{h.cpp}
e37d051 Add a comment to static field with the name of the field
437be99 Perform nondet-init in clinit_wrapper even if clinit doesn't exist
46d47e0 Add a regression test for nondet-static
2ecf8e8 Add nondet-static option to JBMC
9e6caba Mark final fields in Java as constants
48797b0 Nondet-initialize variables in clinit_wrapper constructor
5fe44ed Pass information to clinit_wrapper constructors
655978c Record nondet-static option in java_bytecode_language
82a1bd3 Merge pull request diffblue#2819 from diffblue/trace-with-arguments2
8646fdd Merge pull request diffblue#2817 from NathanJPhillips/cleanup/lazy-loading
7e6ff00 Merge pull request diffblue#2525 from peterschrammel/range-set-neg-offset-test
4c45282 Merge pull request diffblue#2807 from Degiorgio/ssa-doc
bf717d3 show function arguments in trace
08cbe58 add arguments of function calls to goto_trace
668c4f3 Merge pull request diffblue#2772 from mgudemann/doc/doc-21/java_load_jar
e4bc16e Minor code cleanup related to lazy loading
ccd9783 Merge pull request diffblue#2818 from diffblue/trace-with-arguments
91ad280 Merge pull request diffblue#2812 from allredj/fix-readme-label
333527a Merge pull request diffblue#2801 from antlechner/antonia/doc-13-codet
9e68603 Documentation: updates goto-symex/README.md
fc2e8da Document java_class_loader
c4cd791 Documentation for jar_file
0e6efc7 Documentation for class_loader_limit
43c149d rename 'identifier' to 'function_identifier'
2ebbb24 Merge pull request diffblue#2771 from svorenova/doc_typet
0be9f18 Deconflict labels
12efeab Merge pull request diffblue#2781 from smowton/smowton/docs/fi-analysis
53fac78 Merge pull request diffblue#2813 from diffblue/java-char-literals-are-char
a5ce804 Merge pull request diffblue#2783 from smowton/smowton/docs/goto-program
6493c4a Merge pull request diffblue#2796 from smowton/smowton/docs/goto-symex
ad7902a Merge pull request diffblue#2811 from sonodtt/invariant-docs-change
e37e9b8 Remove unneeded header
f08773b Amend DATA_INVARIANT docs
592b114 Add documentation to std_types
7ad664c Add documentation to type_eq
a54746f Add documentation to typet
1273eac Merge pull request diffblue#2804 from NathanJPhillips/cleanup/switch-lazy-mode
a78b5bd First part of codet documentation
ed7dc1d no need for cast for Java char literals
156e3d3 Document class file content for JBMC / java_bytecode readme
93b3e9c Merge pull request diffblue#2752 from NathanJPhillips/feature/parse-parameter-annotations
667738a Use a switch statement for clarity
8d38c5d Briefly document flow-insensitive analysis
a812ba2 Improve goto-symex documentation
45933d0 Update docs for goto-programs
78d22fb Merge pull request diffblue#2763 from diffblue/classpath
b7c430d Merge pull request diffblue#2797 from owen-jones-diffblue/doc/fix-doxygen-errors
61c44d2 Merge pull request diffblue#2799 from apaschos/doxy
589a584 Merge pull request diffblue#2779 from antlechner/antonia/doc-util-readme
c679e55 Merge pull request diffblue#2776 from smowton/smowton/docs/call-graph
dc03c8a Merge pull request diffblue#2778 from smowton/smowton/docs/constant-prop
abae6a0 Merge pull request diffblue#2774 from smowton/smowton/docs/object-numbering
849f256 Merge pull request diffblue#2770 from smowton/smowton/docs/symbol-table
03b7bf2 Enable parsing of annotations on parameters
db7c127 Combine padding specifiers
284137a Add extra spacing to code blocks
64dd1af Set style of left hand navigation tree
4b827eb Set link colours to mustard initially and purple for visited
740eed7 Collapse by default the dependency graphs
4bbaa9d Remove references from and to other functions
5e8308f Merge pull request diffblue#2769 from smowton/smowton/docs/irept
a3b652c Change the order of appearance of class methods
e4224a1 Fix colons in doxygen
68ca9a1 Correct parameter names to stop doxygen warning
dc686bc Reduce heading sizes
712c168 Fix unclosed ``` causing doxygen warning
f8d0fb8 Add overview of constant propagator
665e183 Add call-graph overview
ef5ff03 Add a little more detail and discussion on irept
b227eee Document symbol table and namespace
3f2537d Document dstring to string conversions
2675090 Add documentation for object numbering
af6efcb Make inline code more distinctive
8095948 Add custom style sheet for doxygen html output
096decd Remove links to clobber and memory-models in doc
53b3c4a remove redundant class loader limit test
dbd6988 Merge pull request diffblue#2750 from johnnonweiler/documentation-structure
ba7e06f precompute the category of the classpath entry
5dbd48c unify jar list and classpath
24cbfc6 Merge pull request diffblue#2765 from diffblue/jar_pool
76dbb2a Remove links to classes from high level overview
384f0d4 use jar_poolt in java_class_loadert
d601a44 factor out pool for JARs into jar_poolt
4dddd0c Merge pull request diffblue#2760 from diffblue/jar_pool_cleanup
dbc95f8 java_class_loadert: remove unused parameter
8640288 Merge pull request diffblue#2698 from diffblue/clang-builtins
4ffc2a4 Merge pull request diffblue#2744 from danpoe/feature/invariants-with-diagnostic-information
d0be385 Merge pull request diffblue#2619 from JohnDumbell/jd/bugfix/java_annotation_array_fix
ac6c7d4 Parse java arrays in annotations properly
cb090bf add clang's __builtin_ia32_undefX and __builtin_nontemporal_store and __builtin_nontemporal_load
1ad6b5d Merge pull request diffblue#2754 from antlechner/antonia/ci-lazy-loading-rec-clinit
03bdf37 Merge pull request diffblue#2755 from diffblue/COMPILING-again
df0605e Add test for enum field of argument type
ad1b1d8 Red Hat and Fedora now use dnf instead of yum
c1ef758 jbmc build now uses Maven, not unzip
aa1de84 implement clang's builtin_convertvector
49089b1 Fix lazy loading of enum static initializers
e1fc49f Merge pull request diffblue#2720 from tautschnig/replace_symbol-cleanup1
e327ef2 replace_symbolt: hide {expr,type}_map
3f487c3 Merge pull request diffblue#2724 from tautschnig/replace-symbolt-unit-test
963b866 format_expr now produces unicode
c55d032 Unit test of replace_symbolt
544671e Move 'Flattening' section in solvers/README.md
794ba03 Change heading in java-bytecode docs
1e2fda3 Workaround for Visual Studio not expanding __VA_ARGS__ on macro invocation
f2f2156 Tests for invariant macros with diagnostic output
8a37a2d Invariant macros with diagnostic information
bcb7c76 Merge pull request diffblue#2747 from diffblue/cleanup-message-handler
0d8ea2c remove sequence number from message_handler interface
4557374 use size_t for message counts
ccf3c50 Add outline to module docs
0b7c4fb Add sections to java_bytecode/README.md
85a81ea Merge pull request diffblue#2594 from thk123/array_type_check
2becafd Merge pull request diffblue#2738 from diffblue/remove-memory-models
c2825ef Merge pull request diffblue#2741 from diffblue/remove_asm_function_id
aa7b89f Merge pull request diffblue#2742 from diffblue/symbol_type_fix
1f06cde Merge pull request diffblue#2743 from tautschnig/boolbv-width
ba57a14 remove memory-models
4e95060 Merge pull request diffblue#2739 from diffblue/remove-clobber
0661075 Delete one word ('testing')
d6755b0 Move solvers API description to solvers module
f7bcd0a Move java_bytecode explanations to module doc
ccaa87c Move examples from code-walkthrough to linked module
d33628e Fix boolbv_widtht::get_entry and fail for unknown types
a1d59d2 remove clobber
ef509a5 two further instances of symbol_type
ef4bb3c properly set function id on instructions added by remove_asm
0695df6 Switch one file from ## to using sections
124d012 Combined many pages of developer docs into one
96dc0a3 Fix minor typos
d42821f Adding can_cast_type for array_typet
35e278e Move docs from guide to module-level docs
147c5d9 Add header for orphaned diagram
3eee998 Add references to class-level documentation
d924247 Add in empty lines after headings
3b74238 Fix apostrophe
90e43d9 Fix "#" being converted to "::" in doxygen
c423bb6 Add links to module level documentation
2034faf Move two items out of list
37128c0 Improve how a sentence reads
2ea73b8 Move "Tutorial" section to the right place
dfcb7cd Describe the aim of the documentation marked as "For contributors"
1920f17 Test for byte extract with negative offset

git-subtree-dir: cbmc
git-subtree-split: b0a0002

Author: Owen Jones

.travis.yml

@@ -352,7 +352,6 @@ install:
   - make -C src/ansi-c library_check
   - make -C src/cpp library_check
   - make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3
-  - make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3 clobber.dir memory-models.dir
   - make -C jbmc/src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3
 
 script:

CMakeLists.txt

@@ -52,8 +52,6 @@ set_target_properties(
     big-int
     cbmc
     cbmc-lib
-    clobber
-    clobber-lib
     cpp
     driver
     goto-analyzer
@@ -71,7 +69,6 @@ set_target_properties(
     langapi
     linking
     miniBDD
-    mmcc
     pointer-analysis
     solvers
     test-bigint

COMPILING.md

@@ -37,11 +37,11 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
    To compile JBMC, you additionally need the JDK and the java-models-library.
    For the JDK, on Debian-like distributions, do as root:
    ```
-   apt-get install unzip openjdk-8-jdk
+   apt-get install openjdk-8-jdk maven
    ```
    On Red Hat/Fedora or derivates, do as root:
    ```
-   dnf install unzip java-1.8.0-openjdk-devel
+   dnf install java-1.8.0-openjdk-devel maven
    ```
 
 2. As a user, get the CBMC source via
@@ -220,7 +220,7 @@ require manual modification of build files.
      ```
    - On Red Hat/Fedora or derivates, do
      ```
-     yum install cmake
+     dnf install cmake
      ```
    - On macOS, do
      ```

doc/architectural/background-concepts.md

@@ -3,30 +3,30 @@
 
 \author Martin Brain, Peter Schrammel
 
-# Representations #
+\section representations_section Representations
 
-## AST: types, globals, variables, functions, code blocks, language primitives, assignments, expressions, variables ##
+\subsection AST_section AST: types, globals, variables, functions, code blocks, language primitives, assignments, expressions, variables
 
 To be documented.
 
-## CFG ##
+\subsection CFG_section CFG
 
 To be documented.
 
-## SSA ##
+\subsection SSA_section SSA
 
 To be documented.
 
-# Analysis techniques #
+\section analysis_techniques_section Analysis techniques
 
-## Bounded model checking ##
+\subsection BMC_section Bounded model checking
 
 To be documented (can copy from the CBMC manual).
 
-## SAT and SMT ##
+\subsection SAT_section SAT and SMT
 
 To be documented.
 
-## Static analysis ##
+\subsection static_analysis_section Static analysis
 
 To be documented.

doc/architectural/bmct-class.md

@@ -52,7 +52,7 @@ 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).
+transformation tools (see \ref other-tools).
 
 # Concepts #
 ## {C, java bytecode} → Parse tree → Symbol table → GOTO programs → GOTO program transformations → BMC → counterexample (goto_tracet) → printing ##

doc/architectural/cbmc-architecture.md

@@ -0,0 +1,53 @@
+\ingroup module_hidden 
+\page code-walkthrough Code Walkthrough
+
+\author Cesar Rodriguez, Owen Jones
+
+\section data-structures-core-structures-and-ast-section Data structures: core structures and AST
+
+The core structures used for representing abstract syntax trees are all
+documented in \ref util.
+
+\section data-structures-from-ast-to-goto-program-section Data structures: from AST to GOTO program
+
+See \ref goto-programs, \ref goto_programt and [instructiont](\ref goto_programt::instructiont).
+
+\section front-end-languages-generating-codet-from-multiple-languages-section Front-end languages: generating codet from multiple languages
+
+\subsection language-uit-section language_uit, language_filest, languaget classes:
+
+See \ref langapi.
+
+\subsection languages-c-section C
+
+See \ref ansi-c.
+
+\subsection languages-cpp-section C++
+
+See \ref cpp.
+
+\subsection languages-java-section Java bytecode
+
+See \ref java_bytecode.
+
+\section bmct-class-section Bmct class
+
+\subsection equation-section equation
+
+See \ref symex-overview.
+
+
+\section symbolic-executors-section Symbolic executors
+
+\subsection symbolic-execution-section Symbolic execution
+
+See \ref symex-overview.
+
+
+\section solvers-infrastructure-section Solvers infrastructure
+
+See \ref solvers-overview.
+
+\section  static-analysis-apis-section Static analysis APIs
+
+See \ref analyses and \ref pointer-analysis.

doc/architectural/code-walkthrough.md

@@ -24,7 +24,7 @@ To be documented.
 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
+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: