===========================================================
.___ __ __
_________________ __ __ __| _/|__|/ |_
/ ___\_` __ \__ \ | | \/ __ | | \\_ __\
/ /_/ > | \// __ \| | / /_/ | | || |
\___ /|__| (____ /____/\____ | |__||__|
/_____/ \/ \/
grep rough audit - static analysis tool
v2.8 written by @Wireghoul
=================================[justanotherhacker.com]===
cbmc-5.12/CMakeLists.txt-54-if(DEFINED CMAKE_USE_CUDD)
cbmc-5.12/CMakeLists.txt:55: include("${CMAKE_CURRENT_SOURCE_DIR}/cmake/DownloadProject.cmake")
cbmc-5.12/CMakeLists.txt-56- message(STATUS "Downloading Cudd-3.0.0")
##############################################
cbmc-5.12/doc/architectural/howto.md-42-`cbmc`, `goto-instrument`, and `goto-cc` directories. Add these
cbmc-5.12/doc/architectural/howto.md:43:directories to your `$PATH`:
cbmc-5.12/doc/architectural/howto.md-44-
##############################################
cbmc-5.12/doc/slides/cbmc-latex-beamer/do_figures-5-for a in ${FIG} ; do
cbmc-5.12/doc/slides/cbmc-latex-beamer/do_figures:6: fig2dev -L pdftex $a > `echo $a | sed s/.fig/.pdf/`
cbmc-5.12/doc/slides/cbmc-latex-beamer/do_figures-7-done
##############################################
cbmc-5.12/doc/slides/cbmc-latex-beamer/do_figures-9-for a in ${FIG} ; do
cbmc-5.12/doc/slides/cbmc-latex-beamer/do_figures:10: fig2dev -L pdftex_t -p `echo $a | sed s/.fig/.pdf/` $a > `echo $a | sed s/.fig/.xfigtex/`
cbmc-5.12/doc/slides/cbmc-latex-beamer/do_figures-11-done
##############################################
cbmc-5.12/jbmc/src/java_bytecode/assignments_from_json.h-69-/// possible to rewrite parts of it to set the ordinal depending on the order
cbmc-5.12/jbmc/src/java_bytecode/assignments_from_json.h:70:/// of elements seen in the `$VALUES` array, but it would generally make
cbmc-5.12/jbmc/src/java_bytecode/assignments_from_json.h-71-/// things more complicated.
##############################################
cbmc-5.12/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp-1051-/// the matching parameter.
cbmc-5.12/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp:1052:/// Example: if \p parameter has identifier `java::Outer$Inner::T` and
cbmc-5.12/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp-1053-/// there is a replacement parameter with identifier `java::Outer::T`, the
##############################################
cbmc-5.12/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp-1097-/// `t` of type `Generic<T>`. This function ensures that the parameter points to
cbmc-5.12/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp:1098:/// `java::Outer::T` instead of `java::Outer$Inner::T`.
cbmc-5.12/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp-1099-static void find_and_replace_parameters(
##############################################
cbmc-5.12/jbmc/src/java_bytecode/java_class_loader_limit.cpp-44-/// instruct the driver to load `A.jar` and `B.jar` and the two .class files
cbmc-5.12/jbmc/src/java_bytecode/java_class_loader_limit.cpp:45:/// `jarfile3$A.class` and `jarfile3.class`. All the rest of the .jar files is
cbmc-5.12/jbmc/src/java_bytecode/java_class_loader_limit.cpp-46-/// ignored.
##############################################
cbmc-5.12/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp-972- REQUIRE(parameters.at(0).get_identifier() == "someClass.someMethod::this");
cbmc-5.12/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp:973: REQUIRE(parameters.at(1).get_identifier() == "someClass.someMethod::this$0");
cbmc-5.12/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp-974- REQUIRE(parameters.at(2).get_identifier() == "someClass.someMethod::other");
cbmc-5.12/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp-975- REQUIRE(parameters.at(0).get_base_name() == "this");
cbmc-5.12/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp:976: REQUIRE(parameters.at(1).get_base_name() == "this$0");
cbmc-5.12/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp-977- REQUIRE(parameters.at(2).get_base_name() == "other");
##############################################
cbmc-5.12/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp-1021- symbol_table.lookup_ref(id2string(method_id) + "::this$0");
cbmc-5.12/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp:1022: REQUIRE(inner_symbol.name == id2string(method_id) + "::this$0");
cbmc-5.12/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp:1023: REQUIRE(inner_symbol.base_name == "this$0");
cbmc-5.12/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp-1024- REQUIRE(inner_symbol.type == java_lang_object_type());
##############################################
cbmc-5.12/jbmc/unit/java_bytecode/java_bytecode_parser/parse_class_without_instructions.cpp-50- REQUIRE(method_constructor.local_variable_table[0].name == "this");
cbmc-5.12/jbmc/unit/java_bytecode/java_bytecode_parser/parse_class_without_instructions.cpp:51: REQUIRE(method_constructor.local_variable_table[1].name == "this$0");
cbmc-5.12/jbmc/unit/java_bytecode/java_bytecode_parser/parse_class_without_instructions.cpp-52-}
##############################################
cbmc-5.12/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp-37- {
cbmc-5.12/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp:38: REQUIRE(id2string(class_type->get_name()) == "java::Outer$Inner");
cbmc-5.12/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp-39- }
##############################################
cbmc-5.12/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp-96- {
cbmc-5.12/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp:97: REQUIRE(id2string(class_type->get_name()) == "java::Outer$1");
cbmc-5.12/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp-98- }
##############################################
cbmc-5.12/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp-127- {
cbmc-5.12/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp:128: REQUIRE(id2string(class_type->get_name()) == "java::Outer$RedHerring");
cbmc-5.12/jbmc/unit/java_bytecode/java_bytecode_parser/parse_inner_class.cpp-129- }
##############################################
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-128- const std::string &class_name = gather_full_class_name(descriptor);
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp:129: REQUIRE(class_name == "Outer$Inner");
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-130- }
##############################################
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-137- const std::string &class_name = gather_full_class_name(descriptor);
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp:138: REQUIRE(class_name == "Outer$Inner$Inner2");
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-139- }
##############################################
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-156- const std::string &class_name = gather_full_class_name(signature);
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp:157: REQUIRE(class_name == "ClassName$Inner");
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-158- }
##############################################
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-165- const std::string &class_name = gather_full_class_name(signature);
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp:166: REQUIRE(class_name == "ClassName$Inner");
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-167- }
##############################################
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-174- const std::string &class_name = gather_full_class_name(signature);
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp:175: REQUIRE(class_name == "ClassName$Inner");
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-176- }
##############################################
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-186- const std::string &class_name = gather_full_class_name(signature);
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp:187: REQUIRE(class_name == "ClassName$Inner$Inner2");
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-188- }
##############################################
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-197- const std::string &class_name = gather_full_class_name(signature);
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp:198: REQUIRE(class_name == "ClassName$Inner$Inner2");
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-199- }
##############################################
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-208- const std::string &class_name = gather_full_class_name(signature);
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp:209: REQUIRE(class_name == "ClassName$Inner$Inner2");
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-210- }
##############################################
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-220- const std::string &class_name = gather_full_class_name(signature);
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp:221: REQUIRE(class_name == "ClassName$Inner$Inner2");
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-222- }
##############################################
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-231- const std::string &class_name = gather_full_class_name(signature);
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp:232: REQUIRE(class_name == "ClassName$Inner$Inner2");
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-233- }
##############################################
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-243- const std::string &class_name = gather_full_class_name(signature);
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp:244: REQUIRE(class_name == "ClassName$Inner$Inner2");
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-245- }
##############################################
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-254- const std::string &class_name = gather_full_class_name(signature);
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp:255: REQUIRE(class_name == "ClassName$Inner$Inner2");
cbmc-5.12/jbmc/unit/java_bytecode/java_utils_test.cpp-256- }
##############################################
cbmc-5.12/regression/acceleration/accelerate.sh-2-
cbmc-5.12/regression/acceleration/accelerate.sh:3:bindir=`dirname $0`
cbmc-5.12/regression/acceleration/accelerate.sh-4-goto_cc="$bindir/../../goto-cc/goto-cc"
##############################################
cbmc-5.12/regression/ansi-c/VS_extensions1/main.c-7-
cbmc-5.12/regression/ansi-c/VS_extensions1/main.c:8:void f1() { __asm { mov ax, ax } }
cbmc-5.12/regression/ansi-c/VS_extensions1/main.c-9-
##############################################
cbmc-5.12/regression/ansi-c/asm1/main.c-5-int global asm("rax");
cbmc-5.12/regression/ansi-c/asm1/main.c:6:asm ("nop");
cbmc-5.12/regression/ansi-c/asm1/main.c-7-#endif
##############################################
cbmc-5.12/regression/ansi-c/asm1/main.c-11-// use -fasm-blocks
cbmc-5.12/regression/ansi-c/asm1/main.c:12:asm void test();
cbmc-5.12/regression/ansi-c/asm1/main.c-13-
cbmc-5.12/regression/ansi-c/asm1/main.c-14-// likely to mimic CodeWarrior
cbmc-5.12/regression/ansi-c/asm1/main.c:15:void asm test()
cbmc-5.12/regression/ansi-c/asm1/main.c-16-{
##############################################
cbmc-5.12/regression/ansi-c/asm1/main.c-23- #ifdef __GNUC__
cbmc-5.12/regression/ansi-c/asm1/main.c:24: __asm volatile("mov ax, dx");
cbmc-5.12/regression/ansi-c/asm1/main.c-25-
##############################################
cbmc-5.12/regression/ansi-c/asm1/main.c-28-
cbmc-5.12/regression/ansi-c/asm1/main.c:29: // Apple added "ASM Blocks", similar to MS', to gcc
cbmc-5.12/regression/ansi-c/asm1/main.c:30: __asm {
cbmc-5.12/regression/ansi-c/asm1/main.c-31- mov al, 2
##############################################
cbmc-5.12/regression/ansi-c/asm1/main.c-38- // Microsoft only
cbmc-5.12/regression/ansi-c/asm1/main.c:39: __asm {
cbmc-5.12/regression/ansi-c/asm1/main.c-40- mov al, 2
##############################################
cbmc-5.12/regression/ansi-c/asm1/main.c-45- // alternative syntax:
cbmc-5.12/regression/ansi-c/asm1/main.c:46: __asm mov al, 2
cbmc-5.12/regression/ansi-c/asm1/main.c:47: __asm mov dx, 0xD007
cbmc-5.12/regression/ansi-c/asm1/main.c:48: __asm out dx, al
cbmc-5.12/regression/ansi-c/asm1/main.c-49- #endif
##############################################
cbmc-5.12/regression/ansi-c/asm2/main.c-6- #ifdef __GNUC__
cbmc-5.12/regression/ansi-c/asm2/main.c:7: asm goto ("jc %l[error];"
cbmc-5.12/regression/ansi-c/asm2/main.c-8- : : "r"(x), "r"(&y) : "memory" : error);
##############################################
cbmc-5.12/regression/ansi-c/gcc_builtins5/main.c-41-
cbmc-5.12/regression/ansi-c/gcc_builtins5/main.c:42: asm volatile ("movq %q0,%%fs:%P1" : :
cbmc-5.12/regression/ansi-c/gcc_builtins5/main.c-43- "ir" ((uint64_t) (
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i-7715-{
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i:7716: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i-7717- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i-7731-{
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i:7732: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i-7733- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i-7747-{
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i:7748: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i-7749- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i-12557-{
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i:12558: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i-12559- mov eax, Bit
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i-12637- LONG Barrier;
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i:12638: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i-12639- xchg Barrier, eax
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i-94290-
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i:94291:unsigned long __stdcall inet_addr ( const char * cp);
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i-94292-
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i-94355-
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i:94356:struct hostent * __stdcall gethostbyaddr(
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i-94357- const char * addr,
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i-94435-
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i:94436:HANDLE __stdcall WSAAsyncGetHostByAddr(
cbmc-5.12/regression/ansi-c/windows_h_VS_2005/main.i-94437- HWND hWnd,
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i-10756-{
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i:10757: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i-10758- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i-10772-{
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i:10773: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i-10774- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i-10788-{
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i:10789: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i-10790- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i-15983-{
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i:15984: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i-15985- mov eax, Bit
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i-16133- LONG Barrier;
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i:16134: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i-16135- xchg Barrier, eax
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i-119636-
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i:119637:unsigned long __stdcall inet_addr ( const char * cp);
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i-119638-
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i-119701-
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i:119702:struct hostent * __stdcall gethostbyaddr(
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i-119703- const char * addr,
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i-119781-
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i:119782:HANDLE __stdcall WSAAsyncGetHostByAddr(
cbmc-5.12/regression/ansi-c/windows_h_VS_2008/main.i-119783- HWND hWnd,
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i-12023-{
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i:12024: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i-12025- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i-12039-{
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i:12040: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i-12041- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i-12055-{
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i:12056: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i-12057- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i-17669-{
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i:17670: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i-17671- mov eax, Bit
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i-17817- LONG Barrier;
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i:17818: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i-17819- xchg Barrier, eax
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i-130238-
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i:130239:unsigned long __stdcall inet_addr ( const char * cp);
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i-130240-
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i-130303-
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i:130304:struct hostent * __stdcall gethostbyaddr(
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i-130305- const char * addr,
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i-130383-
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i:130384:HANDLE __stdcall WSAAsyncGetHostByAddr(
cbmc-5.12/regression/ansi-c/windows_h_VS_2010/main.i-130385- HWND hWnd,
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i-13502-{
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i:13503: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i-13504- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i-13518-{
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i:13519: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i-13520- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i-13534-{
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i:13535: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i-13536- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i-20394-{
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i:20395: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i-20396- mov eax, Bit
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i-20543- LONG Barrier;
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i:20544: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i-20545- xchg Barrier, eax
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i-190396-
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i:190397:unsigned long __stdcall inet_addr ( const char * cp);
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i-190398-
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i-190461-
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i:190462:struct hostent * __stdcall gethostbyaddr(
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i-190463- const char * addr,
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i-190541-
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i:190542:HANDLE __stdcall WSAAsyncGetHostByAddr(
cbmc-5.12/regression/ansi-c/windows_h_VS_2012/main.i-190543- HWND hWnd,
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2013/main.i-16135-{
cbmc-5.12/regression/ansi-c/windows_h_VS_2013/main.i:16136: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2013/main.i-16137- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2013/main.i-16151-{
cbmc-5.12/regression/ansi-c/windows_h_VS_2013/main.i:16152: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2013/main.i-16153- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2013/main.i-16167-{
cbmc-5.12/regression/ansi-c/windows_h_VS_2013/main.i:16168: __asm {
cbmc-5.12/regression/ansi-c/windows_h_VS_2013/main.i-16169- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2013/main.i-165418-
cbmc-5.12/regression/ansi-c/windows_h_VS_2013/main.i:165419:unsigned long __stdcall inet_addr ( const char * cp);
cbmc-5.12/regression/ansi-c/windows_h_VS_2013/main.i-165420-
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2013/main.i-165483-
cbmc-5.12/regression/ansi-c/windows_h_VS_2013/main.i:165484:struct hostent * __stdcall gethostbyaddr(
cbmc-5.12/regression/ansi-c/windows_h_VS_2013/main.i-165485- const char * addr,
##############################################
cbmc-5.12/regression/ansi-c/windows_h_VS_2013/main.i-165563-
cbmc-5.12/regression/ansi-c/windows_h_VS_2013/main.i:165564:HANDLE __stdcall WSAAsyncGetHostByAddr(
cbmc-5.12/regression/ansi-c/windows_h_VS_2013/main.i-165565- HWND hWnd,
##############################################
cbmc-5.12/regression/cbmc-library/gethostbyaddr-01/main.c-5-{
cbmc-5.12/regression/cbmc-library/gethostbyaddr-01/main.c:6: gethostbyaddr();
cbmc-5.12/regression/cbmc-library/gethostbyaddr-01/main.c-7- assert(0);
##############################################
cbmc-5.12/regression/cbmc-library/inet_addr-01/main.c-5-{
cbmc-5.12/regression/cbmc-library/inet_addr-01/main.c:6: inet_addr();
cbmc-5.12/regression/cbmc-library/inet_addr-01/main.c-7- assert(0);
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii-7715-{
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii:7716: __asm {
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii-7717- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii-7731-{
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii:7732: __asm {
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii-7733- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii-7747-{
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii:7748: __asm {
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii-7749- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii-12557-{
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii:12558: __asm {
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii-12559- mov eax, Bit
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii-12637- LONG Barrier;
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii:12638: __asm {
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii-12639- xchg Barrier, eax
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii-94290-
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii:94291:unsigned long __stdcall inet_addr ( const char * cp);
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii-94292-
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii-94355-
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii:94356:struct hostent * __stdcall gethostbyaddr(
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii-94357- const char * addr,
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii-94435-
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii:94436:HANDLE __stdcall WSAAsyncGetHostByAddr(
cbmc-5.12/regression/cpp/windows_h_VS_2005/main.ii-94437- HWND hWnd,
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii-10756-{
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii:10757: __asm {
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii-10758- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii-10772-{
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii:10773: __asm {
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii-10774- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii-10788-{
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii:10789: __asm {
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii-10790- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii-15983-{
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii:15984: __asm {
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii-15985- mov eax, Bit
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii-16133- LONG Barrier;
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii:16134: __asm {
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii-16135- xchg Barrier, eax
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii-119636-
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii:119637:unsigned long __stdcall inet_addr ( const char * cp);
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii-119638-
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii-119701-
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii:119702:struct hostent * __stdcall gethostbyaddr(
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii-119703- const char * addr,
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii-119781-
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii:119782:HANDLE __stdcall WSAAsyncGetHostByAddr(
cbmc-5.12/regression/cpp/windows_h_VS_2008/main.ii-119783- HWND hWnd,
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii-12023-{
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii:12024: __asm {
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii-12025- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii-12039-{
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii:12040: __asm {
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii-12041- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii-12055-{
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii:12056: __asm {
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii-12057- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii-17669-{
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii:17670: __asm {
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii-17671- mov eax, Bit
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii-17817- LONG Barrier;
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii:17818: __asm {
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii-17819- xchg Barrier, eax
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii-130238-
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii:130239:unsigned long __stdcall inet_addr ( const char * cp);
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii-130240-
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii-130303-
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii:130304:struct hostent * __stdcall gethostbyaddr(
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii-130305- const char * addr,
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii-130383-
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii:130384:HANDLE __stdcall WSAAsyncGetHostByAddr(
cbmc-5.12/regression/cpp/windows_h_VS_2010/main.ii-130385- HWND hWnd,
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii-13502-{
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii:13503: __asm {
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii-13504- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii-13518-{
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii:13519: __asm {
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii-13520- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii-13534-{
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii:13535: __asm {
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii-13536- mov ecx, ShiftCount
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii-20394-{
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii:20395: __asm {
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii-20396- mov eax, Bit
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii-20543- LONG Barrier;
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii:20544: __asm {
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii-20545- xchg Barrier, eax
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii-190395-
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii:190396:unsigned long __stdcall inet_addr ( const char * cp);
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii-190397-
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii-190460-
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii:190461:struct hostent * __stdcall gethostbyaddr(
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii-190462- const char * addr,
##############################################
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii-190540-
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii:190541:HANDLE __stdcall WSAAsyncGetHostByAddr(
cbmc-5.12/regression/cpp/windows_h_VS_2012/main.ii-190542- HWND hWnd,
##############################################
cbmc-5.12/regression/goto-gcc/dev_null1/main.c-2-{
cbmc-5.12/regression/goto-gcc/dev_null1/main.c:3: asm volatile ( ".if (0 == 0); .error \"asm error\";.endif" );
cbmc-5.12/regression/goto-gcc/dev_null1/main.c-4-}
##############################################
cbmc-5.12/regression/goto-instrument-wmm-core/chain.sh-16- strategy=$2
cbmc-5.12/regression/goto-instrument-wmm-core/chain.sh:17: name=`echo $3 | cut -d. -f1`
cbmc-5.12/regression/goto-instrument-wmm-core/chain.sh-18-elif [ $# -eq 2 ]
##############################################
cbmc-5.12/regression/goto-instrument-wmm-core/chain.sh-21- strategy=
cbmc-5.12/regression/goto-instrument-wmm-core/chain.sh:22: name=`echo $2 | cut -d. -f1`
cbmc-5.12/regression/goto-instrument-wmm-core/chain.sh-23-else
##############################################
cbmc-5.12/regression/goto-instrument/assembly_call_graph_test/main.c-6- // this is Visual Studio syntax
cbmc-5.12/regression/goto-instrument/assembly_call_graph_test/main.c:7: __asm mfence;
cbmc-5.12/regression/goto-instrument/assembly_call_graph_test/main.c-8-#endif
##############################################
cbmc-5.12/regression/k-induction/chain.sh-12-
cbmc-5.12/regression/k-induction/chain.sh:13:name=`echo $2 | cut -d. -f1`
cbmc-5.12/regression/k-induction/chain.sh-14-k=$1
##############################################
cbmc-5.12/regression/test.pl-43- print LOG "Running $cmdline\n";
cbmc-5.12/regression/test.pl:44: system("bash", "-c", "cd '$name' ; $cmdline");
cbmc-5.12/regression/test.pl-45- my $exit_value = $? >> 8;
##############################################
cbmc-5.12/regression/test.pl-60-
cbmc-5.12/regression/test.pl:61: system("bash", "-c", "cd '$name' ; echo '\nEXIT=$exit_value\nSIGNAL=$signal_num\n' >> '$output'");
cbmc-5.12/regression/test.pl-62-
##############################################
cbmc-5.12/scripts/bash-autocomplete/extract_switches.sh-32-#sanity check that there is only one line of output
cbmc-5.12/scripts/bash-autocomplete/extract_switches.sh:33:if [ `echo $cleanstring | wc -l | awk '{print $1}'` -ne 1 ]; then
cbmc-5.12/scripts/bash-autocomplete/extract_switches.sh-34- echo "Problem converting the parameter list to the correct format, I was expecting one line but either got 0 or >2. This is likely to be an error in this conversion script."
##############################################
cbmc-5.12/scripts/benchmark/benchmark_java_project.js-36- if (args[keys[i]])
cbmc-5.12/scripts/benchmark/benchmark_java_project.js:37: result.push(`--${keys[i]}`);
cbmc-5.12/scripts/benchmark/benchmark_java_project.js-38- }
##############################################
cbmc-5.12/scripts/benchmark/benchmark_java_project.js-40- for (let j = 0; j < args[keys[i]].length; j++) {
cbmc-5.12/scripts/benchmark/benchmark_java_project.js:41: result.push(`--${keys[i]}`);
cbmc-5.12/scripts/benchmark/benchmark_java_project.js:42: result.push(`${args[keys[i]][j]}`);
cbmc-5.12/scripts/benchmark/benchmark_java_project.js-43- }
##############################################
cbmc-5.12/scripts/benchmark/benchmark_java_project.js-45- else {
cbmc-5.12/scripts/benchmark/benchmark_java_project.js:46: result.push(`--${keys[i]}`);
cbmc-5.12/scripts/benchmark/benchmark_java_project.js:47: result.push(`${args[keys[i]]}`);
cbmc-5.12/scripts/benchmark/benchmark_java_project.js-48- }
##############################################
cbmc-5.12/scripts/benchmark/benchmark_java_project.js-95- if (typeof modelsPath !== 'undefined')
cbmc-5.12/scripts/benchmark/benchmark_java_project.js:96: config.classpath = `${modelsPath}:${config.classpath}`;
cbmc-5.12/scripts/benchmark/benchmark_java_project.js-97- if (stopAfterSymex) {
##############################################
cbmc-5.12/scripts/cpplint.py-530-# These constants define the current inline assembly state
cbmc-5.12/scripts/cpplint.py:531:_NO_ASM = 0 # Outside of inline assembly block
cbmc-5.12/scripts/cpplint.py:532:_INSIDE_ASM = 1 # Inside inline assembly block
cbmc-5.12/scripts/cpplint.py:533:_END_ASM = 2 # Last line of inline assembly block
cbmc-5.12/scripts/cpplint.py:534:_BLOCK_ASM = 3 # The whole block is an inline assembly block
cbmc-5.12/scripts/cpplint.py-535-
cbmc-5.12/scripts/cpplint.py-536-# Match start of assembly blocks
cbmc-5.12/scripts/cpplint.py:537:_MATCH_ASM = re.compile(r'^\s*(?:asm|_asm|__asm|__asm__)'
cbmc-5.12/scripts/cpplint.py-538- r'(?:\s+(volatile|__volatile__))?'
##############################################
cbmc-5.12/scripts/cpplint.py-2323- self.open_parentheses = 0
cbmc-5.12/scripts/cpplint.py:2324: self.inline_asm = _NO_ASM
cbmc-5.12/scripts/cpplint.py-2325- self.check_namespace_indentation = False
##############################################
cbmc-5.12/scripts/cpplint.py-2577- def InAsmBlock(self):
cbmc-5.12/scripts/cpplint.py:2578: """Check if we are currently one level inside an inline ASM block.
cbmc-5.12/scripts/cpplint.py-2579-
##############################################
cbmc-5.12/scripts/cpplint.py-2582- """
cbmc-5.12/scripts/cpplint.py:2583: return self.stack and self.stack[-1].inline_asm != _NO_ASM
cbmc-5.12/scripts/cpplint.py-2584-
##############################################
cbmc-5.12/scripts/cpplint.py-2732- # Also check if we are starting or ending an inline assembly block.
cbmc-5.12/scripts/cpplint.py:2733: if inner_block.inline_asm in (_NO_ASM, _END_ASM):
cbmc-5.12/scripts/cpplint.py-2734- if (depth_change != 0 and
##############################################
cbmc-5.12/scripts/cpplint.py-2737- # Enter assembly block
cbmc-5.12/scripts/cpplint.py:2738: inner_block.inline_asm = _INSIDE_ASM
cbmc-5.12/scripts/cpplint.py-2739- else:
cbmc-5.12/scripts/cpplint.py-2740- # Not entering assembly block. If previous line was _END_ASM,
cbmc-5.12/scripts/cpplint.py:2741: # we will now shift to _NO_ASM state.
cbmc-5.12/scripts/cpplint.py:2742: inner_block.inline_asm = _NO_ASM
cbmc-5.12/scripts/cpplint.py:2743: elif (inner_block.inline_asm == _INSIDE_ASM and
cbmc-5.12/scripts/cpplint.py-2744- inner_block.open_parentheses == 0):
cbmc-5.12/scripts/cpplint.py-2745- # Exit assembly block
cbmc-5.12/scripts/cpplint.py:2746: inner_block.inline_asm = _END_ASM
cbmc-5.12/scripts/cpplint.py-2747-
##############################################
cbmc-5.12/scripts/cpplint.py-2844- if _MATCH_ASM.match(line):
cbmc-5.12/scripts/cpplint.py:2845: self.stack[-1].inline_asm = _BLOCK_ASM
cbmc-5.12/scripts/cpplint.py-2846-
##############################################
cbmc-5.12/scripts/format_classpath.sh-11-
cbmc-5.12/scripts/format_classpath.sh:12:echo -n `IFS=$separator; echo "$*"`
##############################################
cbmc-5.12/scripts/generate_vcxproj-16- for dir in $dirs ; do
cbmc-5.12/scripts/generate_vcxproj:17: sources="`(cd $dest/src/$dir; make sources)`"
cbmc-5.12/scripts/generate_vcxproj-18- for s in $sources ; do
##############################################
cbmc-5.12/scripts/generate_vcxproj-39- for dir in $dirs ; do
cbmc-5.12/scripts/generate_vcxproj:40: sources="`(cd $dest/src/$dir; make sources)`"
cbmc-5.12/scripts/generate_vcxproj-41- for s in $sources ; do
##############################################
cbmc-5.12/scripts/run_doxygen.sh-12-# Run doxygen and filter warnings
cbmc-5.12/scripts/run_doxygen.sh:13:SCRIPT_FOLDER=`dirname $0`
cbmc-5.12/scripts/run_doxygen.sh-14-cd $SCRIPT_FOLDER/../src
##############################################
cbmc-5.12/scripts/run_lint.sh-2-
cbmc-5.12/scripts/run_lint.sh:3:script_folder=`dirname $0`
cbmc-5.12/scripts/run_lint.sh-4-
##############################################
cbmc-5.12/scripts/travis_lint.sh-4-
cbmc-5.12/scripts/travis_lint.sh:5:script_folder=`dirname $0`
cbmc-5.12/scripts/travis_lint.sh-6-pip install --user unidiff
##############################################
cbmc-5.12/src/ansi-c/ansi_c_convert_type.cpp-276-
cbmc-5.12/src/ansi-c/ansi_c_convert_type.cpp:277: // asm blocks (cf. regression/ansi-c/asm1) - ignore the asm
cbmc-5.12/src/ansi-c/ansi_c_convert_type.cpp-278- if(other.size()==2)
cbmc-5.12/src/ansi-c/ansi_c_convert_type.cpp-279- {
cbmc-5.12/src/ansi-c/ansi_c_convert_type.cpp:280: if(other.front().id()==ID_asm && other.back().id()==ID_empty)
cbmc-5.12/src/ansi-c/ansi_c_convert_type.cpp-281- other.pop_front();
##############################################
cbmc-5.12/src/ansi-c/c_storage_spec.cpp-55- }
cbmc-5.12/src/ansi-c/c_storage_spec.cpp:56: else if(type.id()==ID_asm &&
cbmc-5.12/src/ansi-c/c_storage_spec.cpp-57- type.has_subtype() &&
##############################################
cbmc-5.12/src/ansi-c/c_storage_spec.h-49-
cbmc-5.12/src/ansi-c/c_storage_spec.h:50: // GCC asm labels __asm__("foo") - these change the symbol name
cbmc-5.12/src/ansi-c/c_storage_spec.h-51- irep_idt asm_label;
##############################################
cbmc-5.12/src/ansi-c/c_typecheck_base.cpp-584- error().source_location=symbol.location;
cbmc-5.12/src/ansi-c/c_typecheck_base.cpp:585: error() << "error: replacing asm renaming "
cbmc-5.12/src/ansi-c/c_typecheck_base.cpp-586- << asm_label_map[orig_name] << " by "
##############################################
cbmc-5.12/src/ansi-c/c_typecheck_expr.cpp-792-
cbmc-5.12/src/ansi-c/c_typecheck_expr.cpp:793: // renaming via GCC asm label
cbmc-5.12/src/ansi-c/c_typecheck_expr.cpp-794- asm_label_mapt::const_iterator entry=
##############################################
cbmc-5.12/src/ansi-c/expr2c.cpp-2437- {
cbmc-5.12/src/ansi-c/expr2c.cpp:2438: dest+="__asm {\n";
cbmc-5.12/src/ansi-c/expr2c.cpp-2439- dest+=indent_str(indent);
##############################################
cbmc-5.12/src/ansi-c/gcc_builtin_headers_mem_string.h-58-char* __builtin_dgettext(const char*, const char*);
cbmc-5.12/src/ansi-c/gcc_builtin_headers_mem_string.h:59:void* __builtin_extract_return_addr(void*);
cbmc-5.12/src/ansi-c/gcc_builtin_headers_mem_string.h-60-int __builtin_ffs(int);
##############################################
cbmc-5.12/src/ansi-c/gcc_builtin_headers_mem_string.h-64-void __builtin_free(void*);
cbmc-5.12/src/ansi-c/gcc_builtin_headers_mem_string.h:65:void* __builtin_frob_return_addr(void*);
cbmc-5.12/src/ansi-c/gcc_builtin_headers_mem_string.h-66-char* __builtin_gettext(const char*);
##############################################
cbmc-5.12/src/ansi-c/get-gcc-builtins.sh-16-for f in $builtin_defs ; do
cbmc-5.12/src/ansi-c/get-gcc-builtins.sh:17: [ ! -s `basename $f` ] || continue
cbmc-5.12/src/ansi-c/get-gcc-builtins.sh-18- echo Downloading http://gcc.gnu.org/svn/gcc/trunk/gcc/$f
##############################################
cbmc-5.12/src/ansi-c/get-gcc-builtins.sh-203-for f in $builtin_defs builtins.h i386-builtin-types-expanded.def i386-type-names.def ; do
cbmc-5.12/src/ansi-c/get-gcc-builtins.sh:204: rm `basename $f`
cbmc-5.12/src/ansi-c/get-gcc-builtins.sh-205-done
##############################################
cbmc-5.12/src/ansi-c/get-gcc-builtins.sh-242- if [ $sed_is_gnu_sed -eq 1 ] ; then
cbmc-5.12/src/ansi-c/get-gcc-builtins.sh:243: line=`echo "$line" | sed 's/\<size_t/__CPROVER_size_t/g'`
cbmc-5.12/src/ansi-c/get-gcc-builtins.sh:244: line=`echo "$line" | sed 's/\<complex\>\([^\.]\)/_Complex\1/g'`
cbmc-5.12/src/ansi-c/get-gcc-builtins.sh-245- else
cbmc-5.12/src/ansi-c/get-gcc-builtins.sh:246: line=`echo "$line" | sed 's/[[:<:]]size_t/__CPROVER_size_t/g'`
cbmc-5.12/src/ansi-c/get-gcc-builtins.sh:247: line=`echo "$line" | sed 's/[[:<:]]complex[[:>:]]\([^\.]\)/_Complex\1/g'`
cbmc-5.12/src/ansi-c/get-gcc-builtins.sh-248- fi
##############################################
cbmc-5.12/src/ansi-c/get-gcc-builtins.sh-253-
cbmc-5.12/src/ansi-c/get-gcc-builtins.sh:254: bi=`echo "$line" | cut -f1 -d'(' | sed 's/.* //'`
cbmc-5.12/src/ansi-c/get-gcc-builtins.sh-255-
##############################################
cbmc-5.12/src/ansi-c/library/inet.c-11-
cbmc-5.12/src/ansi-c/library/inet.c:12:in_addr_t inet_addr(const char *cp)
cbmc-5.12/src/ansi-c/library/inet.c-13-{
##############################################
cbmc-5.12/src/ansi-c/library/netdb.c-39-
cbmc-5.12/src/ansi-c/library/netdb.c:40:struct hostent *gethostbyaddr(const void *addr, socklen_t len, int type)
cbmc-5.12/src/ansi-c/library/netdb.c-41-{
##############################################
cbmc-5.12/src/ansi-c/library/unistd.c-136-
cbmc-5.12/src/ansi-c/library/unistd.c:137:// do not include unistd.h as this might trigger GCC asm renaming of
cbmc-5.12/src/ansi-c/library/unistd.c-138-// write to _write; this is covered by the explicit definition of
##############################################
cbmc-5.12/src/ansi-c/library/unistd.c-210-
cbmc-5.12/src/ansi-c/library/unistd.c:211:// do not include unistd.h as this might trigger GCC asm renaming of
cbmc-5.12/src/ansi-c/library/unistd.c-212-// read to _read; this is covered by the explicit definition of _read
##############################################
cbmc-5.12/src/ansi-c/parser.y-150-%token TOK_GCC_DECIMAL128 "_Decimal128"
cbmc-5.12/src/ansi-c/parser.y:151:%token TOK_GCC_ASM "__asm__"
cbmc-5.12/src/ansi-c/parser.y-152-%token TOK_GCC_ASM_PAREN "__asm__ (with parentheses)"
##############################################
cbmc-5.12/src/ansi-c/parser.y-168-%token TOK_GCC_LABEL "__label__"
cbmc-5.12/src/ansi-c/parser.y:169:%token TOK_MSC_ASM "__asm"
cbmc-5.12/src/ansi-c/parser.y-170-%token TOK_MSC_BASED "__based"
##############################################
cbmc-5.12/src/ansi-c/parser.y-1410- | TOK_THREAD_LOCAL { $$=$1; set($$, ID_thread_local); }
cbmc-5.12/src/ansi-c/parser.y:1411: | TOK_GCC_ASM { $$=$1; set($$, ID_asm); }
cbmc-5.12/src/ansi-c/parser.y-1412- | msc_declspec { $$=$1; }
##############################################
cbmc-5.12/src/ansi-c/parser.y-2513-msc_asm_statement:
cbmc-5.12/src/ansi-c/parser.y:2514: TOK_MSC_ASM '{' TOK_ASM_STRING '}'
cbmc-5.12/src/ansi-c/parser.y-2515- { $$=$1;
##############################################
cbmc-5.12/src/ansi-c/parser.y-2519- }
cbmc-5.12/src/ansi-c/parser.y:2520: | TOK_MSC_ASM TOK_ASM_STRING
cbmc-5.12/src/ansi-c/parser.y-2521- { $$=$1;
##############################################
cbmc-5.12/src/ansi-c/parser.y-2584-
cbmc-5.12/src/ansi-c/parser.y:2585:/* asm ( assembler template
cbmc-5.12/src/ansi-c/parser.y-2586- : output operands // optional
##############################################
cbmc-5.12/src/ansi-c/scanner.l-1618- /* The following ugly stuff avoids two-token lookahead in the parser;
cbmc-5.12/src/ansi-c/scanner.l:1619: e.g., asm void f() vs. asm ("xyz") or asm { ... } */
cbmc-5.12/src/ansi-c/scanner.l-1620-<GCC_ASM>{
##############################################
cbmc-5.12/src/assembler/remove_asm.h-25-///
cbmc-5.12/src/assembler/remove_asm.h:26:/// asm volatile (
cbmc-5.12/src/assembler/remove_asm.h-27-/// "mov %1, %0; add $1, %0"
##############################################
cbmc-5.12/src/cbmc/dist-linux-7-VERSION=`./cbmc --version | cut -d " " -f 1`
cbmc-5.12/src/cbmc/dist-linux:8:VERSION_FILE=`echo $VERSION | sed "y/./-/"`
cbmc-5.12/src/cbmc/dist-linux-9-BITS=`getconf LONG_BIT`
##############################################
cbmc-5.12/src/cbmc/dist-macos-11-VERSION=`./cbmc --version | cut -d " " -f 1`
cbmc-5.12/src/cbmc/dist-macos:12:VERSION_FILE=`echo $VERSION | sed "y/./-/"`
cbmc-5.12/src/cbmc/dist-macos-13-BITS=`getconf LONG_BIT`
##############################################
cbmc-5.12/src/cbmc/dist-win-6-VERSION=`./cbmc.exe --version | cut -d " " -f 1`
cbmc-5.12/src/cbmc/dist-win:7:VERSION_FILE=`echo $VERSION | sed "y/./-/"`
cbmc-5.12/src/cbmc/dist-win-8-
##############################################
cbmc-5.12/src/cpp/parse.cpp-1982-/*
cbmc-5.12/src/cpp/parse.cpp:1983: storage.spec : STATIC | EXTERN | AUTO | REGISTER | MUTABLE | ASM |
cbmc-5.12/src/cpp/parse.cpp-1984- THREAD_LOCAL
##############################################
cbmc-5.12/src/cpp/parse.cpp-1994- t==TOK_MUTABLE ||
cbmc-5.12/src/cpp/parse.cpp:1995: t==TOK_GCC_ASM ||
cbmc-5.12/src/cpp/parse.cpp-1996- t==TOK_THREAD_LOCAL)
##############################################
cbmc-5.12/src/cpp/parse.cpp-2079- case TOK_GCC_ASM:
cbmc-5.12/src/cpp/parse.cpp:2080: // asm post-declarator
cbmc-5.12/src/cpp/parse.cpp-2081- // this is stuff like
##############################################
cbmc-5.12/src/cpp/parse.cpp-7170- function.body : compound.statement
cbmc-5.12/src/cpp/parse.cpp:7171: | { asm }
cbmc-5.12/src/cpp/parse.cpp-7172-*/
##############################################
cbmc-5.12/src/cpp/parse.cpp-7898-
cbmc-5.12/src/cpp/parse.cpp:7899: // asm [volatile] ("stuff" [ : ["=S" [(__res)], ... ]]) ;
cbmc-5.12/src/cpp/parse.cpp-7900-
##############################################
cbmc-5.12/src/cpp/parse.cpp-7997-
cbmc-5.12/src/cpp/parse.cpp:7998: // asm "STUFF"
cbmc-5.12/src/cpp/parse.cpp:7999: // asm { "STUFF" }
cbmc-5.12/src/cpp/parse.cpp-8000-
##############################################
cbmc-5.12/src/goto-analyzer/unreachable_instructions.cpp-335- // reachable and unreachable functions; we could also restrict
cbmc-5.12/src/goto-analyzer/unreachable_instructions.cpp:336: // this to macros/asm renaming
cbmc-5.12/src/goto-analyzer/unreachable_instructions.cpp-337- continue;
##############################################
cbmc-5.12/src/goto-cc/dist-linux-5-VERSION=`./goto-cc --version`
cbmc-5.12/src/goto-cc/dist-linux:6:VERSION_FILE=`echo $VERSION | sed "y/./-/"`
cbmc-5.12/src/goto-cc/dist-linux-7-
##############################################
cbmc-5.12/src/goto-cc/dist-win-6-VERSION=`./goto-cc.exe --version`
cbmc-5.12/src/goto-cc/dist-win:7:VERSION_FILE=`echo $VERSION | sed "y/./-/"`
cbmc-5.12/src/goto-cc/dist-win-8-
##############################################
cbmc-5.12/src/goto-cc/gcc_mode.cpp-1011- debug() << "Running " << native_tool_name
cbmc-5.12/src/goto-cc/gcc_mode.cpp:1012: << " to generate native asm output" << eom;
cbmc-5.12/src/goto-cc/gcc_mode.cpp-1013-
##############################################
cbmc-5.12/src/goto-cc/gcc_mode.cpp-1040- debug()
cbmc-5.12/src/goto-cc/gcc_mode.cpp:1041: << "Appending preprocessed sources to generate hybrid asm output"
cbmc-5.12/src/goto-cc/gcc_mode.cpp-1042- << eom;
##############################################
cbmc-5.12/src/goto-diff/scripts/diff-filter.pl-105-
cbmc-5.12/src/goto-diff/scripts/diff-filter.pl:106:`cp -a $old $dir/`;
cbmc-5.12/src/goto-diff/scripts/diff-filter.pl:107:`cp -a $new $dir/`;
cbmc-5.12/src/goto-diff/scripts/diff-filter.pl-108-
##############################################
cbmc-5.12/src/goto-diff/scripts/diff-filter.pl-116- {
cbmc-5.12/src/goto-diff/scripts/diff-filter.pl:117: `sed -i '${l}s/^/$edits{$f}{$l}#/' $f_edit`;
cbmc-5.12/src/goto-diff/scripts/diff-filter.pl-118- }
##############################################
cbmc-5.12/src/goto-diff/scripts/diff-filter.pl-121-
cbmc-5.12/src/goto-diff/scripts/diff-filter.pl:122:my @diff_to_clean=split('\n', `cd $dir && diff -urN $old $new`);
cbmc-5.12/src/goto-diff/scripts/diff-filter.pl-123-my @clean_diff=();
##############################################
cbmc-5.12/src/goto-instrument/wmm/abstract_event.h-28-public:
cbmc-5.12/src/goto-instrument/wmm/abstract_event.h:29: /* for now, both fence functions and asm fences accepted */
cbmc-5.12/src/goto-instrument/wmm/abstract_event.h-30- enum class operationt { Write, Read, Fence, Lwfence, ASMfence };
##############################################
cbmc-5.12/src/goto-instrument/wmm/event_graph.cpp-561-
cbmc-5.12/src/goto-instrument/wmm/event_graph.cpp:562:/// same as is_unsafe, but with ASM fences
cbmc-5.12/src/goto-instrument/wmm/event_graph.cpp-563-bool event_grapht::critical_cyclet::is_unsafe_asm(
##############################################
cbmc-5.12/src/goto-symex/README.md-100-a construct such as
cbmc-5.12/src/goto-symex/README.md:101:`x == &candidate1 ? candidate1 : x == &candidate2 ? candidate2 : x$object`
cbmc-5.12/src/goto-symex/README.md-102-
cbmc-5.12/src/goto-symex/README.md:103:Note the `x$object` fallback candidate, which is known as a *failed symbol* or
cbmc-5.12/src/goto-symex/README.md-104-*failed object*, and represents the unknown object pointed to by `x` when
cbmc-5.12/src/goto-symex/README.md-105-neither of the candidates (`candidate1` and `candidate2` here) matched as
cbmc-5.12/src/goto-symex/README.md:106:expected. This is of course unsound, since `x$object` and `y$object` are always
cbmc-5.12/src/goto-symex/README.md-107-distinct, even if `x` and `y` might actually alias, but at least it ensures
##############################################
cbmc-5.12/src/goto-symex/symex_dereference.cpp-375-/// a. if the `add_failed_symbols` pass has been run then a pointer-typed
cbmc-5.12/src/goto-symex/symex_dereference.cpp:376:/// symbol `x` will have a corresponding failed symbol `x$object`. This
cbmc-5.12/src/goto-symex/symex_dereference.cpp-377-/// is replicated according to L1 renaming on demand, so for example on
cbmc-5.12/src/goto-symex/symex_dereference.cpp-378-/// the first failed dereference of `x!5@10` we will create
cbmc-5.12/src/goto-symex/symex_dereference.cpp:379:/// `x$object!5@10` and add that to the symbol table.
cbmc-5.12/src/goto-symex/symex_dereference.cpp-380-/// This addition is made by
##############################################
cbmc-5.12/src/goto-symex/symex_dereference.cpp-389-/// some legal targets as well this results in an expression like
cbmc-5.12/src/goto-symex/symex_dereference.cpp:390:/// `ptr == &real_obj ? real_obj : ptr$object`.
cbmc-5.12/src/goto-symex/symex_dereference.cpp-391-///
##############################################
cbmc-5.12/src/goto-symex/symex_dereference_state.cpp-26-///
cbmc-5.12/src/goto-symex/symex_dereference_state.cpp:27:/// For example, if \p expr is `p` and it has an `ID_C_failed_symbol` `p$object`
cbmc-5.12/src/goto-symex/symex_dereference_state.cpp-28-/// (the naming convention used by `add_failed_symbols`), and the latest L1
cbmc-5.12/src/goto-symex/symex_dereference_state.cpp:29:/// renaming of `p` is `p!2@4`, then we will create `p$object!2@4` if it doesn't
cbmc-5.12/src/goto-symex/symex_dereference_state.cpp-30-/// already exist.
##############################################
cbmc-5.12/src/solvers/CMakeLists.txt-57-
cbmc-5.12/src/solvers/CMakeLists.txt:58:include("${CBMC_SOURCE_DIR}/../cmake/DownloadProject.cmake")
cbmc-5.12/src/solvers/CMakeLists.txt-59-
##############################################
cbmc-5.12/src/solvers/flattening/bv_pointers.cpp-99- {
cbmc-5.12/src/solvers/flattening/bv_pointers.cpp:100: add_addr(expr, bv);
cbmc-5.12/src/solvers/flattening/bv_pointers.cpp-101- return false;
##############################################
cbmc-5.12/src/solvers/flattening/bv_pointers.cpp-104- {
cbmc-5.12/src/solvers/flattening/bv_pointers.cpp:105: add_addr(expr, bv);
cbmc-5.12/src/solvers/flattening/bv_pointers.cpp-106- return false;
##############################################
cbmc-5.12/src/solvers/flattening/bv_pointers.cpp-192- { // constant
cbmc-5.12/src/solvers/flattening/bv_pointers.cpp:193: add_addr(expr, bv);
cbmc-5.12/src/solvers/flattening/bv_pointers.cpp-194- return false;
##############################################
cbmc-5.12/src/solvers/flattening/bv_pointers.cpp-719-
cbmc-5.12/src/solvers/flattening/bv_pointers.cpp:720:void bv_pointerst::add_addr(const exprt &expr, bvt &bv)
cbmc-5.12/src/solvers/flattening/bv_pointers.cpp-721-{
##############################################
cbmc-5.12/src/solvers/flattening/bv_pointers.h-38-
cbmc-5.12/src/solvers/flattening/bv_pointers.h:39: virtual void add_addr(const exprt &expr, bvt &bv);
cbmc-5.12/src/solvers/flattening/bv_pointers.h-40-
##############################################
cbmc-5.12/src/util/allocate_objects.h-70- ///
cbmc-5.12/src/util/allocate_objects.h:71: /// `alloc_site$1 = ALLOCATE(object_size, FALSE);`
cbmc-5.12/src/util/allocate_objects.h:72: /// `*p = alloc_site$1;`
cbmc-5.12/src/util/allocate_objects.h-73- ///
##############################################
cbmc-5.12/src/util/fresh_symbol.cpp-23-/// \param name_prefix: The new symbol will be named
cbmc-5.12/src/util/fresh_symbol.cpp:24:/// `name_prefix::basename_prefix$num` unless name_prefix is empty, in which
cbmc-5.12/src/util/fresh_symbol.cpp-25-/// case the :: prefix is omitted.
##############################################
cbmc-5.12/src/util/fresh_symbol.cpp-64-/// \param name_prefix: The new symbol will be named
cbmc-5.12/src/util/fresh_symbol.cpp:65:/// `name_prefix::basename_prefix$num` unless name_prefix is empty, in which
cbmc-5.12/src/util/fresh_symbol.cpp-66-/// case the :: prefix is omitted.
##############################################
cbmc-5.12/src/util/std_code.h-1704-
cbmc-5.12/src/util/std_code.h:1705:// to_code_asm only checks the code statement, so no validate_expr is
cbmc-5.12/src/util/std_code.h-1706-// provided for code_asmt
##############################################
cbmc-5.12/unit/catch/catch.hpp-5475- #if defined(__GNUC__) && (defined(__i386) || defined(__x86_64))
cbmc-5.12/unit/catch/catch.hpp:5476: #define CATCH_TRAP() asm volatile ("int $3") /* NOLINT */
cbmc-5.12/unit/catch/catch.hpp-5477- #else // Fall back to the generic way.
##############################################
cbmc-5.12/unit/memory-analyzer/gdb_api.cpp-149-
cbmc-5.12/unit/memory-analyzer/gdb_api.cpp:150: std::regex hex_addr(gdb_api.r_hex_addr);
cbmc-5.12/unit/memory-analyzer/gdb_api.cpp-151-