Merge branch 'develop' into loop_abstract

Author: zhixing-xu

.travis.yml

@@ -49,18 +49,14 @@ jobs:
       env:
         NAME: "DOXYGEN-CHECK"
         DOXYGEN_VERSION: "1.8.14"
-      addons:
-        apt:
-          sources:
-            - sourceline: 'deb http://packages.cloud.google.com/apt cloud-sdk-trusty main'
-              key_url: 'https://packages.cloud.google.com/apt/doc/apt-key.gpg'
-          packages:
-            - cmake
-            - google-cloud-sdk
-            - graphviz
       cache:
         directories:
           - ${TRAVIS_BUILD_DIR}/doxygen/build/bin
+      before_install:
+        - curl -sSL "https://packages.cloud.google.com/apt/doc/apt-key.gpg" | sudo -E apt-key add -
+        - echo "deb http://packages.cloud.google.com/apt cloud-sdk-trusty main" | sudo tee -a /etc/apt/sources.list > /dev/null
+        - sudo apt-get update --option Acquire::Retries=100 --option Acquire::http::Timeout="60"
+        - sudo -E apt-get -yq --no-install-suggests --no-install-recommends --force-yes install cmake google-cloud-sdk graphviz
       install:
         - |
           # Build doxygen if it is not in Travis cache
@@ -90,7 +86,7 @@ jobs:
     # Ubuntu Linux with glibc using g++-5
     - stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
       os: linux
-      sudo: false
+      sudo: true
       compiler: gcc
       cache: ccache
       addons:
@@ -125,7 +121,7 @@ jobs:
     # Ubuntu Linux with glibc using g++-5, debug mode
     - stage: Test different OS/CXX/Flags
       os: linux
-      sudo: false
+      sudo: true
       compiler: gcc
       cache: ccache
       addons:
@@ -149,22 +145,24 @@ jobs:
     # Ubuntu Linux with glibc using clang++-3.7, no-debug mode
     - stage: Test different OS/CXX/Flags
       os: linux
-      sudo: false
+      sudo: true
       compiler: clang
       cache: ccache
       addons:
         apt:
           sources:
             - ubuntu-toolchain-r-test
-            - llvm-toolchain-precise-3.7
           packages:
             - libwww-perl
-            - clang-3.7
             - g++-5
             - libstdc++-5-dev
             - libubsan0
             - parallel
       before_install:
+        - curl -sSL "http://apt.llvm.org/llvm-snapshot.gpg.key" | sudo -E apt-key add -
+        - echo "deb http://apt.llvm.org/precise/ llvm-toolchain-precise-3.7 main" | sudo tee -a /etc/apt/sources.list > /dev/null
+        - sudo apt-get update --option Acquire::Retries=100 --option Acquire::http::Timeout="60"
+        - sudo -E apt-get -yq --no-install-suggests --no-install-recommends --force-yes install clang-3.7
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
         - ln -s /usr/bin/c++-5 bin/g++
@@ -178,21 +176,23 @@ jobs:
     # Ubuntu Linux with glibc using clang++-3.7, debug mode, disable USE_DSTRING
     - stage: Test different OS/CXX/Flags
       os: linux
-      sudo: false
+      sudo: true
       compiler: clang
       cache: ccache
       addons:
         apt:
           sources:
             - ubuntu-toolchain-r-test
-            - llvm-toolchain-precise-3.7
           packages:
             - libwww-perl
-            - clang-3.7
             - g++-5
             - libstdc++-5-dev
             - libubsan0
       before_install:
+        - curl -sSL "http://apt.llvm.org/llvm-snapshot.gpg.key" | sudo -E apt-key add -
+        - echo "deb http://apt.llvm.org/precise/ llvm-toolchain-precise-3.7 main" | sudo tee -a /etc/apt/sources.list > /dev/null
+        - sudo apt-get update --option Acquire::Retries=100 --option Acquire::http::Timeout="60"
+        - sudo -E apt-get -yq --no-install-suggests --no-install-recommends --force-yes install clang-3.7
         - mkdir bin
         - ln -s /usr/bin/gcc-5 bin/gcc
         - ln -s /usr/bin/g++-5 bin/g++
@@ -207,6 +207,7 @@ jobs:
     # cmake build using g++-5
     - stage: Test different OS/CXX/Flags
       os: linux
+      sudo: true
       compiler: gcc
       cache: ccache
       env:
@@ -232,6 +233,7 @@ jobs:
     # cmake build using g++-7
     - stage: Test different OS/CXX/Flags
       os: linux
+      sudo: true
       compiler: gcc
       cache: ccache
       env:
@@ -257,6 +259,7 @@ jobs:
     # cmake build using clang++-6
     - stage: Test different OS/CXX/Flags
       os: linux
+      sudo: true
       compiler: clang
       cache: ccache
       env:
@@ -311,7 +314,7 @@ jobs:
     - stage: Test different OS/CXX/Flags
       if: type = cron
       os: linux
-      sudo: false
+      sudo: true
       compiler: gcc
       cache: ccache
       addons:

COMPILING.md

@@ -202,9 +202,9 @@ helpful for GUI-based tasks, e.g., the class viewer, debugging, etc., and can
 be used for building with MSBuild.  Note that you still need to run flex/bison
 using "make generated_files" before opening the project.
 
-# WORKING WITH CMAKE (EXPERIMENTAL)
+# WORKING WITH CMAKE
 
-There is an experimental build based on CMake instead of hand-written
+There is also a build based on CMake instead of hand-written
 makefiles. It should work on a wider variety of systems than the standard
 makefile build, and can integrate better with IDEs and static-analysis tools.
 On Windows, the CMake build does not depend on Cygwin or MinGW, and doesn't

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.