Inline assembly support (external call)

.github/workflows/build-in-base-env.yml

@@ -0,0 +1,25 @@
+name: Build in UTBot base_env
+
+on:
+  pull_request:
+    branches: utbot-main
+  push:
+    branches: utbot-main
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    container:
+      image: ghcr.io/unittestbot/utbotcpp/base_env:02-02-2022
+      credentials:
+        username: ${{ github.actor }}
+        password: ${{ secrets.GITHUB_TOKEN }}
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v2
+      - name: Run build.sh
+        run: |
+          ./build.sh
+      - name: Run tests
+        run: |
+          cd build && ninja check

.github/workflows/build.yaml

@@ -2,9 +2,9 @@ name: CI
 
 on:
   pull_request:
-    branches: master
+    branches: utbot-main
   push:
-    branches: master
+    branches: utbot-main
 
 # Defaults for building KLEE
 env:
@@ -43,9 +43,6 @@ jobs:
                 "LLVM 7",
                 "LLVM 6",
                 "LLVM 5",
-                "LLVM 4",
-                "LLVM 3.9",
-                "LLVM 3.8",
                 "ASan",
                 "UBSan",
                 "MSan",
@@ -79,16 +76,6 @@ jobs:
           - name: "LLVM 5"
             env:
               LLVM_VERSION: 5
-          - name: "LLVM 4"
-            env:
-              LLVM_VERSION: 4
-          - name: "LLVM 3.9"
-            env:
-              LLVM_VERSION: 3.9
-          - name: "LLVM 3.8"
-            env:
-              LLVM_VERSION: 3.8
-              USE_LIBCXX: 0
           # Sanitizer builds. Do unoptimized build otherwise the optimizer might remove problematic code
           - name: "ASan"
             env:

.gitignore

@@ -4,9 +4,11 @@ Debug/
 Debug+Asserts/
 Output/
 
+.idea
 # commonly used as cmake build directory
 /build
-
+cmake-build-debug
+cmake-build-release
 cscope.*
 *~
 
@@ -30,3 +32,5 @@ lit.site.cfg
 autoconf/aclocal.m4
 autoconf/autom4te.cache/
 autom4te.cache/
+
+.vscode

.travis.yml

@@ -12,7 +12,7 @@ env:
     ###########################################################################
 
     # Check a subset of the matrix of:
-    #   LLVM  : {3.8, 3.9, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0, 10.0, 11.0}
+    #   LLVM  : {5.0, 6.0, 7.0, 8.0, 9.0, 10.0, 11.0}
     #   SOLVERS : {Z3, STP, STP:Z3, metaSMT}
     #   STP_VERSION   : {2.3.3, master}
     #   METASMT_VERSION : {v4.rc1}
@@ -74,15 +74,6 @@ jobs:
     - name: "LLVM 5"
       env: LLVM_VERSION=5.0
 
-    - name: "LLVM 4"
-      env: LLVM_VERSION=4.0
-
-    - name: "LLVM 3.9"
-      env: LLVM_VERSION=3.9
-
-    - name: "LLVM 3.8"
-      env: LLVM_VERSION=3.8 USE_LIBCXX=0
-
     # Sanitizer builds. Do unoptimized build otherwise the optimizer might remove problematic code
     - name: "ASan"
       env: SANITIZER_BUILD=address ENABLE_OPTIMIZED=0 USE_TCMALLOC=0

CMakeLists.txt

@@ -39,7 +39,7 @@ include(CheckLibraryExists)
 # Project version
 ###############################################################################
 set(KLEE_VERSION_MAJOR 2)
-set(KLEE_VERSION_MINOR 2)
+set(KLEE_VERSION_MINOR 2-utbot_lazy_initialization)
 set(KLEE_VERSION "${KLEE_VERSION_MAJOR}.${KLEE_VERSION_MINOR}")
 
 # If a patch is needed, we can add KLEE_VERSION_PATCH
@@ -516,6 +516,40 @@ else()
   message(STATUS "POSIX runtime disabled")
 endif()
 
+################################################################################
+# KLEE floating point support
+################################################################################
+option(ENABLE_FLOATING_POINT "Enable KLEE's floating point extension" OFF)
+if (ENABLE_FLOATING_POINT)
+  if (NOT ${ENABLE_Z3})
+    message (FATAL_ERROR "Floating point extension is availible only when using Z3 backend."
+            "You should enable Z3 by passing the following option to cmake:\n"
+            "\"-DENABLE_SOLVER_Z3=ON\"\n")
+  else()
+    set(ENABLE_FP 1) # For config.h
+    message(STATUS "Floating point extension enabled")
+  endif()
+else()
+  set(ENABLE_FP 0) # For config.h
+  message(STATUS "Floating point extension disabled")
+endif()
+
+################################################################################
+# KLEE floating point runtime
+################################################################################
+option(ENABLE_FP_RUNTIME "Enable KLEE's floating point runtime" OFF)
+if (ENABLE_FP_RUNTIME)
+  if (NOT ENABLE_FLOATING_POINT)
+    message (FATAL_ERROR "Floating point runtime is availible only when using KLEE fp extension."
+            "You should enable it by passing the following option to cmake:\n"
+            "\"-DENABLE_FLOATING_POINT=ON\"\n")
+  else()
+    message(STATUS "Floating point runtime enabled")
+  endif()
+else()
+  message(STATUS "Floating point runtime disabled")
+endif()
+
 ################################################################################
 # KLEE uclibc support
 ################################################################################
@@ -718,6 +752,11 @@ set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
 set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
 set(KLEE_UTILS_DIR ${CMAKE_SOURCE_DIR}/utils)
 
+################################################################################
+# Set install destination paths for targets
+################################################################################
+set(RUN_KLEE_MAIN_LIB_DEST "lib/run_klee")
+set(RUN_KLEE_LIB_DEST "${RUN_KLEE_MAIN_LIB_DEST}/${CMAKE_BUILD_TYPE}")
 
 ################################################################################
 # Report the value of various variables to aid debugging
@@ -824,4 +863,17 @@ endif()
 ################################################################################
 # Miscellaneous install
 ################################################################################
-install(FILES include/klee/klee.h DESTINATION include/klee)
+install(FILES include/klee/klee.h include/klee/ADT/KTest.h include/klee/ADT/TestCase.h DESTINATION include/klee)
+INSTALL(FILES lib/Core/Executor.h DESTINATION include/klee/Core)
+INSTALL(DIRECTORY include/klee/Expr DESTINATION include/klee)
+INSTALL(DIRECTORY include/klee/Module DESTINATION include/klee)
+INSTALL(DIRECTORY include/klee/Statistics DESTINATION include/klee)
+INSTALL(DIRECTORY include/klee/Support DESTINATION include/klee)
+
+install(EXPORT run_klee
+        DESTINATION "${RUN_KLEE_LIB_DEST}"
+        )
+
+install(FILES cmake/run_klee-config.cmake
+        DESTINATION "${RUN_KLEE_MAIN_LIB_DEST}"
+        )