if(ENABLE_PYTHON_FRONTEND)
  add_definitions(-DPYTHON_FRONTEND)
endif()

add_library(gotoprograms goto_convert.cpp goto_function.cpp goto_main.cpp
  goto_sideeffects.cpp goto_program.cpp goto_check.cpp goto_inline.cpp
  remove_no_op.cpp goto_convert_functions.cpp remove_unreachable.cpp
  builtin_functions.cpp show_claims.cpp destructor.cpp set_claims.cpp
  add_race_assertions.cpp rw_set.cpp goto_binary_reader.cpp static_analysis.cpp
  goto_program_serialization.cpp goto_function_serialization.cpp
  read_bin_goto_object.cpp goto_program_irep.cpp format_strings.cpp
  loop_numbers.cpp goto_loops.cpp goto_loop_simplify.cpp write_goto_binary.cpp
  goto_k_induction.cpp goto_termination.cpp loopst.cpp goto_coverage.cpp goto_coverage_rm.cpp k_path_spanning.cpp goto_cfg.cpp goto_loop_invariant.cpp
  goto_atomicity_check.cpp frame_enforcer.cpp contracts/contracts.cpp)
add_library(gotoalgorithms loop_unroll.cpp mark_decl_as_non_det.cpp assign_params_as_non_det.cpp goto_check_uninit_vars.cpp goto_check_unchecked_return.cpp)

if(ENABLE_GOTO_CONTRACTOR)
    include(SetupIbex)
    add_library(gotocontractor goto_contractor.cpp)
    target_include_directories(gotocontractor PUBLIC ${IBEX_INCLUDE_DIRS} ${IBEX_INCLUDE_DIRS}/ibex ${IBEX_INCLUDE_DIRS}/ibex/3rd)
    target_link_libraries(gotocontractor PUBLIC algorithms gotoprograms PkgConfig::IBEX)
endif()

add_subdirectory(abstract-interpretation)
target_link_libraries(gotoalgorithms PUBLIC algorithms gotoprograms PRIVATE abstract-interpretation)

# gotocontractor uses ait<> which calls ai_baset virtual methods from abstract-interpretation.
# Declaring the cycle lets CMake emit --start-group on static-link builds.
if(ENABLE_GOTO_CONTRACTOR)
    target_link_libraries(gotocontractor PRIVATE abstract-interpretation)
endif()
target_include_directories(gotoprograms
    PRIVATE ${Boost_INCLUDE_DIRS}
)
target_include_directories(gotoalgorithms
    PRIVATE ${Boost_INCLUDE_DIRS}
)
target_compile_definitions(gotoprograms PUBLIC BOOST_ALL_NO_LIB YAML_CPP_STATIC_DEFINE)

target_link_libraries(gotoprograms PUBLIC pointeranalysis PRIVATE bigint usr_utils langapi)