===========================================================
.___ __ __
_________________ __ __ __| _/|__|/ |_
/ ___\_` __ \__ \ | | \/ __ | | \\_ __\
/ /_/ > | \// __ \| | / /_/ | | || |
\___ /|__| (____ /____/\____ | |__||__|
/_____/ \/ \/
grep rough audit - static analysis tool
v2.8 written by @Wireghoul
=================================[justanotherhacker.com]===
z3-4.8.9/CMakeLists.txt-57-################################################################################
z3-4.8.9/CMakeLists.txt:58:include(${PROJECT_SOURCE_DIR}/cmake/git_utils.cmake)
z3-4.8.9/CMakeLists.txt-59-macro(disable_git_describe)
##############################################
z3-4.8.9/CMakeLists.txt-177-################################################################################
z3-4.8.9/CMakeLists.txt:178:include(${PROJECT_SOURCE_DIR}/cmake/target_arch_detect.cmake)
z3-4.8.9/CMakeLists.txt-179-detect_target_architecture(TARGET_ARCHITECTURE)
##############################################
z3-4.8.9/CMakeLists.txt-185-################################################################################
z3-4.8.9/CMakeLists.txt:186:include(${PROJECT_SOURCE_DIR}/cmake/z3_add_cxx_flag.cmake)
z3-4.8.9/CMakeLists.txt-187-
##############################################
z3-4.8.9/CMakeLists.txt-327-################################################################################
z3-4.8.9/CMakeLists.txt:328:include(${PROJECT_SOURCE_DIR}/cmake/compiler_warnings.cmake)
z3-4.8.9/CMakeLists.txt-329-
##############################################
z3-4.8.9/CMakeLists.txt-393-################################################################################
z3-4.8.9/CMakeLists.txt:394:include(${PROJECT_SOURCE_DIR}/cmake/compiler_lto.cmake)
z3-4.8.9/CMakeLists.txt-395-
##############################################
z3-4.8.9/CMakeLists.txt-431-if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
z3-4.8.9/CMakeLists.txt:432: include(${PROJECT_SOURCE_DIR}/cmake/msvc_legacy_quirks.cmake)
z3-4.8.9/CMakeLists.txt-433-endif()
##############################################
z3-4.8.9/CMakeLists.txt-538-################################################################################
z3-4.8.9/CMakeLists.txt:539:include(${PROJECT_SOURCE_DIR}/cmake/z3_add_component.cmake)
z3-4.8.9/CMakeLists.txt:540:include(${PROJECT_SOURCE_DIR}/cmake/z3_append_linker_flag_list_to_target.cmake)
z3-4.8.9/CMakeLists.txt-541-add_subdirectory(src)
##############################################
z3-4.8.9/README-CMake.md-380-The build system supports single configuration and multi-configuration generators. This means
z3-4.8.9/README-CMake.md:381:it is not possible to know the build type at configure time and therefore ``${CMAKE_BUILD_TYPE}``
z3-4.8.9/README-CMake.md-382-should not be conditionally used to set compiler flags or definitions. Instead you should use Generator expressions which are evaluated by the generator.
##############################################
z3-4.8.9/cmake/Z3Config.cmake.in-13-# Exported targets
z3-4.8.9/cmake/Z3Config.cmake.in:14:include("${CMAKE_CURRENT_LIST_DIR}/Z3Targets.cmake")
z3-4.8.9/cmake/Z3Config.cmake.in-15-
##############################################
z3-4.8.9/cmake/compiler_lto.cmake-42- # `Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS`) doesn't seem to support generator
z3-4.8.9/cmake/compiler_lto.cmake:43: # expressions so we can't do `$<$<CONFIG:Release>:${_lto_linker_flag}>`.
z3-4.8.9/cmake/compiler_lto.cmake-44- set(CMAKE_CXX_FLAGS_${_config} "${CMAKE_CXX_FLAGS_${_config}} ${_lto_compiler_flag}")
##############################################
z3-4.8.9/doc/design_recfuns.md-46-
z3-4.8.9/doc/design_recfuns.md:47:and a special literal `[max_depth=$n]` for each `n:int`.
z3-4.8.9/doc/design_recfuns.md-48-Solving is done under the local assumption
z3-4.8.9/doc/design_recfuns.md:49:`[max_depth=$current_max_unfold_depth]` (this should be handled in some outer
z3-4.8.9/doc/design_recfuns.md-50-loop, e.g. in a custom tactic).
##############################################
z3-4.8.9/doc/design_recfuns.md-53-`unfold_depth`. If `unfold_depth > current_max_unfold_depth`, then
z3-4.8.9/doc/design_recfuns.md:54:the conflict clause `[max_depth=$current_max_unfold_depth] => Γ => false`
z3-4.8.9/doc/design_recfuns.md-55-where `Γ` is the conjunction of all `A_f_i[t1…tn]` true in the trail.
##############################################
z3-4.8.9/doc/design_recfuns.md-59-If the solver answers "SAT", we have a model.
z3-4.8.9/doc/design_recfuns.md:60:Otherwise, if `[max_depth=$current_max_unfold_depth]` is part of the
z3-4.8.9/doc/design_recfuns.md-61-unsat-core, then we increase `current_max_unfold_depth`.
##############################################
z3-4.8.9/scripts/mk_util.py-3210- install`` and ``make uninstall``. These methods correctly use
z3-4.8.9/scripts/mk_util.py:3211: ``$(PREFIX)`` and ``$(DESTDIR)`` and therefore are preferable
z3-4.8.9/scripts/mk_util.py-3212- to writing commands manually which can be error prone.
##############################################
z3-4.8.9/scripts/mk_util.py-3360- # helper to simplify code. This will also let us replace ``@`` with
z3-4.8.9/scripts/mk_util.py:3361: # ``$(Verb)`` and have it set to ``@`` or empty at build time depending on
z3-4.8.9/scripts/mk_util.py-3362- # a variable (e.g. ``VERBOSE``) passed to the ``make`` invocation. This
##############################################
z3-4.8.9/scripts/update_api.py-997- log_c.write(" P(0);\n")
z3-4.8.9/scripts/update_api.py:998: exe_c.write("in.get_obj_addr(%s)" % i)
z3-4.8.9/scripts/update_api.py-999- elif ty == PRINT_MODE or ty == ERROR_CODE:
##############################################
z3-4.8.9/scripts/update_api.py-1008- log_c.write(" P(0);\n")
z3-4.8.9/scripts/update_api.py:1009: exe_c.write("reinterpret_cast<%s>(in.get_obj_addr(%s))" % (param2str(p), i))
z3-4.8.9/scripts/update_api.py-1010- elif ty == STRING:
z3-4.8.9/scripts/update_api.py-1011- log_c.write(" S(\"\");\n")
z3-4.8.9/scripts/update_api.py:1012: exe_c.write("in.get_str_addr(%s)" % i)
z3-4.8.9/scripts/update_api.py-1013- elif ty == UINT:
z3-4.8.9/scripts/update_api.py-1014- log_c.write(" U(0);\n")
z3-4.8.9/scripts/update_api.py:1015: exe_c.write("in.get_uint_addr(%s)" % i)
z3-4.8.9/scripts/update_api.py-1016- elif ty == UINT64:
z3-4.8.9/scripts/update_api.py-1017- log_c.write(" U(0);\n")
z3-4.8.9/scripts/update_api.py:1018: exe_c.write("in.get_uint64_addr(%s)" % i)
z3-4.8.9/scripts/update_api.py-1019- elif ty == INT:
z3-4.8.9/scripts/update_api.py-1020- log_c.write(" I(0);\n")
z3-4.8.9/scripts/update_api.py:1021: exe_c.write("in.get_int_addr(%s)" % i)
z3-4.8.9/scripts/update_api.py-1022- elif ty == INT64:
z3-4.8.9/scripts/update_api.py-1023- log_c.write(" I(0);\n")
z3-4.8.9/scripts/update_api.py:1024: exe_c.write("in.get_int64_addr(%s)" % i)
z3-4.8.9/scripts/update_api.py-1025- elif ty == VOID_PTR:
z3-4.8.9/scripts/update_api.py-1026- log_c.write(" P(0);\n")
z3-4.8.9/scripts/update_api.py:1027: exe_c.write("in.get_obj_addr(%s)" % i)
z3-4.8.9/scripts/update_api.py-1028- else:
##############################################
z3-4.8.9/src/api/dotnet/CMakeLists.txt-180- # move the local repo to the installation directory (cancel the build-time repo)
z3-4.8.9/src/api/dotnet/CMakeLists.txt:181: install(CODE "include(${CMAKE_CURRENT_LIST_DIR}/../../../cmake/modules/FindDotnet.cmake)\n DOTNET_REGISTER_LOCAL_REPOSITORY(\"${Z3_DOTNET_LOCALREPO_NAME}\" \"${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR}/z3.nuget\")")
z3-4.8.9/src/api/dotnet/CMakeLists.txt-182- install(FILES "${PROJECT_BINARY_DIR}/Microsoft.Z3/Microsoft.Z3.xml" DESTINATION "${CMAKE_INSTALL_LIBDIR}/z3.nuget")
##############################################
z3-4.8.9/src/api/dotnet/Solver.cs-335- ASTVector vars = new ASTVector(Context);
z3-4.8.9/src/api/dotnet/Solver.cs:336: foreach (var asm in assumptions) asms.Push(asm);
z3-4.8.9/src/api/dotnet/Solver.cs-337- foreach (var v in variables) vars.Push(v);
##############################################
z3-4.8.9/src/api/java/Solver.java-273- ASTVector vars = new ASTVector(getContext());
z3-4.8.9/src/api/java/Solver.java:274: for (BoolExpr asm : assumptions) asms.push(asm);
z3-4.8.9/src/api/java/Solver.java-275- for (Expr v : variables) vars.push(v);
##############################################
z3-4.8.9/src/api/ml/README.md-203-The `dllz3ml.so` is usually installed in the stubs library in opam
z3-4.8.9/src/api/ml/README.md:204:installation (`$(opam config var lib)/stublibs`), it is done
z3-4.8.9/src/api/ml/README.md-205-automatically by `ocamlfind` so no special treatment is needed.
##############################################
z3-4.8.9/src/api/z3_replayer.cpp-660-
z3-4.8.9/src/api/z3_replayer.cpp:661: int * get_int_addr(unsigned pos) {
z3-4.8.9/src/api/z3_replayer.cpp-662- check_arg(pos, INT64);
##############################################
z3-4.8.9/src/api/z3_replayer.cpp-665-
z3-4.8.9/src/api/z3_replayer.cpp:666: int64_t * get_int64_addr(unsigned pos) {
z3-4.8.9/src/api/z3_replayer.cpp-667- check_arg(pos, INT64);
##############################################
z3-4.8.9/src/api/z3_replayer.cpp-670-
z3-4.8.9/src/api/z3_replayer.cpp:671: unsigned * get_uint_addr(unsigned pos) {
z3-4.8.9/src/api/z3_replayer.cpp-672- check_arg(pos, UINT64);
##############################################
z3-4.8.9/src/api/z3_replayer.cpp-675-
z3-4.8.9/src/api/z3_replayer.cpp:676: uint64_t * get_uint64_addr(unsigned pos) {
z3-4.8.9/src/api/z3_replayer.cpp-677- check_arg(pos, UINT64);
##############################################
z3-4.8.9/src/api/z3_replayer.cpp-680-
z3-4.8.9/src/api/z3_replayer.cpp:681: Z3_string * get_str_addr(unsigned pos) {
z3-4.8.9/src/api/z3_replayer.cpp-682- check_arg(pos, STRING);
##############################################
z3-4.8.9/src/api/z3_replayer.cpp-685-
z3-4.8.9/src/api/z3_replayer.cpp:686: void ** get_obj_addr(unsigned pos) {
z3-4.8.9/src/api/z3_replayer.cpp-687- check_arg(pos, OBJECT);
##############################################
z3-4.8.9/src/api/z3_replayer.cpp-788-
z3-4.8.9/src/api/z3_replayer.cpp:789:int * z3_replayer::get_int_addr(unsigned pos) {
z3-4.8.9/src/api/z3_replayer.cpp:790: return m_imp->get_int_addr(pos);
z3-4.8.9/src/api/z3_replayer.cpp-791-}
z3-4.8.9/src/api/z3_replayer.cpp-792-
z3-4.8.9/src/api/z3_replayer.cpp:793:int64_t * z3_replayer::get_int64_addr(unsigned pos) {
z3-4.8.9/src/api/z3_replayer.cpp:794: return m_imp->get_int64_addr(pos);
z3-4.8.9/src/api/z3_replayer.cpp-795-}
z3-4.8.9/src/api/z3_replayer.cpp-796-
z3-4.8.9/src/api/z3_replayer.cpp:797:unsigned * z3_replayer::get_uint_addr(unsigned pos) {
z3-4.8.9/src/api/z3_replayer.cpp:798: return m_imp->get_uint_addr(pos);
z3-4.8.9/src/api/z3_replayer.cpp-799-}
z3-4.8.9/src/api/z3_replayer.cpp-800-
z3-4.8.9/src/api/z3_replayer.cpp:801:uint64_t * z3_replayer::get_uint64_addr(unsigned pos) {
z3-4.8.9/src/api/z3_replayer.cpp:802: return m_imp->get_uint64_addr(pos);
z3-4.8.9/src/api/z3_replayer.cpp-803-}
z3-4.8.9/src/api/z3_replayer.cpp-804-
z3-4.8.9/src/api/z3_replayer.cpp:805:Z3_string * z3_replayer::get_str_addr(unsigned pos) {
z3-4.8.9/src/api/z3_replayer.cpp:806: return m_imp->get_str_addr(pos);
z3-4.8.9/src/api/z3_replayer.cpp-807-}
z3-4.8.9/src/api/z3_replayer.cpp-808-
z3-4.8.9/src/api/z3_replayer.cpp:809:void ** z3_replayer::get_obj_addr(unsigned pos) {
z3-4.8.9/src/api/z3_replayer.cpp:810: return m_imp->get_obj_addr(pos);
z3-4.8.9/src/api/z3_replayer.cpp-811-}
##############################################
z3-4.8.9/src/api/z3_replayer.h-56-
z3-4.8.9/src/api/z3_replayer.h:57: int * get_int_addr(unsigned pos);
z3-4.8.9/src/api/z3_replayer.h:58: int64_t * get_int64_addr(unsigned pos);
z3-4.8.9/src/api/z3_replayer.h:59: unsigned * get_uint_addr(unsigned pos);
z3-4.8.9/src/api/z3_replayer.h:60: uint64_t * get_uint64_addr(unsigned pos);
z3-4.8.9/src/api/z3_replayer.h:61: Z3_string * get_str_addr(unsigned pos);
z3-4.8.9/src/api/z3_replayer.h:62: void ** get_obj_addr(unsigned pos);
z3-4.8.9/src/api/z3_replayer.h-63-
##############################################
z3-4.8.9/src/math/lp/hnf.h-11- Creates the Hermite Normal Form of a matrix in place.
z3-4.8.9/src/math/lp/hnf.h:12: We suppose that $A$ is an integral $m$ by $n$ matrix or rank $m$, where $n >= m$.
z3-4.8.9/src/math/lp/hnf.h-13- The paragraph below is applicable to the usage of HNF.
##############################################
z3-4.8.9/src/opt/maxres.cpp-431-
z3-4.8.9/src/opt/maxres.cpp:432: struct compare_asm {
z3-4.8.9/src/opt/maxres.cpp-433- maxres& mr;
##############################################
z3-4.8.9/src/opt/maxres.cpp-442- void sort_assumptions(expr_ref_vector& _asms) {
z3-4.8.9/src/opt/maxres.cpp:443: compare_asm comp(*this);
z3-4.8.9/src/opt/maxres.cpp-444- exprs asms(_asms.size(), _asms.c_ptr());
##############################################
z3-4.8.9/src/opt/maxres.cpp-698- //
z3-4.8.9/src/opt/maxres.cpp:699: // asm => b_i
z3-4.8.9/src/opt/maxres.cpp:700: // asm => d_{i-1} or b_{i-1}
z3-4.8.9/src/opt/maxres.cpp-701- // d_i => d_{i-1} or b_{i-1}
##############################################
z3-4.8.9/src/opt/wmax.cpp-127-
z3-4.8.9/src/opt/wmax.cpp:128: struct compare_asm {
z3-4.8.9/src/opt/wmax.cpp-129- wmax& max;
##############################################
z3-4.8.9/src/opt/wmax.cpp-141- }
z3-4.8.9/src/opt/wmax.cpp:142: compare_asm comp(*this);
z3-4.8.9/src/opt/wmax.cpp-143- std::sort(_asms.begin(),_asms.end(), comp);
##############################################
z3-4.8.9/src/smt/smt_clause.cpp-49- if (del_eh)
z3-4.8.9/src/smt/smt_clause.cpp:50: *(const_cast<clause_del_eh **>(cls->get_del_eh_addr())) = del_eh;
z3-4.8.9/src/smt/smt_clause.cpp-51- if (js)
z3-4.8.9/src/smt/smt_clause.cpp:52: *(const_cast<justification **>(cls->get_justification_addr())) = js;
z3-4.8.9/src/smt/smt_clause.cpp-53- if (save_atoms) {
##############################################
z3-4.8.9/src/smt/smt_clause.cpp-56- m.inc_ref(atom);
z3-4.8.9/src/smt/smt_clause.cpp:57: const_cast<expr**>(cls->get_atoms_addr())[i] = TAG(expr*, atom, lits[i].sign());
z3-4.8.9/src/smt/smt_clause.cpp-58- }
##############################################
z3-4.8.9/src/smt/smt_clause.cpp-95- m.dec_ref(get_atom(i));
z3-4.8.9/src/smt/smt_clause.cpp:96: const_cast<expr**>(get_atoms_addr())[i] = nullptr;
z3-4.8.9/src/smt/smt_clause.cpp-97- }
##############################################
z3-4.8.9/src/smt/smt_clause.h-86-
z3-4.8.9/src/smt/smt_clause.h:87: unsigned const * get_activity_addr() const {
z3-4.8.9/src/smt/smt_clause.h-88- return reinterpret_cast<unsigned const *>(m_lits + m_capacity);
##############################################
z3-4.8.9/src/smt/smt_clause.h-90-
z3-4.8.9/src/smt/smt_clause.h:91: unsigned * get_activity_addr() {
z3-4.8.9/src/smt/smt_clause.h-92- return reinterpret_cast<unsigned *>(m_lits + m_capacity);
##############################################
z3-4.8.9/src/smt/smt_clause.h-94-
z3-4.8.9/src/smt/smt_clause.h:95: clause_del_eh * const * get_del_eh_addr() const {
z3-4.8.9/src/smt/smt_clause.h:96: unsigned const * addr = get_activity_addr();
z3-4.8.9/src/smt/smt_clause.h-97- if (is_lemma())
##############################################
z3-4.8.9/src/smt/smt_clause.h-107-
z3-4.8.9/src/smt/smt_clause.h:108: justification * const * get_justification_addr() const {
z3-4.8.9/src/smt/smt_clause.h:109: clause_del_eh * const * addr = get_del_eh_addr();
z3-4.8.9/src/smt/smt_clause.h-110- if (m_has_del_eh)
##############################################
z3-4.8.9/src/smt/smt_clause.h-114-
z3-4.8.9/src/smt/smt_clause.h:115: expr * const * get_atoms_addr() const {
z3-4.8.9/src/smt/smt_clause.h:116: justification * const * addr = get_justification_addr();
z3-4.8.9/src/smt/smt_clause.h-117- if (m_has_justification)
##############################################
z3-4.8.9/src/smt/smt_clause.h-146- SASSERT(!is_lemma() || new_js == 0 || !new_js->in_region());
z3-4.8.9/src/smt/smt_clause.h:147: justification ** js_addr = const_cast<justification**>(get_justification_addr());
z3-4.8.9/src/smt/smt_clause.h-148- *js_addr = new_js;
##############################################
z3-4.8.9/src/smt/smt_clause.h-215- SASSERT(is_lemma());
z3-4.8.9/src/smt/smt_clause.h:216: return *(get_activity_addr());
z3-4.8.9/src/smt/smt_clause.h-217- }
##############################################
z3-4.8.9/src/smt/smt_clause.h-220- SASSERT(is_lemma());
z3-4.8.9/src/smt/smt_clause.h:221: *(get_activity_addr()) = act;
z3-4.8.9/src/smt/smt_clause.h-222- }
##############################################
z3-4.8.9/src/smt/smt_clause.h-224- clause_del_eh * get_del_eh() const {
z3-4.8.9/src/smt/smt_clause.h:225: return m_has_del_eh ? *(get_del_eh_addr()) : nullptr;
z3-4.8.9/src/smt/smt_clause.h-226- }
##############################################
z3-4.8.9/src/smt/smt_clause.h-228- justification * get_justification() const {
z3-4.8.9/src/smt/smt_clause.h:229: return m_has_justification ? *(get_justification_addr()) : nullptr;
z3-4.8.9/src/smt/smt_clause.h-230- }
##############################################
z3-4.8.9/src/smt/smt_clause.h-237- SASSERT(idx < get_num_atoms());
z3-4.8.9/src/smt/smt_clause.h:238: return UNTAG(expr*, get_atoms_addr()[idx]);
z3-4.8.9/src/smt/smt_clause.h-239- }
##############################################
z3-4.8.9/src/smt/smt_clause.h-242- SASSERT(idx < get_num_atoms());
z3-4.8.9/src/smt/smt_clause.h:243: return GET_TAG(get_atoms_addr()[idx]) == 1;
z3-4.8.9/src/smt/smt_clause.h-244- }
##############################################
z3-4.8.9/src/smt/smt_clause.h-268- (*del_eh)(m, this);
z3-4.8.9/src/smt/smt_clause.h:269: *(const_cast<clause_del_eh **>(get_del_eh_addr())) = nullptr;
z3-4.8.9/src/smt/smt_clause.h-270- }
##############################################
z3-4.8.9/src/util/hwf.cpp-300-
z3-4.8.9/src/util/hwf.cpp:301: __asm {
z3-4.8.9/src/util/hwf.cpp-302- fld xv
##############################################
z3-4.8.9/.pc/00-intrinsics.patch/src/util/hwf.cpp-300-
z3-4.8.9/.pc/00-intrinsics.patch/src/util/hwf.cpp:301: __asm {
z3-4.8.9/.pc/00-intrinsics.patch/src/util/hwf.cpp-302- fld xv