Import ikos 1.3

.clang-format

@@ -0,0 +1,16 @@
+---
+BasedOnStyle: Google
+---
+Language: Cpp
+SpacesInAngles: true
+AccessModifierOffset: -2
+DerivePointerAlignment: false
+AllowShortIfStatementsOnASingleLine: false
+AllowShortLoopsOnASingleLine: false
+AllowShortFunctionsOnASingleLine: Inline
+BinPackParameters: false
+BinPackArguments: false
+PenaltyBreakBeforeFirstCallParameter: 5000
+PenaltyReturnTypeOnItsOwnLine: 500
+SpacesBeforeTrailingComments: 1
+---

.gitignore

@@ -0,0 +1,38 @@
+build
+
+# Editors
+*.swp
+*~
+.ycm_extra_conf.py
+
+# Python
+*.pyc
+__pycache__
+
+# Object files
+*.o
+*.ko
+*.obj
+*.elf
+
+# Libraries
+*.lib
+*.a
+
+# Shared objects (inc. Windows DLLs)
+*.dll
+*.so
+*.so.*
+*.dylib
+
+# Executables
+*.exe
+*.out
+*.app
+*.i*86
+*.x86_64
+*.hex
+
+# IKOS
+*.ar
+*.db

CMakeLists.txt

@@ -0,0 +1,95 @@
+#*******************************************************************************
+#
+# Author: Maxime Arthaud
+#
+# Contact: ikos@lists.nasa.gov
+#
+# Notices:
+#
+# Copyright (c) 2011-2017 United States Government as represented by the
+# Administrator of the National Aeronautics and Space Administration.
+# All Rights Reserved.
+#
+# Disclaimers:
+#
+# No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF
+# ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT LIMITED
+# TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO SPECIFICATIONS,
+# ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE,
+# OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL BE
+# ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF PROVIDED, WILL CONFORM TO
+# THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN ANY MANNER, CONSTITUTE AN
+# ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR RECIPIENT OF ANY RESULTS,
+# RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR ANY OTHER APPLICATIONS
+# RESULTING FROM USE OF THE SUBJECT SOFTWARE.  FURTHER, GOVERNMENT AGENCY
+# DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING THIRD-PARTY SOFTWARE,
+# IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES IT "AS IS."
+#
+# Waiver and Indemnity:  RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST
+# THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL
+# AS ANY PRIOR RECIPIENT.  IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS
+# IN ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH
+# USE, INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM,
+# RECIPIENT'S USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD
+# HARMLESS THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS,
+# AS WELL AS ANY PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW.
+# RECIPIENT'S SOLE REMEDY FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE,
+# UNILATERAL TERMINATION OF THIS AGREEMENT.
+#
+#*****************************************************************************/
+
+cmake_minimum_required(VERSION 2.8.12.2 FATAL_ERROR)
+
+project(ikos)
+set(PACKAGE_VERSION "1.3")
+
+#
+# Build settings
+#
+
+if (CMAKE_SOURCE_DIR STREQUAL CMAKE_BINARY_DIR)
+  message (FATAL_ERROR
+    "In-source builds are not allowed. Please clean your source tree and try again.")
+endif()
+
+if (NOT CMAKE_BUILD_TYPE)
+  set(CMAKE_BUILD_TYPE "Release" CACHE STRING "Choose the type of build." FORCE)
+endif()
+
+if (CMAKE_INSTALL_PREFIX_INITIALIZED_TO_DEFAULT)
+  set(CMAKE_INSTALL_PREFIX "${CMAKE_SOURCE_DIR}/install" CACHE STRING "Install directory." FORCE)
+endif()
+message(STATUS "All libraries and binaries will be installed in ${CMAKE_INSTALL_PREFIX}")
+
+# Do not build anything when running make install
+set(CMAKE_SKIP_INSTALL_ALL_DEPENDENCY TRUE)
+
+# Add path for custom modules
+set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_CURRENT_SOURCE_DIR}/cmake")
+
+# Enable tests
+include(CTest)
+enable_testing()
+
+# Add abstract-representation
+add_subdirectory(abs-repr)
+
+set(ARBOS_FOUND "ON")
+set(ARBOS_INCLUDE_DIR "${CMAKE_SOURCE_DIR}/abs-repr/include")
+set(ARBOS_LIB arbos-api)
+set(ARBOS_BIN "")
+
+# LLVM frontend
+add_subdirectory(frontends/llvm)
+
+# IKOS core
+add_subdirectory(core)
+
+set(IKOS_FOUND "ON")
+set(IKOS_INCLUDE_DIR "${CMAKE_SOURCE_DIR}/core/include")
+
+# Analyzer
+add_subdirectory(analyzer)
+
+# Doxygen
+add_custom_target(docs DEPENDS doxygen-arbos doxygen-ikos doxygen-analyzer)