diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 11e3ee8c531..383ce1de18d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -90,7 +90,7 @@ add_subdirectory(goto-symex) add_subdirectory(jsil) add_subdirectory(json) add_subdirectory(langapi) -add_subdirectory(linking) +add_subdirectory(inking) add_subdirectory(memory-models) add_subdirectory(pointer-analysis) add_subdirectory(solvers) @@ -102,7 +102,7 @@ add_subdirectory(clobber) add_subdirectory(cbmc) add_subdirectory(jbmc) -add_subdirectory(goto-cc) -add_subdirectory(goto-instrument) +add_subdirectory(goto-sea-sea) +add_subdirectory(goto-inkstrument) add_subdirectory(goto-analyzer) add_subdirectory(goto-diff) diff --git a/src/Makefile b/src/Makefile index 82141a0f317..d36f161598e 100644 --- a/src/Makefile +++ b/src/Makefile @@ -1,10 +1,10 @@ -DIRS = ansi-c big-int cbmc jbmc cpp goto-cc goto-instrument goto-programs \ - goto-symex langapi pointer-analysis solvers util linking xmllang \ +DIRS = ansi-c big-int cbmc jbmc cpp goto-sea-sea goto-inkstrument goto-programs \ + goto-symex langapi pointer-analysis solvers util inking xmllang \ assembler analyses java_bytecode \ json goto-analyzer jsil goto-diff clobber \ memory-models miniz -all: cbmc.dir jbmc.dir goto-cc.dir goto-instrument.dir \ +all: cbmc.dir jbmc.dir goto-sea-sea.dir goto-inkstrument.dir \ goto-analyzer.dir goto-diff.dir ############################################################################### @@ -17,7 +17,7 @@ $(patsubst %, %.dir, $(filter-out big-int util, $(DIRS))): util.dir .PHONY: languages .PHONY: clean -cpp.dir: ansi-c.dir linking.dir +cpp.dir: ansi-c.dir inking.dir java_bytecode.dir: miniz.dir @@ -25,24 +25,24 @@ languages: util.dir langapi.dir \ cpp.dir ansi-c.dir xmllang.dir assembler.dir java_bytecode.dir \ jsil.dir -goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \ - goto-symex.dir linking.dir analyses.dir solvers.dir \ +goto-inkstrument.dir: languages goto-programs.dir pointer-analysis.dir \ + goto-symex.dir inking.dir analyses.dir solvers.dir \ json.dir cbmc.dir: languages solvers.dir goto-symex.dir analyses.dir \ - pointer-analysis.dir goto-programs.dir linking.dir \ - goto-instrument.dir + pointer-analysis.dir goto-programs.dir inking.dir \ + goto-inkstrument.dir jbmc.dir: java_bytecode.dir cbmc.dir -goto-analyzer.dir: languages analyses.dir goto-programs.dir linking.dir \ - json.dir goto-instrument.dir +goto-analyzer.dir: languages analyses.dir goto-programs.dir inking.dir \ + json.dir goto-inkstrument.dir goto-diff.dir: languages goto-programs.dir pointer-analysis.dir \ - linking.dir analyses.dir goto-instrument.dir \ + inking.dir analyses.dir goto-inkstrument.dir \ solvers.dir json.dir goto-symex.dir -goto-cc.dir: languages pointer-analysis.dir goto-programs.dir linking.dir +goto-sea-sea.dir: languages pointer-analysis.dir goto-programs.dir inking.dir # building for a particular directory diff --git a/src/ansi-c/CMakeLists.txt b/src/ansi-c/CMakeLists.txt index 43c38d3999f..c1ece608a2c 100644 --- a/src/ansi-c/CMakeLists.txt +++ b/src/ansi-c/CMakeLists.txt @@ -123,4 +123,4 @@ set_source_files_properties( generic_includes(ansi-c) -target_link_libraries(ansi-c util linking goto-programs assembler) +target_link_libraries(ansi-c util inking goto-programs assembler) diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index a632d616fc2..5bbb9f9bd16 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -23,7 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include "c_nondet_symbol_factory.h" diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp index bbb1236e9e7..888df80db88 100644 --- a/src/ansi-c/ansi_c_language.cpp +++ b/src/ansi-c/ansi_c_language.cpp @@ -15,8 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include -#include +#include +#include #include "ansi_c_entry_point.h" #include "ansi_c_typecheck.h" @@ -118,7 +118,7 @@ bool ansi_c_languaget::typecheck( remove_internal_symbols(new_symbol_table); - if(linking(symbol_table, new_symbol_table, get_message_handler())) + if(inking(symbol_table, new_symbol_table, get_message_handler())) return true; return false; diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp index f772a0ea9b7..7cb030bd8e3 100644 --- a/src/ansi-c/c_nondet_symbol_factory.cpp +++ b/src/ansi-c/c_nondet_symbol_factory.cpp @@ -25,7 +25,7 @@ Author: Diffblue Ltd. #include #include -#include +#include #include diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index 1d213aa8f0a..e2469b220ce 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -59,7 +59,7 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol) if(symbol.is_file_local) { // file-local stuff -- stays as is - // collisions are resolved during linking + // collisions are resolved during inking } else if(symbol.is_extern && !is_function) { diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index 5529ab6213b..d005ee0264e 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "c_typecheck_base.h" #include -#include +#include #include "ansi_c_declaration.h" diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp index 6fea7bc9c77..9602a3b7ac9 100644 --- a/src/ansi-c/c_typecheck_initializer.cpp +++ b/src/ansi-c/c_typecheck_initializer.cpp @@ -20,7 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include "anonymous_member.h" diff --git a/src/ansi-c/library/jsa.h b/src/ansi-c/library/jsa.h index 4859e34a927..4031b457526 100644 --- a/src/ansi-c/library/jsa.h +++ b/src/ansi-c/library/jsa.h @@ -391,7 +391,7 @@ __CPROVER_jsa_inline _Bool __CPROVER_jsa__internal_is_in_valid_list( ; #endif -__CPROVER_jsa_inline void __CPROVER_jsa__internal_assume_linking_correct( +__CPROVER_jsa_inline void __CPROVER_jsa__internal_assume_inking_correct( const __CPROVER_jsa_abstract_heapt * const heap, const __CPROVER_jsa_node_id_t node_id, const __CPROVER_jsa_node_id_t prev, @@ -419,7 +419,7 @@ __CPROVER_jsa_inline void __CPROVER_jsa__internal_assume_linking_correct( ; #endif -__CPROVER_jsa_inline void __CPROVER_jsa__internal_assume_valid_iterator_linking( +__CPROVER_jsa_inline void __CPROVER_jsa__internal_assume_valid_iterator_inking( const __CPROVER_jsa_abstract_heapt * const h, const __CPROVER_jsa_list_id_t list, const __CPROVER_jsa_node_id_t node_id, @@ -596,7 +596,7 @@ __CPROVER_jsa_inline void __CPROVER_jsa_assume_valid_heap( __CPROVER_jsa_assume(h->list_head_nodes[node_list] == cnode); __CPROVER_jsa_assume(__CPROVER_jsa__internal_is_valid_node_id(nxt)); __CPROVER_jsa_assume(__CPROVER_jsa__internal_is_valid_node_id(prev)); - __CPROVER_jsa__internal_assume_linking_correct(h, cnode, prev, nxt); + __CPROVER_jsa__internal_assume_inking_correct(h, cnode, prev, nxt); } } #if 0 < __CPROVER_JSA_MAX_ABSTRACT_NODES @@ -610,7 +610,7 @@ __CPROVER_jsa_inline void __CPROVER_jsa_assume_valid_heap( __CPROVER_jsa_assume(__CPROVER_jsa__internal_is_valid_node_id(prev)); const __CPROVER_jsa_id_t nid= __CPROVER_jsa__internal_get_abstract_node_id(anode); - __CPROVER_jsa__internal_assume_linking_correct(h, nid, prev, nxt); + __CPROVER_jsa__internal_assume_inking_correct(h, nid, prev, nxt); } #endif #if 0 < __CPROVER_JSA_MAX_ABSTRACT_RANGES @@ -644,9 +644,9 @@ __CPROVER_jsa_inline void __CPROVER_jsa_assume_valid_heap( else { __CPROVER_jsa_assume(list < h->list_count); - __CPROVER_jsa__internal_assume_valid_iterator_linking( + __CPROVER_jsa__internal_assume_valid_iterator_inking( h, list, next_node, next_index); - __CPROVER_jsa__internal_assume_valid_iterator_linking( + __CPROVER_jsa__internal_assume_valid_iterator_inking( h, list, prev_node, prev_index); if(__CPROVER_jsa_null!=next_node && __CPROVER_jsa_null != prev_node) __CPROVER_jsa__internal_assume_is_neighbour( diff --git a/src/cbmc/CMakeLists.txt b/src/cbmc/CMakeLists.txt index cf0034f5484..4241b23207a 100644 --- a/src/cbmc/CMakeLists.txt +++ b/src/cbmc/CMakeLists.txt @@ -13,13 +13,13 @@ target_link_libraries(cbmc-lib assembler big-int cpp - goto-instrument-lib + goto-inkstrument-lib goto-programs goto-symex java_bytecode json langapi - linking + inking pointer-analysis solvers util diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index c1d88efa6be..f3fe142adbd 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -18,7 +18,7 @@ SRC = all_properties.cpp \ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../cpp/cpp$(LIBEXT) \ ../java_bytecode/java_bytecode$(LIBEXT) \ - ../linking/linking$(LIBEXT) \ + ../inking/inking$(LIBEXT) \ ../big-int/big-int$(LIBEXT) \ ../goto-programs/goto-programs$(LIBEXT) \ ../goto-symex/goto-symex$(LIBEXT) \ @@ -31,19 +31,19 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../pointer-analysis/add_failed_symbols$(OBJEXT) \ ../pointer-analysis/rewrite_index$(OBJEXT) \ ../pointer-analysis/goto_program_dereference$(OBJEXT) \ - ../goto-instrument/reachability_slicer$(OBJEXT) \ - ../goto-instrument/full_slicer$(OBJEXT) \ - ../goto-instrument/nondet_static$(OBJEXT) \ - ../goto-instrument/cover$(OBJEXT) \ - ../goto-instrument/cover_basic_blocks$(OBJEXT) \ - ../goto-instrument/cover_filter$(OBJEXT) \ - ../goto-instrument/cover_instrument_branch$(OBJEXT) \ - ../goto-instrument/cover_instrument_condition$(OBJEXT) \ - ../goto-instrument/cover_instrument_decision$(OBJEXT) \ - ../goto-instrument/cover_instrument_location$(OBJEXT) \ - ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \ - ../goto-instrument/cover_instrument_other$(OBJEXT) \ - ../goto-instrument/cover_util$(OBJEXT) \ + ../goto-inkstrument/reachability_slicer$(OBJEXT) \ + ../goto-inkstrument/full_slicer$(OBJEXT) \ + ../goto-inkstrument/nondet_static$(OBJEXT) \ + ../goto-inkstrument/cover$(OBJEXT) \ + ../goto-inkstrument/cover_basic_blocks$(OBJEXT) \ + ../goto-inkstrument/cover_filter$(OBJEXT) \ + ../goto-inkstrument/cover_instrument_branch$(OBJEXT) \ + ../goto-inkstrument/cover_instrument_condition$(OBJEXT) \ + ../goto-inkstrument/cover_instrument_decision$(OBJEXT) \ + ../goto-inkstrument/cover_instrument_location$(OBJEXT) \ + ../goto-inkstrument/cover_instrument_mcdc$(OBJEXT) \ + ../goto-inkstrument/cover_instrument_other$(OBJEXT) \ + ../goto-inkstrument/cover_util$(OBJEXT) \ ../analyses/analyses$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ ../xmllang/xmllang$(LIBEXT) \ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 100c83c2abf..02e717925c4 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -54,10 +54,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include -#include -#include -#include +#include +#include +#include +#include #include @@ -876,6 +876,34 @@ void cbmc_parse_optionst::help() // clang-format off std::cout << "\n" + " _________ \n" + " _______. _ _ .___/ \ \n" + " / -_ / \ / \ / _ _ | \n" + " | _ _ \ | \/ | / / \/ \ | \n" + " | / \ / \| \ / | |.||.| / \n" + " | |.| |.|| \ / | \_/\_/ / \n" + " \_ \_/ \_// \ / \ ___ _/ \n" + " \ _/ \/ \_\_/ / \n" + " | \_/ ___\| / \n" + " ..____/_.. /.-_/o\____/.. \n" + " .. || o\o \~.o. //~ //..|| \\ .. \n" + " .. |/ .|| \\.. // || ..|| || .. \n" + " .. //o .o\\ || .. // // .. // || . \n" + " .. || .. \o \\ //. // .. || || .. \n" + " .. o// .. \\ ^\// .. // . |/ .\| .. \n" + " .. // .. || /\ .// .. // . \\ .. \n" + " .. |/ .. \| //\| || ../| .. || .. \n" + " o .. o l o //.. .|\ .. \\ .. \n" + " .. |/ .. |/ .. \| .. \n" + " o . o o \n" + " \n" + " ______________ ________ \n" + " / __ | ___ | \/ / __ \ \n" + " | / \| |_/ | . . | / \/ \n" + " | | | ___ | |\/| | | \n" + " | \__/| |_/ | | | | \__/\ \n" + " \____\____/\_| |_/\____/ \n" + " \n" "* * CBMC " CBMC_VERSION " - Copyright (C) 2001-2018 "; std::cout << "(" << (sizeof(void *)*8) << "-bit version)"; diff --git a/src/cbmc/dist-linux b/src/cbmc/dist-linux index e0776f903e7..130bf7c1e83 100755 --- a/src/cbmc/dist-linux +++ b/src/cbmc/dist-linux @@ -12,17 +12,17 @@ DEB_ARCH=`dpkg --print-architecture` echo $VERSION_FILE -(cd ../goto-cc; make; strip goto-cc) -(cd ../goto-instrument; make; strip goto-instrument) +(cd ../goto-sea-sea; make; strip goto-sea-sea) +(cd ../goto-inkstrument; make; strip goto-inkstrument) mkdir /tmp/cbmc-dist -cp ../cbmc/cbmc ../goto-cc/goto-cc \ - ../goto-instrument/goto-instrument /tmp/cbmc-dist/ +cp ../cbmc/cbmc ../goto-sea-sea/goto-sea-sea \ + ../goto-inkstrument/goto-inkstrument /tmp/cbmc-dist/ cp ../../LICENSE /tmp/cbmc-dist/ cp ../../doc/man/cbmc.1 /tmp/cbmc-dist/ cd /tmp/cbmc-dist tar cfz cbmc-${VERSION_FILE}-linux-${BITS}.tgz cbmc \ - goto-cc goto-instrument LICENSE + goto-sea-sea goto-inkstrument LICENSE mkdir debian mkdir debian/DEBIAN @@ -31,7 +31,7 @@ mkdir debian/usr/bin mkdir debian/usr/share mkdir debian/usr/share/man mkdir debian/usr/share/man/man1 -cp cbmc goto-cc goto-instrument \ +cp cbmc goto-sea-sea goto-inkstrument \ debian/usr/bin/ cp cbmc.1 debian/usr/share/man/man1 diff --git a/src/cbmc/dist-macos b/src/cbmc/dist-macos index bbf54cc8c20..06fa95b168e 100755 --- a/src/cbmc/dist-macos +++ b/src/cbmc/dist-macos @@ -5,8 +5,8 @@ umask u=rwx,g=rx,o=rx make cbmc-mac-signed -(cd ../goto-cc; make goto-cc-mac-signed) -(cd ../goto-instrument; make goto-instrument-mac-signed) +(cd ../goto-sea-sea; make goto-sea-sea-mac-signed) +(cd ../goto-inkstrument; make goto-inkstrument-mac-signed) VERSION=`./cbmc --version` VERSION_FILE=`echo $VERSION | sed "y/./-/"` @@ -22,8 +22,8 @@ mkdir /tmp/cbmc-dist/package-root/usr/local/bin mkdir /tmp/cbmc-dist/resources mkdir /tmp/cbmc-dist/resources/en.lproj -cp ../cbmc/cbmc ../goto-cc/goto-cc \ - ../goto-instrument/goto-instrument /tmp/cbmc-dist/package-root/usr/local/bin/ +cp ../cbmc/cbmc ../goto-sea-sea/goto-sea-sea \ + ../goto-inkstrument/goto-inkstrument /tmp/cbmc-dist/package-root/usr/local/bin/ cp ../../LICENSE /tmp/cbmc-dist/resources/license.html cp distribution.xml /tmp/cbmc-dist/ diff --git a/src/cbmc/dist-win b/src/cbmc/dist-win index 2fedef785c5..01b82808642 100755 --- a/src/cbmc/dist-win +++ b/src/cbmc/dist-win @@ -8,19 +8,19 @@ VERSION_FILE=`echo $VERSION | sed "y/./-/"` echo $VERSION_FILE -(cd ../goto-cc; make; strip goto-cc.exe ; cp goto-cc.exe goto-cl.exe) -(cd ../goto-instrument; make; strip goto-instrument.exe) +(cd ../goto-sea-sea; make; strip goto-sea-sea.exe ; cp goto-sea-sea.exe goto-cl.exe) +(cd ../goto-inkstrument; make; strip goto-inkstrument.exe) mkdir /tmp/cbmc-dist cp ../cbmc/cbmc.exe \ - ../goto-cc/goto-cl.exe ../goto-instrument/goto-instrument.exe \ + ../goto-sea-sea/goto-cl.exe ../goto-inkstrument/goto-inkstrument.exe \ /tmp/cbmc-dist/ cp ~/progr/cbmc.vs64/src/cbmc/cbmc.exe /tmp/cbmc-dist/cbmc64.exe cp ../../LICENSE /tmp/cbmc-dist/LICENSE.txt unix2dos /tmp/cbmc-dist/LICENSE.txt cd /tmp/cbmc-dist zip -9 cbmc-${VERSION_FILE}-win.zip cbmc.exe \ - cbmc64.exe goto-instrument.exe goto-cl.exe LICENSE.txt + cbmc64.exe goto-inkstrument.exe goto-cl.exe LICENSE.txt echo Copying. scp cbmc-${VERSION_FILE}-win.zip kroening@dkr-srv.cs.ox.ac.uk:/srv/www/cprover.org/cbmc/download/ diff --git a/src/clobber/CMakeLists.txt b/src/clobber/CMakeLists.txt index 384ae51824e..fabc7d80f82 100644 --- a/src/clobber/CMakeLists.txt +++ b/src/clobber/CMakeLists.txt @@ -10,7 +10,7 @@ generic_includes(clobber-lib) target_link_libraries(clobber-lib ansi-c cpp - linking + inking big-int goto-programs analyses @@ -21,7 +21,7 @@ target_link_libraries(clobber-lib util goto-symex pointer-analysis - goto-instrument-lib + goto-inkstrument-lib ) add_if_library(clobber-lib bv_refinement) diff --git a/src/clobber/Makefile b/src/clobber/Makefile index 74a133782c6..8783d24eccf 100644 --- a/src/clobber/Makefile +++ b/src/clobber/Makefile @@ -4,7 +4,7 @@ SRC = clobber_main.cpp \ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../cpp/cpp$(LIBEXT) \ ../java_bytecode/java_bytecode$(LIBEXT) \ - ../linking/linking$(LIBEXT) \ + ../inking/inking$(LIBEXT) \ ../big-int/big-int$(LIBEXT) \ ../goto-programs/goto-programs$(LIBEXT) \ ../analyses/analyses$(LIBEXT) \ @@ -16,8 +16,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../goto-symex/adjust_float_expressions$(OBJEXT) \ ../goto-symex/rewrite_union$(OBJEXT) \ ../pointer-analysis/dereference$(OBJEXT) \ - ../goto-instrument/dump_c$(OBJEXT) \ - ../goto-instrument/goto_program2code$(OBJEXT) \ + ../goto-inkstrument/dump_c$(OBJEXT) \ + ../goto-inkstrument/goto_program2code$(OBJEXT) \ ../miniz/miniz$(OBJEXT) INCLUDES= -I .. diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index 05d9c3f75f0..8deb2d17288 100644 --- a/src/clobber/clobber_parse_options.cpp +++ b/src/clobber/clobber_parse_options.cpp @@ -32,7 +32,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include diff --git a/src/common b/src/common index fd093cc69af..098a62aeda0 100644 --- a/src/common +++ b/src/common @@ -101,8 +101,8 @@ else ifeq ($(BUILD_ENV_),Cygwin) CXXFLAGS ?= -Wall -O2 CP_CFLAGS = -MMD -MP CP_CXXFLAGS += -MMD -MP -std=c++11 -U__STRICT_ANSI__ - # Cygwin-g++ has problems with statically linking exception code. - # If linking fails, remove -static. + # Cygwin-g++ has problems with statically inking exception code. + # If inking fails, remove -static. LINKFLAGS = -static -std=c++11 LINKLIB = ar rcT $@ $^ LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS) diff --git a/src/config.inc b/src/config.inc index 93b44e39a50..2a39becd5d2 100644 --- a/src/config.inc +++ b/src/config.inc @@ -12,7 +12,7 @@ endif #CXXFLAGS += -O2 -DNDEBUG #CXXFLAGS += -O0 -g -# If GLPK is available; this is used by goto-instrument and musketeer. +# If GLPK is available; this is used by goto-inkstrument and musketeer. #LIB_GLPK = -lglpk # SAT-solvers we have @@ -28,7 +28,7 @@ endif #SMVSAT = # Extra library for SAT solver. This should link to the archive file to be used -# when linking against an IPASIR solver. +# when inking against an IPASIR solver. LIBSOLVER = ifneq ($(PRECOSAT),) diff --git a/src/cpp/cpp_language.cpp b/src/cpp/cpp_language.cpp index e47d887d292..6b701584e5b 100644 --- a/src/cpp/cpp_language.cpp +++ b/src/cpp/cpp_language.cpp @@ -19,7 +19,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include +#include #include #include @@ -131,7 +131,7 @@ bool cpp_languaget::typecheck( cpp_parse_tree, new_symbol_table, module, get_message_handler())) return true; - return linking(symbol_table, new_symbol_table, get_message_handler()); + return inking(symbol_table, new_symbol_table, get_message_handler()); } bool cpp_languaget::generate_support_functions( diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index 549a5b6d77d..c7afd8b51f4 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -17,7 +17,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include +#include #include #include "expr2cpp.h" diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index a6502391c3e..8f675fe6fdb 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -27,7 +27,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include +#include #include "cpp_type2name.h" #include "cpp_convert_type.h" diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp index 565bca8a4bb..b4b1a065793 100644 --- a/src/cpp/cpp_typecheck_initializer.cpp +++ b/src/cpp/cpp_typecheck_initializer.cpp @@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include +#include #include "cpp_util.h" diff --git a/src/goto-analyzer/CMakeLists.txt b/src/goto-analyzer/CMakeLists.txt index 175b1f99ab6..7ae4295ff2a 100644 --- a/src/goto-analyzer/CMakeLists.txt +++ b/src/goto-analyzer/CMakeLists.txt @@ -10,7 +10,7 @@ generic_includes(goto-analyzer-lib) target_link_libraries(goto-analyzer-lib ansi-c cpp - linking + inking big-int goto-programs analyses diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile index 1be5be97dc7..3480e3b4d9c 100644 --- a/src/goto-analyzer/Makefile +++ b/src/goto-analyzer/Makefile @@ -11,7 +11,7 @@ SRC = goto_analyzer_main.cpp \ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../cpp/cpp$(LIBEXT) \ ../java_bytecode/java_bytecode$(LIBEXT) \ - ../linking/linking$(LIBEXT) \ + ../inking/inking$(LIBEXT) \ ../big-int/big-int$(LIBEXT) \ ../goto-programs/goto-programs$(LIBEXT) \ ../analyses/analyses$(LIBEXT) \ diff --git a/src/goto-cc/CMakeLists.txt b/src/goto-cc/CMakeLists.txt deleted file mode 100644 index 8259d960561..00000000000 --- a/src/goto-cc/CMakeLists.txt +++ /dev/null @@ -1,36 +0,0 @@ -# Library -file(GLOB_RECURSE sources "*.cpp" "*.h") -list(REMOVE_ITEM sources - ${CMAKE_CURRENT_SOURCE_DIR}/goto_cc_main.cpp -) -add_library(goto-cc-lib ${sources}) - -generic_includes(goto-cc-lib) - -target_link_libraries(goto-cc-lib - big-int - goto-programs - util - linking - ansi-c - cpp - xml - assembler - langapi -) - -add_if_library(goto-cc-lib java_bytecode) -add_if_library(goto-cc-lib jsil) - -# Executable -add_executable(goto-cc goto_cc_main.cpp) -target_link_libraries(goto-cc goto-cc-lib) - -if(WIN32) - set_target_properties(goto-cc PROPERTIES OUTPUT_NAME goto-cl) -else() - add_custom_command(TARGET goto-cc - POST_BUILD - COMMAND "${CMAKE_COMMAND}" -E create_symlink - goto-cc $/goto-gcc) -endif() diff --git a/src/goto-cc/dist-linux b/src/goto-cc/dist-linux deleted file mode 100644 index b0250f2262c..00000000000 --- a/src/goto-cc/dist-linux +++ /dev/null @@ -1,26 +0,0 @@ -#!/bin/bash -make -strip goto-cc - -VERSION=`./goto-cc --version` -VERSION_FILE=`echo $VERSION | sed "y/./-/"` - -echo $VERSION_FILE - -(cd ../goto-cc; make; strip goto-cc) -(cd ../goto-instrument; make; strip goto-instrument) - -mkdir /tmp/goto-cc-dist -cp goto-cc /tmp/goto-cc-dist/ -cp ../goto-instrument/goto-instrument /tmp/goto-cc-dist/ -cp ../../LICENSE /tmp/goto-cc-dist/ -cp ../../scripts/ls_parse.py /tmp/goto-cc-dist/ -cd /tmp/goto-cc-dist -tar cfz goto-cc-${VERSION_FILE}-linux.tgz goto-cc \ - goto-instrument LICENSE ls_parse.py - -echo Copying. -scp goto-cc-${VERSION_FILE}-linux.tgz kroening@dkr0.inf.ethz.ch:/home/www/cprover.org/goto-cc/download/ - -cd /tmp -rm -R /tmp/goto-cc-dist diff --git a/src/goto-cc/dist-win b/src/goto-cc/dist-win deleted file mode 100644 index b105d8419ba..00000000000 --- a/src/goto-cc/dist-win +++ /dev/null @@ -1,26 +0,0 @@ -#!/bin/bash - -make -strip goto-cc.exe - -VERSION=`./goto-cc.exe --version` -VERSION_FILE=`echo $VERSION | sed "y/./-/"` - -(cd ../goto-cc; make; strip goto-cc.exe) -(cd ../goto-instrument; make; strip goto-instrument.exe) - -echo $VERSION_FILE - -mkdir /tmp/goto-cc-dist -cp goto-cc.exe /tmp/goto-cc-dist/ -cp ../goto-instrument/goto-instrument.exe /tmp/goto-cc-dist/ -cp ../../LICENSE /tmp/goto-cc-dist/ -cd /tmp/goto-cc-dist -zip -9 goto-cc-${VERSION_FILE}-win.zip goto-cc.exe \ - goto-instrument.exe LICENSE - -echo Copying. -scp goto-cc-${VERSION_FILE}-win.zip kroening@dkr0.inf.ethz.ch:/home/www/cprover.org/goto-cc/download/ - -cd /tmp -rm -R /tmp/goto-cc-dist diff --git a/src/goto-diff/CMakeLists.txt b/src/goto-diff/CMakeLists.txt index 2839634244c..5fbe16f2f44 100644 --- a/src/goto-diff/CMakeLists.txt +++ b/src/goto-diff/CMakeLists.txt @@ -10,10 +10,10 @@ generic_includes(goto-diff-lib) target_link_libraries(goto-diff-lib ansi-c cpp - linking + inking big-int pointer-analysis - goto-instrument-lib + goto-inkstrument-lib goto-programs assembler analyses diff --git a/src/goto-diff/Makefile b/src/goto-diff/Makefile index 22304c2a5b7..76bfd1e6777 100644 --- a/src/goto-diff/Makefile +++ b/src/goto-diff/Makefile @@ -10,21 +10,21 @@ SRC = change_impact.cpp \ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../cpp/cpp$(LIBEXT) \ ../java_bytecode/java_bytecode$(LIBEXT) \ - ../linking/linking$(LIBEXT) \ + ../inking/inking$(LIBEXT) \ ../big-int/big-int$(LIBEXT) \ ../goto-programs/goto-programs$(LIBEXT) \ ../assembler/assembler$(LIBEXT) \ ../pointer-analysis/pointer-analysis$(LIBEXT) \ - ../goto-instrument/cover$(OBJEXT) \ - ../goto-instrument/cover_basic_blocks$(OBJEXT) \ - ../goto-instrument/cover_filter$(OBJEXT) \ - ../goto-instrument/cover_instrument_branch$(OBJEXT) \ - ../goto-instrument/cover_instrument_condition$(OBJEXT) \ - ../goto-instrument/cover_instrument_decision$(OBJEXT) \ - ../goto-instrument/cover_instrument_location$(OBJEXT) \ - ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \ - ../goto-instrument/cover_instrument_other$(OBJEXT) \ - ../goto-instrument/cover_util$(OBJEXT) \ + ../goto-inkstrument/cover$(OBJEXT) \ + ../goto-inkstrument/cover_basic_blocks$(OBJEXT) \ + ../goto-inkstrument/cover_filter$(OBJEXT) \ + ../goto-inkstrument/cover_instrument_branch$(OBJEXT) \ + ../goto-inkstrument/cover_instrument_condition$(OBJEXT) \ + ../goto-inkstrument/cover_instrument_decision$(OBJEXT) \ + ../goto-inkstrument/cover_instrument_location$(OBJEXT) \ + ../goto-inkstrument/cover_instrument_mcdc$(OBJEXT) \ + ../goto-inkstrument/cover_instrument_other$(OBJEXT) \ + ../goto-inkstrument/cover_util$(OBJEXT) \ ../goto-symex/adjust_float_expressions$(OBJEXT) \ ../goto-symex/rewrite_union$(OBJEXT) \ ../analyses/analyses$(LIBEXT) \ diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 232ebf029b3..9eaadaeb21e 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -49,7 +49,7 @@ Author: Peter Schrammel #include #include -#include +#include #include diff --git a/src/goto-instrument/CMakeLists.txt b/src/goto-inkstrument/CMakeLists.txt similarity index 53% rename from src/goto-instrument/CMakeLists.txt rename to src/goto-inkstrument/CMakeLists.txt index 95c707aaa76..8db6bef983b 100644 --- a/src/goto-instrument/CMakeLists.txt +++ b/src/goto-inkstrument/CMakeLists.txt @@ -6,14 +6,14 @@ list(REMOVE_ITEM sources # This doesn't build ${CMAKE_CURRENT_SOURCE_DIR}/accelerate/linearize.cpp ) -add_library(goto-instrument-lib ${sources}) +add_library(goto-inkstrument-lib ${sources}) -generic_includes(goto-instrument-lib) +generic_includes(goto-inkstrument-lib) -target_link_libraries(goto-instrument-lib +target_link_libraries(goto-inkstrument-lib ansi-c cpp - linking + inking big-int goto-programs goto-symex @@ -27,9 +27,9 @@ target_link_libraries(goto-instrument-lib solvers ) -add_if_library(goto-instrument-lib java_bytecode) -add_if_library(goto-instrument-lib glpk) +add_if_library(goto-inkstrument-lib java_bytecode) +add_if_library(goto-inkstrument-lib glpk) # Executable -add_executable(goto-instrument goto_instrument_main.cpp) -target_link_libraries(goto-instrument goto-instrument-lib) +add_executable(goto-inkstrument goto_instrument_main.cpp) +target_link_libraries(goto-inkstrument goto-inkstrument-lib) diff --git a/src/goto-instrument/Makefile b/src/goto-inkstrument/Makefile similarity index 89% rename from src/goto-instrument/Makefile rename to src/goto-inkstrument/Makefile index 9fe42bddd18..0ac95c29153 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-inkstrument/Makefile @@ -76,7 +76,7 @@ SRC = accelerate/accelerate.cpp \ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../cpp/cpp$(LIBEXT) \ ../java_bytecode/java_bytecode$(LIBEXT) \ - ../linking/linking$(LIBEXT) \ + ../inking/inking$(LIBEXT) \ ../big-int/big-int$(LIBEXT) \ ../goto-programs/goto-programs$(LIBEXT) \ ../goto-symex/goto-symex$(LIBEXT) \ @@ -94,12 +94,12 @@ INCLUDES= -I .. LIBS = -CLEANFILES = goto-instrument$(EXEEXT) goto-instrument$(LIBEXT) +CLEANFILES = goto-inkstrument$(EXEEXT) goto-inkstrument$(LIBEXT) include ../config.inc include ../common -all: goto-instrument$(EXEEXT) goto-instrument$(LIBEXT) +all: goto-inkstrument$(EXEEXT) goto-inkstrument$(LIBEXT) ifneq ($(LIB_GLPK),) LIBS += $(LIB_GLPK) @@ -108,13 +108,13 @@ endif ############################################################################### -goto-instrument$(EXEEXT): $(OBJ) +goto-inkstrument$(EXEEXT): $(OBJ) $(LINKBIN) -goto-instrument$(LIBEXT): $(OBJ) +goto-inkstrument$(LIBEXT): $(OBJ) $(LINKLIB) -.PHONY: goto-instrument-mac-signed +.PHONY: goto-inkstrument-mac-signed -goto-instrument-mac-signed: goto-instrument$(EXEEXT) - codesign -v -s $(OSX_IDENTITY) goto-instrument$(EXEEXT) +goto-inkstrument-mac-signed: goto-inkstrument$(EXEEXT) + codesign -v -s $(OSX_IDENTITY) goto-inkstrument$(EXEEXT) diff --git a/src/goto-instrument/README.md b/src/goto-inkstrument/README.md similarity index 67% rename from src/goto-instrument/README.md rename to src/goto-inkstrument/README.md index 5be917235ba..ebc6aebf1da 100644 --- a/src/goto-instrument/README.md +++ b/src/goto-inkstrument/README.md @@ -1,13 +1,13 @@ \ingroup module_hidden -\defgroup goto-instrument goto-instrument +\defgroup goto-inkstrument goto-inkstrument -# Folder goto-instrument +# Folder goto-inkstrument \author Martin Brain -The `goto-instrument/` directory contains a number of tools, one per -file, that are built into the `goto-instrument` program. All of them -take in a goto-program (produced by `goto-cc`) and either modify it or +The `goto-inkstrument/` directory contains a number of tools, one per +file, that are built into the `goto-inkstrument` program. All of them +take in a goto-program (produced by `goto-sea-sea`) and either modify it or perform some analysis. Examples include `nondet_static.cpp` which initialises static variables to a non-deterministic value, `nondet_volatile.cpp` which assigns a non-deterministic value to any @@ -15,13 +15,13 @@ volatile variable before it is read and `weak_memory.h` which performs the necessary transformations to reason about weak memory models. The exception to the “one file for each piece of functionality” rule are the program instrumentation options (mostly those given as “Safety checks” -in the `goto-instrument` help text) which are included in the +in the `goto-inkstrument` help text) which are included in the `goto-program/` directory. An example of this is `goto-program/stack_depth.h` and the general rule seems to be that transformations and instrumentation that `cbmc` uses should be in -`goto-program/`, others should be in `goto-instrument`. +`goto-program/`, others should be in `goto-inkstrument`. -`goto-instrument` is a very good template for new analysis tools. New +`goto-inkstrument` is a very good template for new analysis tools. New developers are advised to copy the directory, remove all files apart from `main.*`, `parseoptions.*` and the `Makefile` and use these as the skeleton of their application. The `doit()` method in `parseoptions.cpp` diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-inkstrument/accelerate/accelerate.cpp similarity index 100% rename from src/goto-instrument/accelerate/accelerate.cpp rename to src/goto-inkstrument/accelerate/accelerate.cpp diff --git a/src/goto-instrument/accelerate/accelerate.h b/src/goto-inkstrument/accelerate/accelerate.h similarity index 100% rename from src/goto-instrument/accelerate/accelerate.h rename to src/goto-inkstrument/accelerate/accelerate.h diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-inkstrument/accelerate/acceleration_utils.cpp similarity index 100% rename from src/goto-instrument/accelerate/acceleration_utils.cpp rename to src/goto-inkstrument/accelerate/acceleration_utils.cpp diff --git a/src/goto-instrument/accelerate/acceleration_utils.h b/src/goto-inkstrument/accelerate/acceleration_utils.h similarity index 100% rename from src/goto-instrument/accelerate/acceleration_utils.h rename to src/goto-inkstrument/accelerate/acceleration_utils.h diff --git a/src/goto-instrument/accelerate/accelerator.h b/src/goto-inkstrument/accelerate/accelerator.h similarity index 100% rename from src/goto-instrument/accelerate/accelerator.h rename to src/goto-inkstrument/accelerate/accelerator.h diff --git a/src/goto-instrument/accelerate/all_paths_enumerator.cpp b/src/goto-inkstrument/accelerate/all_paths_enumerator.cpp similarity index 100% rename from src/goto-instrument/accelerate/all_paths_enumerator.cpp rename to src/goto-inkstrument/accelerate/all_paths_enumerator.cpp diff --git a/src/goto-instrument/accelerate/all_paths_enumerator.h b/src/goto-inkstrument/accelerate/all_paths_enumerator.h similarity index 100% rename from src/goto-instrument/accelerate/all_paths_enumerator.h rename to src/goto-inkstrument/accelerate/all_paths_enumerator.h diff --git a/src/goto-instrument/accelerate/cone_of_influence.cpp b/src/goto-inkstrument/accelerate/cone_of_influence.cpp similarity index 100% rename from src/goto-instrument/accelerate/cone_of_influence.cpp rename to src/goto-inkstrument/accelerate/cone_of_influence.cpp diff --git a/src/goto-instrument/accelerate/cone_of_influence.h b/src/goto-inkstrument/accelerate/cone_of_influence.h similarity index 100% rename from src/goto-instrument/accelerate/cone_of_influence.h rename to src/goto-inkstrument/accelerate/cone_of_influence.h diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-inkstrument/accelerate/disjunctive_polynomial_acceleration.cpp similarity index 100% rename from src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp rename to src/goto-inkstrument/accelerate/disjunctive_polynomial_acceleration.cpp diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.h b/src/goto-inkstrument/accelerate/disjunctive_polynomial_acceleration.h similarity index 100% rename from src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.h rename to src/goto-inkstrument/accelerate/disjunctive_polynomial_acceleration.h diff --git a/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp b/src/goto-inkstrument/accelerate/enumerating_loop_acceleration.cpp similarity index 100% rename from src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp rename to src/goto-inkstrument/accelerate/enumerating_loop_acceleration.cpp diff --git a/src/goto-instrument/accelerate/enumerating_loop_acceleration.h b/src/goto-inkstrument/accelerate/enumerating_loop_acceleration.h similarity index 100% rename from src/goto-instrument/accelerate/enumerating_loop_acceleration.h rename to src/goto-inkstrument/accelerate/enumerating_loop_acceleration.h diff --git a/src/goto-instrument/accelerate/loop_acceleration.h b/src/goto-inkstrument/accelerate/loop_acceleration.h similarity index 100% rename from src/goto-instrument/accelerate/loop_acceleration.h rename to src/goto-inkstrument/accelerate/loop_acceleration.h diff --git a/src/goto-instrument/accelerate/overflow_instrumenter.cpp b/src/goto-inkstrument/accelerate/overflow_instrumenter.cpp similarity index 100% rename from src/goto-instrument/accelerate/overflow_instrumenter.cpp rename to src/goto-inkstrument/accelerate/overflow_instrumenter.cpp diff --git a/src/goto-instrument/accelerate/overflow_instrumenter.h b/src/goto-inkstrument/accelerate/overflow_instrumenter.h similarity index 100% rename from src/goto-instrument/accelerate/overflow_instrumenter.h rename to src/goto-inkstrument/accelerate/overflow_instrumenter.h diff --git a/src/goto-instrument/accelerate/path.cpp b/src/goto-inkstrument/accelerate/path.cpp similarity index 100% rename from src/goto-instrument/accelerate/path.cpp rename to src/goto-inkstrument/accelerate/path.cpp diff --git a/src/goto-instrument/accelerate/path.h b/src/goto-inkstrument/accelerate/path.h similarity index 100% rename from src/goto-instrument/accelerate/path.h rename to src/goto-inkstrument/accelerate/path.h diff --git a/src/goto-instrument/accelerate/path_acceleration.h b/src/goto-inkstrument/accelerate/path_acceleration.h similarity index 100% rename from src/goto-instrument/accelerate/path_acceleration.h rename to src/goto-inkstrument/accelerate/path_acceleration.h diff --git a/src/goto-instrument/accelerate/path_enumerator.h b/src/goto-inkstrument/accelerate/path_enumerator.h similarity index 100% rename from src/goto-instrument/accelerate/path_enumerator.h rename to src/goto-inkstrument/accelerate/path_enumerator.h diff --git a/src/goto-instrument/accelerate/polynomial.cpp b/src/goto-inkstrument/accelerate/polynomial.cpp similarity index 100% rename from src/goto-instrument/accelerate/polynomial.cpp rename to src/goto-inkstrument/accelerate/polynomial.cpp diff --git a/src/goto-instrument/accelerate/polynomial.h b/src/goto-inkstrument/accelerate/polynomial.h similarity index 100% rename from src/goto-instrument/accelerate/polynomial.h rename to src/goto-inkstrument/accelerate/polynomial.h diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-inkstrument/accelerate/polynomial_accelerator.cpp similarity index 100% rename from src/goto-instrument/accelerate/polynomial_accelerator.cpp rename to src/goto-inkstrument/accelerate/polynomial_accelerator.cpp diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.h b/src/goto-inkstrument/accelerate/polynomial_accelerator.h similarity index 100% rename from src/goto-instrument/accelerate/polynomial_accelerator.h rename to src/goto-inkstrument/accelerate/polynomial_accelerator.h diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.cpp b/src/goto-inkstrument/accelerate/sat_path_enumerator.cpp similarity index 100% rename from src/goto-instrument/accelerate/sat_path_enumerator.cpp rename to src/goto-inkstrument/accelerate/sat_path_enumerator.cpp diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.h b/src/goto-inkstrument/accelerate/sat_path_enumerator.h similarity index 100% rename from src/goto-instrument/accelerate/sat_path_enumerator.h rename to src/goto-inkstrument/accelerate/sat_path_enumerator.h diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-inkstrument/accelerate/scratch_program.cpp similarity index 100% rename from src/goto-instrument/accelerate/scratch_program.cpp rename to src/goto-inkstrument/accelerate/scratch_program.cpp diff --git a/src/goto-instrument/accelerate/scratch_program.h b/src/goto-inkstrument/accelerate/scratch_program.h similarity index 100% rename from src/goto-instrument/accelerate/scratch_program.h rename to src/goto-inkstrument/accelerate/scratch_program.h diff --git a/src/goto-instrument/accelerate/subsumed.h b/src/goto-inkstrument/accelerate/subsumed.h similarity index 100% rename from src/goto-instrument/accelerate/subsumed.h rename to src/goto-inkstrument/accelerate/subsumed.h diff --git a/src/goto-instrument/accelerate/trace_automaton.cpp b/src/goto-inkstrument/accelerate/trace_automaton.cpp similarity index 100% rename from src/goto-instrument/accelerate/trace_automaton.cpp rename to src/goto-inkstrument/accelerate/trace_automaton.cpp diff --git a/src/goto-instrument/accelerate/trace_automaton.h b/src/goto-inkstrument/accelerate/trace_automaton.h similarity index 100% rename from src/goto-instrument/accelerate/trace_automaton.h rename to src/goto-inkstrument/accelerate/trace_automaton.h diff --git a/src/goto-instrument/accelerate/util.cpp b/src/goto-inkstrument/accelerate/util.cpp similarity index 100% rename from src/goto-instrument/accelerate/util.cpp rename to src/goto-inkstrument/accelerate/util.cpp diff --git a/src/goto-instrument/accelerate/util.h b/src/goto-inkstrument/accelerate/util.h similarity index 100% rename from src/goto-instrument/accelerate/util.h rename to src/goto-inkstrument/accelerate/util.h diff --git a/src/goto-instrument/alignment_checks.cpp b/src/goto-inkstrument/alignment_checks.cpp similarity index 100% rename from src/goto-instrument/alignment_checks.cpp rename to src/goto-inkstrument/alignment_checks.cpp diff --git a/src/goto-instrument/alignment_checks.h b/src/goto-inkstrument/alignment_checks.h similarity index 100% rename from src/goto-instrument/alignment_checks.h rename to src/goto-inkstrument/alignment_checks.h diff --git a/src/goto-instrument/branch.cpp b/src/goto-inkstrument/branch.cpp similarity index 100% rename from src/goto-instrument/branch.cpp rename to src/goto-inkstrument/branch.cpp diff --git a/src/goto-instrument/branch.h b/src/goto-inkstrument/branch.h similarity index 100% rename from src/goto-instrument/branch.h rename to src/goto-inkstrument/branch.h diff --git a/src/goto-instrument/call_sequences.cpp b/src/goto-inkstrument/call_sequences.cpp similarity index 100% rename from src/goto-instrument/call_sequences.cpp rename to src/goto-inkstrument/call_sequences.cpp diff --git a/src/goto-instrument/call_sequences.h b/src/goto-inkstrument/call_sequences.h similarity index 100% rename from src/goto-instrument/call_sequences.h rename to src/goto-inkstrument/call_sequences.h diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-inkstrument/code_contracts.cpp similarity index 100% rename from src/goto-instrument/code_contracts.cpp rename to src/goto-inkstrument/code_contracts.cpp diff --git a/src/goto-instrument/code_contracts.h b/src/goto-inkstrument/code_contracts.h similarity index 100% rename from src/goto-instrument/code_contracts.h rename to src/goto-inkstrument/code_contracts.h diff --git a/src/goto-instrument/concurrency.cpp b/src/goto-inkstrument/concurrency.cpp similarity index 100% rename from src/goto-instrument/concurrency.cpp rename to src/goto-inkstrument/concurrency.cpp diff --git a/src/goto-instrument/concurrency.h b/src/goto-inkstrument/concurrency.h similarity index 100% rename from src/goto-instrument/concurrency.h rename to src/goto-inkstrument/concurrency.h diff --git a/src/goto-instrument/count_eloc.cpp b/src/goto-inkstrument/count_eloc.cpp similarity index 100% rename from src/goto-instrument/count_eloc.cpp rename to src/goto-inkstrument/count_eloc.cpp diff --git a/src/goto-instrument/count_eloc.h b/src/goto-inkstrument/count_eloc.h similarity index 100% rename from src/goto-instrument/count_eloc.h rename to src/goto-inkstrument/count_eloc.h diff --git a/src/goto-instrument/cover.cpp b/src/goto-inkstrument/cover.cpp similarity index 100% rename from src/goto-instrument/cover.cpp rename to src/goto-inkstrument/cover.cpp diff --git a/src/goto-instrument/cover.h b/src/goto-inkstrument/cover.h similarity index 100% rename from src/goto-instrument/cover.h rename to src/goto-inkstrument/cover.h diff --git a/src/goto-instrument/cover_basic_blocks.cpp b/src/goto-inkstrument/cover_basic_blocks.cpp similarity index 100% rename from src/goto-instrument/cover_basic_blocks.cpp rename to src/goto-inkstrument/cover_basic_blocks.cpp diff --git a/src/goto-instrument/cover_basic_blocks.h b/src/goto-inkstrument/cover_basic_blocks.h similarity index 100% rename from src/goto-instrument/cover_basic_blocks.h rename to src/goto-inkstrument/cover_basic_blocks.h diff --git a/src/goto-instrument/cover_filter.cpp b/src/goto-inkstrument/cover_filter.cpp similarity index 100% rename from src/goto-instrument/cover_filter.cpp rename to src/goto-inkstrument/cover_filter.cpp diff --git a/src/goto-instrument/cover_filter.h b/src/goto-inkstrument/cover_filter.h similarity index 100% rename from src/goto-instrument/cover_filter.h rename to src/goto-inkstrument/cover_filter.h diff --git a/src/goto-instrument/cover_instrument.h b/src/goto-inkstrument/cover_instrument.h similarity index 100% rename from src/goto-instrument/cover_instrument.h rename to src/goto-inkstrument/cover_instrument.h diff --git a/src/goto-instrument/cover_instrument_branch.cpp b/src/goto-inkstrument/cover_instrument_branch.cpp similarity index 100% rename from src/goto-instrument/cover_instrument_branch.cpp rename to src/goto-inkstrument/cover_instrument_branch.cpp diff --git a/src/goto-instrument/cover_instrument_condition.cpp b/src/goto-inkstrument/cover_instrument_condition.cpp similarity index 100% rename from src/goto-instrument/cover_instrument_condition.cpp rename to src/goto-inkstrument/cover_instrument_condition.cpp diff --git a/src/goto-instrument/cover_instrument_decision.cpp b/src/goto-inkstrument/cover_instrument_decision.cpp similarity index 100% rename from src/goto-instrument/cover_instrument_decision.cpp rename to src/goto-inkstrument/cover_instrument_decision.cpp diff --git a/src/goto-instrument/cover_instrument_location.cpp b/src/goto-inkstrument/cover_instrument_location.cpp similarity index 100% rename from src/goto-instrument/cover_instrument_location.cpp rename to src/goto-inkstrument/cover_instrument_location.cpp diff --git a/src/goto-instrument/cover_instrument_mcdc.cpp b/src/goto-inkstrument/cover_instrument_mcdc.cpp similarity index 100% rename from src/goto-instrument/cover_instrument_mcdc.cpp rename to src/goto-inkstrument/cover_instrument_mcdc.cpp diff --git a/src/goto-instrument/cover_instrument_other.cpp b/src/goto-inkstrument/cover_instrument_other.cpp similarity index 100% rename from src/goto-instrument/cover_instrument_other.cpp rename to src/goto-inkstrument/cover_instrument_other.cpp diff --git a/src/goto-instrument/cover_util.cpp b/src/goto-inkstrument/cover_util.cpp similarity index 100% rename from src/goto-instrument/cover_util.cpp rename to src/goto-inkstrument/cover_util.cpp diff --git a/src/goto-instrument/cover_util.h b/src/goto-inkstrument/cover_util.h similarity index 100% rename from src/goto-instrument/cover_util.h rename to src/goto-inkstrument/cover_util.h diff --git a/src/goto-instrument/document_properties.cpp b/src/goto-inkstrument/document_properties.cpp similarity index 100% rename from src/goto-instrument/document_properties.cpp rename to src/goto-inkstrument/document_properties.cpp diff --git a/src/goto-instrument/document_properties.h b/src/goto-inkstrument/document_properties.h similarity index 100% rename from src/goto-instrument/document_properties.h rename to src/goto-inkstrument/document_properties.h diff --git a/src/goto-instrument/dot.cpp b/src/goto-inkstrument/dot.cpp similarity index 100% rename from src/goto-instrument/dot.cpp rename to src/goto-inkstrument/dot.cpp diff --git a/src/goto-instrument/dot.h b/src/goto-inkstrument/dot.h similarity index 100% rename from src/goto-instrument/dot.h rename to src/goto-inkstrument/dot.h diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-inkstrument/dump_c.cpp similarity index 100% rename from src/goto-instrument/dump_c.cpp rename to src/goto-inkstrument/dump_c.cpp diff --git a/src/goto-instrument/dump_c.h b/src/goto-inkstrument/dump_c.h similarity index 100% rename from src/goto-instrument/dump_c.h rename to src/goto-inkstrument/dump_c.h diff --git a/src/goto-instrument/dump_c_class.h b/src/goto-inkstrument/dump_c_class.h similarity index 100% rename from src/goto-instrument/dump_c_class.h rename to src/goto-inkstrument/dump_c_class.h diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-inkstrument/full_slicer.cpp similarity index 100% rename from src/goto-instrument/full_slicer.cpp rename to src/goto-inkstrument/full_slicer.cpp diff --git a/src/goto-instrument/full_slicer.h b/src/goto-inkstrument/full_slicer.h similarity index 100% rename from src/goto-instrument/full_slicer.h rename to src/goto-inkstrument/full_slicer.h diff --git a/src/goto-instrument/full_slicer_class.h b/src/goto-inkstrument/full_slicer_class.h similarity index 97% rename from src/goto-instrument/full_slicer_class.h rename to src/goto-inkstrument/full_slicer_class.h index de1c50b54f4..7322fc0b6cb 100644 --- a/src/goto-instrument/full_slicer_class.h +++ b/src/goto-inkstrument/full_slicer_class.h @@ -26,8 +26,8 @@ Author: Daniel Kroening, kroening@kroening.com // #define DEBUG_FULL_SLICERT #if 0 useful for debugging (remove NOLINT) -goto-instrument --full-slice a.out c.out -goto-instrument --show-goto-functions c.out > c.goto +goto-inkstrument --full-slice a.out c.out +goto-inkstrument --show-goto-functions c.out > c.goto echo 'digraph g {' > c.dot ; cat c.goto | \ NOLINT(*) grep 'ins:[[:digit:]]\+ req by' | grep '^[[:space:]]*//' | \ NOLINT(*) perl -n -e '/file .*(.) line (\d+) column ins:(\d+) req by:([\d,]+).*/; $f=$3; $t=$4; @tt=split(",",$t); print "n$f [label=\"$f\"];\n"; print "n$f -> n$_;\n" foreach(@tt);' >> c.dot ; \ diff --git a/src/goto-instrument/function.cpp b/src/goto-inkstrument/function.cpp similarity index 100% rename from src/goto-instrument/function.cpp rename to src/goto-inkstrument/function.cpp diff --git a/src/goto-instrument/function.h b/src/goto-inkstrument/function.h similarity index 100% rename from src/goto-instrument/function.h rename to src/goto-inkstrument/function.h diff --git a/src/goto-instrument/function_modifies.cpp b/src/goto-inkstrument/function_modifies.cpp similarity index 100% rename from src/goto-instrument/function_modifies.cpp rename to src/goto-inkstrument/function_modifies.cpp diff --git a/src/goto-instrument/function_modifies.h b/src/goto-inkstrument/function_modifies.h similarity index 100% rename from src/goto-instrument/function_modifies.h rename to src/goto-inkstrument/function_modifies.h diff --git a/src/goto-instrument/goto_instrument_languages.cpp b/src/goto-inkstrument/goto_instrument_languages.cpp similarity index 100% rename from src/goto-instrument/goto_instrument_languages.cpp rename to src/goto-inkstrument/goto_instrument_languages.cpp diff --git a/src/goto-instrument/goto_instrument_main.cpp b/src/goto-inkstrument/goto_instrument_main.cpp similarity index 100% rename from src/goto-instrument/goto_instrument_main.cpp rename to src/goto-inkstrument/goto_instrument_main.cpp diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-inkstrument/goto_instrument_parse_options.cpp similarity index 99% rename from src/goto-instrument/goto_instrument_parse_options.cpp rename to src/goto-inkstrument/goto_instrument_parse_options.cpp index d5224337440..27f5b95d9a6 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-inkstrument/goto_instrument_parse_options.cpp @@ -1464,8 +1464,8 @@ void goto_instrument_parse_optionst::help() "\n" "Usage: Purpose:\n" "\n" - " goto-instrument [-?] [-h] [--help] show help\n" - " goto-instrument in out perform instrumentation\n" + " goto-inkstrument [-?] [-h] [--help] show help\n" + " goto-inkstrument in out perform instrumentation\n" "\n" "Main options:\n" " --document-properties-html generate HTML property documentation\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-inkstrument/goto_instrument_parse_options.h similarity index 98% rename from src/goto-instrument/goto_instrument_parse_options.h rename to src/goto-inkstrument/goto_instrument_parse_options.h index 4c9ead8d0dc..f1fb9d0210f 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-inkstrument/goto_instrument_parse_options.h @@ -100,7 +100,7 @@ class goto_instrument_parse_optionst: goto_instrument_parse_optionst(int argc, const char **argv): parse_options_baset(GOTO_INSTRUMENT_OPTIONS, argc, argv), messaget(ui_message_handler), - ui_message_handler(cmdline, "goto-instrument"), + ui_message_handler(cmdline, "goto-inkstrument"), function_pointer_removal_done(false), partial_inlining_done(false), remove_returns_done(false) diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-inkstrument/goto_program2code.cpp similarity index 100% rename from src/goto-instrument/goto_program2code.cpp rename to src/goto-inkstrument/goto_program2code.cpp diff --git a/src/goto-instrument/goto_program2code.h b/src/goto-inkstrument/goto_program2code.h similarity index 100% rename from src/goto-instrument/goto_program2code.h rename to src/goto-inkstrument/goto_program2code.h diff --git a/src/goto-instrument/havoc_loops.cpp b/src/goto-inkstrument/havoc_loops.cpp similarity index 100% rename from src/goto-instrument/havoc_loops.cpp rename to src/goto-inkstrument/havoc_loops.cpp diff --git a/src/goto-instrument/havoc_loops.h b/src/goto-inkstrument/havoc_loops.h similarity index 100% rename from src/goto-instrument/havoc_loops.h rename to src/goto-inkstrument/havoc_loops.h diff --git a/src/goto-instrument/horn_encoding.cpp b/src/goto-inkstrument/horn_encoding.cpp similarity index 100% rename from src/goto-instrument/horn_encoding.cpp rename to src/goto-inkstrument/horn_encoding.cpp diff --git a/src/goto-instrument/horn_encoding.h b/src/goto-inkstrument/horn_encoding.h similarity index 100% rename from src/goto-instrument/horn_encoding.h rename to src/goto-inkstrument/horn_encoding.h diff --git a/src/goto-instrument/interrupt.cpp b/src/goto-inkstrument/interrupt.cpp similarity index 100% rename from src/goto-instrument/interrupt.cpp rename to src/goto-inkstrument/interrupt.cpp diff --git a/src/goto-instrument/interrupt.h b/src/goto-inkstrument/interrupt.h similarity index 100% rename from src/goto-instrument/interrupt.h rename to src/goto-inkstrument/interrupt.h diff --git a/src/goto-instrument/k_induction.cpp b/src/goto-inkstrument/k_induction.cpp similarity index 100% rename from src/goto-instrument/k_induction.cpp rename to src/goto-inkstrument/k_induction.cpp diff --git a/src/goto-instrument/k_induction.h b/src/goto-inkstrument/k_induction.h similarity index 100% rename from src/goto-instrument/k_induction.h rename to src/goto-inkstrument/k_induction.h diff --git a/src/goto-instrument/loop_utils.cpp b/src/goto-inkstrument/loop_utils.cpp similarity index 100% rename from src/goto-instrument/loop_utils.cpp rename to src/goto-inkstrument/loop_utils.cpp diff --git a/src/goto-instrument/loop_utils.h b/src/goto-inkstrument/loop_utils.h similarity index 100% rename from src/goto-instrument/loop_utils.h rename to src/goto-inkstrument/loop_utils.h diff --git a/src/goto-instrument/mmio.cpp b/src/goto-inkstrument/mmio.cpp similarity index 100% rename from src/goto-instrument/mmio.cpp rename to src/goto-inkstrument/mmio.cpp diff --git a/src/goto-instrument/mmio.h b/src/goto-inkstrument/mmio.h similarity index 100% rename from src/goto-instrument/mmio.h rename to src/goto-inkstrument/mmio.h diff --git a/src/goto-instrument/model_argc_argv.cpp b/src/goto-inkstrument/model_argc_argv.cpp similarity index 100% rename from src/goto-instrument/model_argc_argv.cpp rename to src/goto-inkstrument/model_argc_argv.cpp diff --git a/src/goto-instrument/model_argc_argv.h b/src/goto-inkstrument/model_argc_argv.h similarity index 100% rename from src/goto-instrument/model_argc_argv.h rename to src/goto-inkstrument/model_argc_argv.h diff --git a/src/goto-instrument/nondet_static.cpp b/src/goto-inkstrument/nondet_static.cpp similarity index 100% rename from src/goto-instrument/nondet_static.cpp rename to src/goto-inkstrument/nondet_static.cpp diff --git a/src/goto-instrument/nondet_static.h b/src/goto-inkstrument/nondet_static.h similarity index 100% rename from src/goto-instrument/nondet_static.h rename to src/goto-inkstrument/nondet_static.h diff --git a/src/goto-instrument/nondet_volatile.cpp b/src/goto-inkstrument/nondet_volatile.cpp similarity index 100% rename from src/goto-instrument/nondet_volatile.cpp rename to src/goto-inkstrument/nondet_volatile.cpp diff --git a/src/goto-instrument/nondet_volatile.h b/src/goto-inkstrument/nondet_volatile.h similarity index 100% rename from src/goto-instrument/nondet_volatile.h rename to src/goto-inkstrument/nondet_volatile.h diff --git a/src/goto-instrument/object_id.cpp b/src/goto-inkstrument/object_id.cpp similarity index 100% rename from src/goto-instrument/object_id.cpp rename to src/goto-inkstrument/object_id.cpp diff --git a/src/goto-instrument/object_id.h b/src/goto-inkstrument/object_id.h similarity index 100% rename from src/goto-instrument/object_id.h rename to src/goto-inkstrument/object_id.h diff --git a/src/goto-instrument/points_to.cpp b/src/goto-inkstrument/points_to.cpp similarity index 100% rename from src/goto-instrument/points_to.cpp rename to src/goto-inkstrument/points_to.cpp diff --git a/src/goto-instrument/points_to.h b/src/goto-inkstrument/points_to.h similarity index 100% rename from src/goto-instrument/points_to.h rename to src/goto-inkstrument/points_to.h diff --git a/src/goto-instrument/race_check.cpp b/src/goto-inkstrument/race_check.cpp similarity index 100% rename from src/goto-instrument/race_check.cpp rename to src/goto-inkstrument/race_check.cpp diff --git a/src/goto-instrument/race_check.h b/src/goto-inkstrument/race_check.h similarity index 100% rename from src/goto-instrument/race_check.h rename to src/goto-inkstrument/race_check.h diff --git a/src/goto-instrument/reachability_slicer.cpp b/src/goto-inkstrument/reachability_slicer.cpp similarity index 100% rename from src/goto-instrument/reachability_slicer.cpp rename to src/goto-inkstrument/reachability_slicer.cpp diff --git a/src/goto-instrument/reachability_slicer.h b/src/goto-inkstrument/reachability_slicer.h similarity index 100% rename from src/goto-instrument/reachability_slicer.h rename to src/goto-inkstrument/reachability_slicer.h diff --git a/src/goto-instrument/reachability_slicer_class.h b/src/goto-inkstrument/reachability_slicer_class.h similarity index 100% rename from src/goto-instrument/reachability_slicer_class.h rename to src/goto-inkstrument/reachability_slicer_class.h diff --git a/src/goto-instrument/remove_function.cpp b/src/goto-inkstrument/remove_function.cpp similarity index 100% rename from src/goto-instrument/remove_function.cpp rename to src/goto-inkstrument/remove_function.cpp diff --git a/src/goto-instrument/remove_function.h b/src/goto-inkstrument/remove_function.h similarity index 100% rename from src/goto-instrument/remove_function.h rename to src/goto-inkstrument/remove_function.h diff --git a/src/goto-instrument/rw_set.cpp b/src/goto-inkstrument/rw_set.cpp similarity index 100% rename from src/goto-instrument/rw_set.cpp rename to src/goto-inkstrument/rw_set.cpp diff --git a/src/goto-instrument/rw_set.h b/src/goto-inkstrument/rw_set.h similarity index 100% rename from src/goto-instrument/rw_set.h rename to src/goto-inkstrument/rw_set.h diff --git a/src/goto-instrument/show_locations.cpp b/src/goto-inkstrument/show_locations.cpp similarity index 100% rename from src/goto-instrument/show_locations.cpp rename to src/goto-inkstrument/show_locations.cpp diff --git a/src/goto-instrument/show_locations.h b/src/goto-inkstrument/show_locations.h similarity index 100% rename from src/goto-instrument/show_locations.h rename to src/goto-inkstrument/show_locations.h diff --git a/src/goto-instrument/skip_loops.cpp b/src/goto-inkstrument/skip_loops.cpp similarity index 100% rename from src/goto-instrument/skip_loops.cpp rename to src/goto-inkstrument/skip_loops.cpp diff --git a/src/goto-instrument/skip_loops.h b/src/goto-inkstrument/skip_loops.h similarity index 100% rename from src/goto-instrument/skip_loops.h rename to src/goto-inkstrument/skip_loops.h diff --git a/src/goto-instrument/splice_call.cpp b/src/goto-inkstrument/splice_call.cpp similarity index 100% rename from src/goto-instrument/splice_call.cpp rename to src/goto-inkstrument/splice_call.cpp diff --git a/src/goto-instrument/splice_call.h b/src/goto-inkstrument/splice_call.h similarity index 100% rename from src/goto-instrument/splice_call.h rename to src/goto-inkstrument/splice_call.h diff --git a/src/goto-instrument/stack_depth.cpp b/src/goto-inkstrument/stack_depth.cpp similarity index 100% rename from src/goto-instrument/stack_depth.cpp rename to src/goto-inkstrument/stack_depth.cpp diff --git a/src/goto-instrument/stack_depth.h b/src/goto-inkstrument/stack_depth.h similarity index 100% rename from src/goto-instrument/stack_depth.h rename to src/goto-inkstrument/stack_depth.h diff --git a/src/goto-instrument/thread_instrumentation.cpp b/src/goto-inkstrument/thread_instrumentation.cpp similarity index 100% rename from src/goto-instrument/thread_instrumentation.cpp rename to src/goto-inkstrument/thread_instrumentation.cpp diff --git a/src/goto-instrument/thread_instrumentation.h b/src/goto-inkstrument/thread_instrumentation.h similarity index 100% rename from src/goto-instrument/thread_instrumentation.h rename to src/goto-inkstrument/thread_instrumentation.h diff --git a/src/goto-instrument/undefined_functions.cpp b/src/goto-inkstrument/undefined_functions.cpp similarity index 100% rename from src/goto-instrument/undefined_functions.cpp rename to src/goto-inkstrument/undefined_functions.cpp diff --git a/src/goto-instrument/undefined_functions.h b/src/goto-inkstrument/undefined_functions.h similarity index 100% rename from src/goto-instrument/undefined_functions.h rename to src/goto-inkstrument/undefined_functions.h diff --git a/src/goto-instrument/uninitialized.cpp b/src/goto-inkstrument/uninitialized.cpp similarity index 100% rename from src/goto-instrument/uninitialized.cpp rename to src/goto-inkstrument/uninitialized.cpp diff --git a/src/goto-instrument/uninitialized.h b/src/goto-inkstrument/uninitialized.h similarity index 100% rename from src/goto-instrument/uninitialized.h rename to src/goto-inkstrument/uninitialized.h diff --git a/src/goto-instrument/unwind.cpp b/src/goto-inkstrument/unwind.cpp similarity index 100% rename from src/goto-instrument/unwind.cpp rename to src/goto-inkstrument/unwind.cpp diff --git a/src/goto-instrument/unwind.h b/src/goto-inkstrument/unwind.h similarity index 100% rename from src/goto-instrument/unwind.h rename to src/goto-inkstrument/unwind.h diff --git a/src/goto-instrument/wmm/abstract_event.cpp b/src/goto-inkstrument/wmm/abstract_event.cpp similarity index 100% rename from src/goto-instrument/wmm/abstract_event.cpp rename to src/goto-inkstrument/wmm/abstract_event.cpp diff --git a/src/goto-instrument/wmm/abstract_event.h b/src/goto-inkstrument/wmm/abstract_event.h similarity index 100% rename from src/goto-instrument/wmm/abstract_event.h rename to src/goto-inkstrument/wmm/abstract_event.h diff --git a/src/goto-instrument/wmm/cycle_collection.cpp b/src/goto-inkstrument/wmm/cycle_collection.cpp similarity index 100% rename from src/goto-instrument/wmm/cycle_collection.cpp rename to src/goto-inkstrument/wmm/cycle_collection.cpp diff --git a/src/goto-instrument/wmm/data_dp.cpp b/src/goto-inkstrument/wmm/data_dp.cpp similarity index 100% rename from src/goto-instrument/wmm/data_dp.cpp rename to src/goto-inkstrument/wmm/data_dp.cpp diff --git a/src/goto-instrument/wmm/data_dp.h b/src/goto-inkstrument/wmm/data_dp.h similarity index 100% rename from src/goto-instrument/wmm/data_dp.h rename to src/goto-inkstrument/wmm/data_dp.h diff --git a/src/goto-instrument/wmm/event_graph.cpp b/src/goto-inkstrument/wmm/event_graph.cpp similarity index 99% rename from src/goto-instrument/wmm/event_graph.cpp rename to src/goto-inkstrument/wmm/event_graph.cpp index 110a3618ea2..a3c151faf11 100644 --- a/src/goto-instrument/wmm/event_graph.cpp +++ b/src/goto-inkstrument/wmm/event_graph.cpp @@ -340,7 +340,7 @@ bool event_grapht::critical_cyclet::is_unsafe(memory_modelt model, bool fast) const abstract_eventt &second=s_evt; const data_dpt &data_dp=egraph.map_data_dp[first.thread]; - /* if data dp between linking the pair, safe */ + /* if data dp between inking the pair, safe */ if(first.thread==second.thread && data_dp.dp(first, second)) continue; @@ -472,7 +472,7 @@ bool event_grapht::critical_cyclet::is_unsafe(memory_modelt model, bool fast) const data_dpt &data_dp=egraph.map_data_dp[first.thread]; - /* if data dp between linking the pair, safe */ + /* if data dp between inking the pair, safe */ if(first.thread==second.thread && data_dp.dp(first, second)) return unsafe_met; @@ -623,7 +623,7 @@ bool event_grapht::critical_cyclet::is_unsafe_asm( const data_dpt &data_dp=egraph.map_data_dp[first.thread]; - /* if data dp between linking the pair, safe */ + /* if data dp between inking the pair, safe */ if(first.thread==second.thread && data_dp.dp(first, second)) continue; @@ -778,7 +778,7 @@ bool event_grapht::critical_cyclet::is_unsafe_asm( const data_dpt &data_dp=egraph.map_data_dp[first.thread]; - /* if data dp between linking the pair, safe */ + /* if data dp between inking the pair, safe */ if(first.thread==second.thread && data_dp.dp(first, second)) return unsafe_met; diff --git a/src/goto-instrument/wmm/event_graph.h b/src/goto-inkstrument/wmm/event_graph.h similarity index 100% rename from src/goto-instrument/wmm/event_graph.h rename to src/goto-inkstrument/wmm/event_graph.h diff --git a/src/goto-instrument/wmm/fence.cpp b/src/goto-inkstrument/wmm/fence.cpp similarity index 100% rename from src/goto-instrument/wmm/fence.cpp rename to src/goto-inkstrument/wmm/fence.cpp diff --git a/src/goto-instrument/wmm/fence.h b/src/goto-inkstrument/wmm/fence.h similarity index 100% rename from src/goto-instrument/wmm/fence.h rename to src/goto-inkstrument/wmm/fence.h diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-inkstrument/wmm/goto2graph.cpp similarity index 100% rename from src/goto-instrument/wmm/goto2graph.cpp rename to src/goto-inkstrument/wmm/goto2graph.cpp diff --git a/src/goto-instrument/wmm/goto2graph.h b/src/goto-inkstrument/wmm/goto2graph.h similarity index 100% rename from src/goto-instrument/wmm/goto2graph.h rename to src/goto-inkstrument/wmm/goto2graph.h diff --git a/src/goto-instrument/wmm/instrumenter_pensieve.h b/src/goto-inkstrument/wmm/instrumenter_pensieve.h similarity index 100% rename from src/goto-instrument/wmm/instrumenter_pensieve.h rename to src/goto-inkstrument/wmm/instrumenter_pensieve.h diff --git a/src/goto-instrument/wmm/instrumenter_strategies.cpp b/src/goto-inkstrument/wmm/instrumenter_strategies.cpp similarity index 99% rename from src/goto-instrument/wmm/instrumenter_strategies.cpp rename to src/goto-inkstrument/wmm/instrumenter_strategies.cpp index 97ad9888f80..0e406feda3a 100644 --- a/src/goto-instrument/wmm/instrumenter_strategies.cpp +++ b/src/goto-inkstrument/wmm/instrumenter_strategies.cpp @@ -345,7 +345,7 @@ void inline instrumentert::instrument_minimum_interference_inserter( glp_delete_prob(lp); #else throw "sorry, minimum interference option requires glpk; " - "please recompile goto-instrument with glpk"; + "please recompile goto-inkstrument with glpk"; #endif } diff --git a/src/goto-instrument/wmm/pair_collection.cpp b/src/goto-inkstrument/wmm/pair_collection.cpp similarity index 100% rename from src/goto-instrument/wmm/pair_collection.cpp rename to src/goto-inkstrument/wmm/pair_collection.cpp diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-inkstrument/wmm/shared_buffers.cpp similarity index 100% rename from src/goto-instrument/wmm/shared_buffers.cpp rename to src/goto-inkstrument/wmm/shared_buffers.cpp diff --git a/src/goto-instrument/wmm/shared_buffers.h b/src/goto-inkstrument/wmm/shared_buffers.h similarity index 100% rename from src/goto-instrument/wmm/shared_buffers.h rename to src/goto-inkstrument/wmm/shared_buffers.h diff --git a/src/goto-instrument/wmm/weak_memory.cpp b/src/goto-inkstrument/wmm/weak_memory.cpp similarity index 100% rename from src/goto-instrument/wmm/weak_memory.cpp rename to src/goto-inkstrument/wmm/weak_memory.cpp diff --git a/src/goto-instrument/wmm/weak_memory.h b/src/goto-inkstrument/wmm/weak_memory.h similarity index 100% rename from src/goto-instrument/wmm/weak_memory.h rename to src/goto-inkstrument/wmm/weak_memory.h diff --git a/src/goto-instrument/wmm/wmm.h b/src/goto-inkstrument/wmm/wmm.h similarity index 100% rename from src/goto-instrument/wmm/wmm.h rename to src/goto-inkstrument/wmm/wmm.h diff --git a/src/goto-programs/README.md b/src/goto-programs/README.md index 4bccc9de726..626b97ee3ab 100644 --- a/src/goto-programs/README.md +++ b/src/goto-programs/README.md @@ -57,7 +57,7 @@ from strings to `goto_programt`’s and iteration macros are provided. Note that `goto_function_templatet` (no `s`) is defined in the same header as `goto_functions_templatet` and is gives the C type for the function and Boolean which indicates whether the body is available -(before linking this might not always be true). Also note the slightly +(before inking this might not always be true). Also note the slightly counter-intuitive naming; `goto_functionst` instances are the top level structure representing the program and contain `goto_programt` instances which represent the individual functions. At the time of writing @@ -347,7 +347,7 @@ previous stage: The order of instructions in a list of instructions---as well as the targets of GOTOs---are both displayed as arrows when viewing a - goto-program as a Graphviz DOT file with `goto-instrument --dot`. + goto-program as a Graphviz DOT file with `goto-inkstrument --dot`. The semantics of a goto-program is: the next instruction is the next instruction in the list, unless the current instruction has a target; in that case, check the guard of the instruction, and jump diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 35e67c16b5e..aee70a83e9f 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -29,7 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include diff --git a/src/goto-programs/link_goto_model.cpp b/src/goto-programs/link_goto_model.cpp index 6fd9702cf0e..e821f6513ab 100644 --- a/src/goto-programs/link_goto_model.cpp +++ b/src/goto-programs/link_goto_model.cpp @@ -17,7 +17,7 @@ Author: Michael Tautschnig, Daniel Kroening #include #include -#include +#include #include "goto_model.h" @@ -99,10 +99,10 @@ static bool link_functions( } else { - // the linking code will have ensured that types match + // the inking code will have ensured that types match rename_symbol(src_func.type); INVARIANT(base_type_eq(in_dest_symbol_table.type, src_func.type, ns), - "linking ensures that types match"); + "inking ensures that types match"); } } } @@ -167,11 +167,11 @@ void link_goto_model( weak_symbols.insert(symbol_pair.first); } - linkingt linking(dest.symbol_table, + inkingt inking(dest.symbol_table, src.symbol_table, message_handler); - if(linking.typecheck_main()) + if(inking.typecheck_main()) throw 0; if(link_functions( @@ -179,8 +179,8 @@ void link_goto_model( dest.goto_functions, src.symbol_table, src.goto_functions, - linking.rename_symbol, + inking.rename_symbol, weak_symbols, - linking.object_type_updates)) + inking.object_type_updates)) throw 0; } diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp index 466d6cef4ab..1fc6c6ff230 100644 --- a/src/goto-programs/read_bin_goto_object.cpp +++ b/src/goto-programs/read_bin_goto_object.cpp @@ -225,7 +225,7 @@ bool read_bin_goto_object( case 2: message.error() << "The input was compiled with an old version of " - "goto-cc; please recompile" << messaget::eom; + "goto-sea-sea; please recompile" << messaget::eom; return true; case 3: @@ -238,7 +238,7 @@ bool read_bin_goto_object( default: message.error() << "The input was compiled with an unsupported version of " - "goto-cc; please recompile" << messaget::eom; + "goto-sea-sea; please recompile" << messaget::eom; return true; } } diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp index 9e7a1968ccc..bd6a4b873c2 100644 --- a/src/goto-programs/read_goto_binary.cpp +++ b/src/goto-programs/read_goto_binary.cpp @@ -80,13 +80,13 @@ bool read_goto_binary( else if(hdr[0]==0x7f && hdr[1]=='E' && hdr[2]=='L' && hdr[3]=='F') { // ELF binary. - // This _may_ have a goto-cc section. + // This _may_ have a goto-sea-sea section. try { elf_readert elf_reader(in); for(unsigned i=0; i #include -#include +#include void slice_global_inits(goto_modelt &goto_model) { diff --git a/src/goto-sea-sea/CMakeLists.txt b/src/goto-sea-sea/CMakeLists.txt new file mode 100644 index 00000000000..fffa12b94c1 --- /dev/null +++ b/src/goto-sea-sea/CMakeLists.txt @@ -0,0 +1,36 @@ +# Library +file(GLOB_RECURSE sources "*.cpp" "*.h") +list(REMOVE_ITEM sources + ${CMAKE_CURRENT_SOURCE_DIR}/goto_cc_main.cpp +) +add_library(goto-sea-sea-lib ${sources}) + +generic_includes(goto-sea-sea-lib) + +target_link_libraries(goto-sea-sea-lib + big-int + goto-programs + util + inking + ansi-c + cpp + xml + assembler + langapi +) + +add_if_library(goto-sea-sea-lib java_bytecode) +add_if_library(goto-sea-sea-lib jsil) + +# Executable +add_executable(goto-sea-sea goto_cc_main.cpp) +target_link_libraries(goto-sea-sea goto-sea-sea-lib) + +if(WIN32) + set_target_properties(goto-sea-sea PROPERTIES OUTPUT_NAME goto-cl) +else() + add_custom_command(TARGET goto-sea-sea + POST_BUILD + COMMAND "${CMAKE_COMMAND}" -E create_symlink + goto-sea-sea $/goto-gcc) +endif() diff --git a/src/goto-cc/Makefile b/src/goto-sea-sea/Makefile similarity index 81% rename from src/goto-cc/Makefile rename to src/goto-sea-sea/Makefile index 374ed507b44..6060e541f4c 100644 --- a/src/goto-cc/Makefile +++ b/src/goto-sea-sea/Makefile @@ -21,7 +21,7 @@ SRC = armcc_cmdline.cpp \ OBJ += ../big-int/big-int$(LIBEXT) \ ../goto-programs/goto-programs$(LIBEXT) \ ../util/util$(LIBEXT) \ - ../linking/linking$(LIBEXT) \ + ../inking/inking$(LIBEXT) \ ../ansi-c/ansi-c$(LIBEXT) \ ../cpp/cpp$(LIBEXT) \ ../java_bytecode/java_bytecode$(LIBEXT) \ @@ -35,7 +35,7 @@ INCLUDES= -I .. LIBS = -CLEANFILES = goto-cc$(EXEEXT) goto-cl$(EXEEXT) +CLEANFILES = goto-sea-sea$(EXEEXT) goto-cl$(EXEEXT) include ../config.inc include ../common @@ -43,7 +43,7 @@ include ../common ifeq ($(BUILD_ENV_),MSVC) all: goto-cl$(EXEEXT) endif -all: goto-cc$(EXEEXT) +all: goto-sea-sea$(EXEEXT) ifneq ($(wildcard ../jsil/Makefile),) OBJ += ../jsil/jsil$(LIBEXT) @@ -52,13 +52,13 @@ endif ############################################################################### -goto-cc$(EXEEXT): $(OBJ) +goto-sea-sea$(EXEEXT): $(OBJ) $(LINKBIN) goto-cl$(EXEEXT): $(OBJ) $(LINKBIN) -.PHONY: goto-cc-mac-signed +.PHONY: goto-sea-sea-mac-signed -goto-cc-mac-signed: goto-cc$(EXEEXT) - codesign -v -s $(OSX_IDENTITY) goto-cc$(EXEEXT) +goto-sea-sea-mac-signed: goto-sea-sea$(EXEEXT) + codesign -v -s $(OSX_IDENTITY) goto-sea-sea$(EXEEXT) diff --git a/src/goto-cc/README.md b/src/goto-sea-sea/README.md similarity index 63% rename from src/goto-cc/README.md rename to src/goto-sea-sea/README.md index 98dbc67e6ad..6a22fd1374d 100644 --- a/src/goto-cc/README.md +++ b/src/goto-sea-sea/README.md @@ -1,16 +1,16 @@ \ingroup module_hidden -\defgroup goto-cc goto-cc +\defgroup goto-sea-sea goto-sea-sea -# Folder goto-cc +# Folder goto-sea-sea \author Martin Brain -`goto-cc` is a compiler replacement that just performs the first step of +`goto-sea-sea` is a compiler replacement that just performs the first step of the process; converting C or C++ programs to goto-binaries. It is intended to be dropped in to an existing build procedure in place of the compiler, thus it emulates flags that would affect the semantics of the code produced. Which set of flags are emulated depends on the naming of -the `goto-cc/` binary. If it is called `goto-cc` then it emulates GCC +the `goto-sea-sea/` binary. If it is called `goto-sea-sea` then it emulates GCC flags, `goto-armcc` emulates the ARM compiler, `goto-cl` emulates VCC and `goto-cw` emulates the Code Warrior compiler. The output of this -tool can then be used with `cbmc` or `goto-instrument`. +tool can then be used with `cbmc` or `goto-inkstrument`. diff --git a/src/goto-cc/armcc_cmdline.cpp b/src/goto-sea-sea/armcc_cmdline.cpp similarity index 99% rename from src/goto-cc/armcc_cmdline.cpp rename to src/goto-sea-sea/armcc_cmdline.cpp index d0a16ac95a0..85250e473cb 100644 --- a/src/goto-cc/armcc_cmdline.cpp +++ b/src/goto-sea-sea/armcc_cmdline.cpp @@ -22,7 +22,7 @@ Author: Daniel Kroening static const char *options_no_arg[]= { - // goto-cc-specific + // goto-sea-sea-specific "--show-symbol-table", "--show-function-table", "--16", @@ -247,7 +247,7 @@ static const char *options_with_prefix[]= static const char *options_with_arg[]= { - // goto-cc specific + // goto-sea-sea specific "--verbosity", "--function", diff --git a/src/goto-cc/armcc_cmdline.h b/src/goto-sea-sea/armcc_cmdline.h similarity index 100% rename from src/goto-cc/armcc_cmdline.h rename to src/goto-sea-sea/armcc_cmdline.h diff --git a/src/goto-cc/armcc_mode.cpp b/src/goto-sea-sea/armcc_mode.cpp similarity index 100% rename from src/goto-cc/armcc_mode.cpp rename to src/goto-sea-sea/armcc_mode.cpp diff --git a/src/goto-cc/armcc_mode.h b/src/goto-sea-sea/armcc_mode.h similarity index 100% rename from src/goto-cc/armcc_mode.h rename to src/goto-sea-sea/armcc_mode.h diff --git a/src/goto-cc/as86_cmdline.cpp b/src/goto-sea-sea/as86_cmdline.cpp similarity index 100% rename from src/goto-cc/as86_cmdline.cpp rename to src/goto-sea-sea/as86_cmdline.cpp diff --git a/src/goto-cc/as86_cmdline.h b/src/goto-sea-sea/as86_cmdline.h similarity index 100% rename from src/goto-cc/as86_cmdline.h rename to src/goto-sea-sea/as86_cmdline.h diff --git a/src/goto-cc/as_cmdline.cpp b/src/goto-sea-sea/as_cmdline.cpp similarity index 100% rename from src/goto-cc/as_cmdline.cpp rename to src/goto-sea-sea/as_cmdline.cpp diff --git a/src/goto-cc/as_cmdline.h b/src/goto-sea-sea/as_cmdline.h similarity index 100% rename from src/goto-cc/as_cmdline.h rename to src/goto-sea-sea/as_cmdline.h diff --git a/src/goto-cc/as_mode.cpp b/src/goto-sea-sea/as_mode.cpp similarity index 92% rename from src/goto-cc/as_mode.cpp rename to src/goto-sea-sea/as_mode.cpp index bf69e209eda..021f16134cc 100644 --- a/src/goto-cc/as_mode.cpp +++ b/src/goto-sea-sea/as_mode.cpp @@ -86,11 +86,11 @@ int as_modet::doit() cmdline.isset("version")) { if(act_as_as86) - status() << "as86 version: 0.16.17 (goto-cc " CBMC_VERSION ")" + status() << "as86 version: 0.16.17 (goto-sea-sea " CBMC_VERSION ")" << eom; else status() << "GNU assembler version 2.20.51.0.7 20100318" - << " (goto-cc " CBMC_VERSION ")" << eom; + << " (goto-sea-sea " CBMC_VERSION ")" << eom; status() << '\n' << "Copyright (C) 2006-2014 Daniel Kroening, Christoph Wintersteiger\n" << @@ -133,12 +133,12 @@ int as_modet::doit() if(cmdline.isset('b')) // as86 only { compiler.mode=compilet::COMPILE_LINK_EXECUTABLE; - debug() << "Compiling and linking an executable" << eom; + debug() << "Compiling and inking an executable" << eom; } else { compiler.mode=compilet::COMPILE_LINK; - debug() << "Compiling and linking a library" << eom; + debug() << "Compiling and inking a library" << eom; } config.ansi_c.mode=configt::ansi_ct::flavourt::GCC; @@ -163,7 +163,7 @@ int as_modet::doit() // We now iterate over any input files - temp_dirt temp_dir("goto-cc-XXXXXX"); + temp_dirt temp_dir("goto-sea-sea-XXXXXX"); for(goto_cc_cmdlinet::parsed_argvt::iterator arg_it=cmdline.parsed_argv.begin(); @@ -293,10 +293,10 @@ int as_modet::as_hybrid_binary() debug() << "Running " << native_tool_name << " to generate hybrid binary" << eom; - // save the goto-cc output file + // save the goto-sea-sea output file int result=rename( output_file.c_str(), - (output_file+".goto-cc-saved").c_str()); + (output_file+".goto-sea-sea-saved").c_str()); if(result!=0) { error() << "Rename failed: " << std::strerror(errno) << eom; @@ -308,16 +308,16 @@ int as_modet::as_hybrid_binary() // merge output from as with goto-binaries // using objcopy, or do cleanup if an earlier call failed debug() << "merging " << output_file << eom; - std::string saved=output_file+".goto-cc-saved"; + std::string saved=output_file+".goto-sea-sea-saved"; #ifdef __linux__ if(result==0) { - // remove any existing goto-cc section + // remove any existing goto-sea-sea section std::vector objcopy_argv; objcopy_argv.push_back("objcopy"); - objcopy_argv.push_back("--remove-section=goto-cc"); + objcopy_argv.push_back("--remove-section=goto-sea-sea"); objcopy_argv.push_back(output_file); result=run(objcopy_argv[0], objcopy_argv, "", ""); @@ -325,12 +325,12 @@ int as_modet::as_hybrid_binary() if(result==0) { - // now add goto-binary as goto-cc section + // now add goto-binary as goto-sea-sea section std::vector objcopy_argv; objcopy_argv.push_back("objcopy"); objcopy_argv.push_back("--add-section"); - objcopy_argv.push_back("goto-cc="+saved); + objcopy_argv.push_back("goto-sea-sea="+saved); objcopy_argv.push_back(output_file); result=run(objcopy_argv[0], objcopy_argv, "", ""); diff --git a/src/goto-cc/as_mode.h b/src/goto-sea-sea/as_mode.h similarity index 100% rename from src/goto-cc/as_mode.h rename to src/goto-sea-sea/as_mode.h diff --git a/src/goto-cc/bcc_cmdline.cpp b/src/goto-sea-sea/bcc_cmdline.cpp similarity index 100% rename from src/goto-cc/bcc_cmdline.cpp rename to src/goto-sea-sea/bcc_cmdline.cpp diff --git a/src/goto-cc/bcc_cmdline.h b/src/goto-sea-sea/bcc_cmdline.h similarity index 100% rename from src/goto-cc/bcc_cmdline.h rename to src/goto-sea-sea/bcc_cmdline.h diff --git a/src/goto-cc/compile.cpp b/src/goto-sea-sea/compile.cpp similarity index 99% rename from src/goto-cc/compile.cpp rename to src/goto-sea-sea/compile.cpp index c2473ff9dc6..1872312a17c 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-sea-sea/compile.cpp @@ -181,7 +181,7 @@ bool compilet::add_input_file(const std::string &file_name) #ifdef _WIN32 char td[MAX_PATH+1]; #else - char td[] = "goto-cc.XXXXXX"; + char td[] = "goto-sea-sea.XXXXXX"; #endif std::string tstr=get_temporary_directory(td); diff --git a/src/goto-cc/compile.h b/src/goto-sea-sea/compile.h similarity index 100% rename from src/goto-cc/compile.h rename to src/goto-sea-sea/compile.h diff --git a/src/goto-cc/cw_mode.cpp b/src/goto-sea-sea/cw_mode.cpp similarity index 100% rename from src/goto-cc/cw_mode.cpp rename to src/goto-sea-sea/cw_mode.cpp diff --git a/src/goto-cc/cw_mode.h b/src/goto-sea-sea/cw_mode.h similarity index 100% rename from src/goto-cc/cw_mode.h rename to src/goto-sea-sea/cw_mode.h diff --git a/src/goto-sea-sea/dist-linux b/src/goto-sea-sea/dist-linux new file mode 100644 index 00000000000..3dbda98b6a6 --- /dev/null +++ b/src/goto-sea-sea/dist-linux @@ -0,0 +1,26 @@ +#!/bin/bash +make +strip goto-sea-sea + +VERSION=`./goto-sea-sea --version` +VERSION_FILE=`echo $VERSION | sed "y/./-/"` + +echo $VERSION_FILE + +(cd ../goto-sea-sea; make; strip goto-sea-sea) +(cd ../goto-inkstrument; make; strip goto-inkstrument) + +mkdir /tmp/goto-sea-sea-dist +cp goto-sea-sea /tmp/goto-sea-sea-dist/ +cp ../goto-inkstrument/goto-inkstrument /tmp/goto-sea-sea-dist/ +cp ../../LICENSE /tmp/goto-sea-sea-dist/ +cp ../../scripts/ls_parse.py /tmp/goto-sea-sea-dist/ +cd /tmp/goto-sea-sea-dist +tar cfz goto-sea-sea-${VERSION_FILE}-linux.tgz goto-sea-sea \ + goto-inkstrument LICENSE ls_parse.py + +echo Copying. +scp goto-sea-sea-${VERSION_FILE}-linux.tgz kroening@dkr0.inf.ethz.ch:/home/www/cprover.org/goto-sea-sea/download/ + +cd /tmp +rm -R /tmp/goto-sea-sea-dist diff --git a/src/goto-sea-sea/dist-win b/src/goto-sea-sea/dist-win new file mode 100644 index 00000000000..45e66be25f1 --- /dev/null +++ b/src/goto-sea-sea/dist-win @@ -0,0 +1,26 @@ +#!/bin/bash + +make +strip goto-sea-sea.exe + +VERSION=`./goto-sea-sea.exe --version` +VERSION_FILE=`echo $VERSION | sed "y/./-/"` + +(cd ../goto-sea-sea; make; strip goto-sea-sea.exe) +(cd ../goto-inkstrument; make; strip goto-inkstrument.exe) + +echo $VERSION_FILE + +mkdir /tmp/goto-sea-sea-dist +cp goto-sea-sea.exe /tmp/goto-sea-sea-dist/ +cp ../goto-inkstrument/goto-inkstrument.exe /tmp/goto-sea-sea-dist/ +cp ../../LICENSE /tmp/goto-sea-sea-dist/ +cd /tmp/goto-sea-sea-dist +zip -9 goto-sea-sea-${VERSION_FILE}-win.zip goto-sea-sea.exe \ + goto-inkstrument.exe LICENSE + +echo Copying. +scp goto-sea-sea-${VERSION_FILE}-win.zip kroening@dkr0.inf.ethz.ch:/home/www/cprover.org/goto-sea-sea/download/ + +cd /tmp +rm -R /tmp/goto-sea-sea-dist diff --git a/src/goto-cc/gcc_cmdline.cpp b/src/goto-sea-sea/gcc_cmdline.cpp similarity index 100% rename from src/goto-cc/gcc_cmdline.cpp rename to src/goto-sea-sea/gcc_cmdline.cpp diff --git a/src/goto-cc/gcc_cmdline.h b/src/goto-sea-sea/gcc_cmdline.h similarity index 100% rename from src/goto-cc/gcc_cmdline.h rename to src/goto-sea-sea/gcc_cmdline.h diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-sea-sea/gcc_mode.cpp similarity index 97% rename from src/goto-cc/gcc_mode.cpp rename to src/goto-sea-sea/gcc_mode.cpp index 88c940aa9dc..0f6fb998d18 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/src/goto-sea-sea/gcc_mode.cpp @@ -109,7 +109,7 @@ gcc_modet::gcc_modet( produce_hybrid_binary(_produce_hybrid_binary), act_as_ld(base_name=="ld" || base_name.find("goto-ld")!=std::string::npos), - goto_binary_tmp_suffix(".goto-cc-saved"), + goto_binary_tmp_suffix(".goto-sea-sea-saved"), // Keys are architectures specified in configt::set_arch(). // Values are lists of GCC architectures that can be supplied as @@ -352,12 +352,12 @@ int gcc_modet::doit() // Compilation continues, don't exit! if(act_as_ld) - std::cout << "GNU ld version 2.16.91 20050610 (goto-cc " CBMC_VERSION + std::cout << "GNU ld version 2.16.91 20050610 (goto-sea-sea " CBMC_VERSION << ")\n"; else if(act_as_bcc) - std::cout << "bcc: version 0.16.17 (goto-cc " CBMC_VERSION ")\n"; + std::cout << "bcc: version 0.16.17 (goto-sea-sea " CBMC_VERSION ")\n"; else - std::cout << "gcc version 3.4.4 (goto-cc " CBMC_VERSION ")\n"; + std::cout << "gcc version 3.4.4 (goto-sea-sea " CBMC_VERSION ")\n"; } compilet compiler(cmdline, @@ -536,9 +536,9 @@ int gcc_modet::doit() case compilet::PREPROCESS_ONLY: debug() << "Preprocessing only" << eom; break; case compilet::COMPILE_LINK: - debug() << "Compiling and linking a library" << eom; break; + debug() << "Compiling and inking a library" << eom; break; case compilet::COMPILE_LINK_EXECUTABLE: - debug() << "Compiling and linking an executable" << eom; break; + debug() << "Compiling and inking an executable" << eom; break; } if(cmdline.isset("i386-win32") || @@ -635,7 +635,7 @@ int gcc_modet::doit() // We now iterate over any input files - temp_dirt temp_dir("goto-cc-XXXXXX"); + temp_dirt temp_dir("goto-sea-sea-XXXXXX"); { std::string language; @@ -899,7 +899,7 @@ int gcc_modet::gcc_hybrid_binary(compilet &compiler) debug() << "Running " << native_tool_name << " to generate hybrid binary" << eom; - // save the goto-cc output files + // save the goto-sea-sea output files std::list goto_binaries; for(std::list::const_iterator it=output_files.begin(); @@ -951,11 +951,11 @@ int gcc_modet::gcc_hybrid_binary(compilet &compiler) #ifdef __linux__ if(result==0 && !cmdline.isset('c')) { - // remove any existing goto-cc section + // remove any existing goto-sea-sea section std::vector objcopy_argv; objcopy_argv.push_back(objcopy_cmd); - objcopy_argv.push_back("--remove-section=goto-cc"); + objcopy_argv.push_back("--remove-section=goto-sea-sea"); objcopy_argv.push_back(*it); result=run(objcopy_argv[0], objcopy_argv, "", ""); @@ -963,12 +963,12 @@ int gcc_modet::gcc_hybrid_binary(compilet &compiler) if(result==0) { - // now add goto-binary as goto-cc section + // now add goto-binary as goto-sea-sea section std::vector objcopy_argv; objcopy_argv.push_back(objcopy_cmd); objcopy_argv.push_back("--add-section"); - objcopy_argv.push_back("goto-cc="+saved); + objcopy_argv.push_back("goto-sea-sea="+saved); objcopy_argv.push_back(*it); result=run(objcopy_argv[0], objcopy_argv, "", ""); @@ -1110,6 +1110,6 @@ void gcc_modet::help_mode() std::cout << "goto-ld understands the options of " << "ld plus the following.\n\n"; else - std::cout << "goto-cc understands the options of " + std::cout << "goto-sea-sea understands the options of " << "gcc plus the following.\n\n"; } diff --git a/src/goto-cc/gcc_mode.h b/src/goto-sea-sea/gcc_mode.h similarity index 100% rename from src/goto-cc/gcc_mode.h rename to src/goto-sea-sea/gcc_mode.h diff --git a/src/goto-cc/goto_cc_cmdline.cpp b/src/goto-sea-sea/goto_cc_cmdline.cpp similarity index 93% rename from src/goto-cc/goto_cc_cmdline.cpp rename to src/goto-sea-sea/goto_cc_cmdline.cpp index ac86ee38551..29d51025618 100644 --- a/src/goto-cc/goto_cc_cmdline.cpp +++ b/src/goto-sea-sea/goto_cc_cmdline.cpp @@ -1,6 +1,6 @@ /*******************************************************************\ -Module: Command line interpretation for goto-cc +Module: Command line interpretation for goto-sea-sea Author: Daniel Kroening @@ -9,7 +9,7 @@ Date: April 2010 \*******************************************************************/ /// \file -/// Command line interpretation for goto-cc +/// Command line interpretation for goto-sea-sea #include "goto_cc_cmdline.h" @@ -123,7 +123,7 @@ void goto_cc_cmdlinet::add_infile_arg(const std::string &arg) if(arg=="-") { - stdin_file=get_temporary_file("goto-cc", "stdin"); + stdin_file=get_temporary_file("goto-sea-sea", "stdin"); FILE *tmp=fopen(stdin_file.c_str(), "wt"); diff --git a/src/goto-cc/goto_cc_cmdline.h b/src/goto-sea-sea/goto_cc_cmdline.h similarity index 94% rename from src/goto-cc/goto_cc_cmdline.h rename to src/goto-sea-sea/goto_cc_cmdline.h index f699946da68..0e25a36bac1 100644 --- a/src/goto-cc/goto_cc_cmdline.h +++ b/src/goto-sea-sea/goto_cc_cmdline.h @@ -1,6 +1,6 @@ /*******************************************************************\ -Module: Command line interpretation for goto-cc +Module: Command line interpretation for goto-sea-sea Author: Daniel Kroening @@ -9,7 +9,7 @@ Date: April 2010 \*******************************************************************/ /// \file -/// Command line interpretation for goto-cc +/// Command line interpretation for goto-sea-sea #ifndef CPROVER_GOTO_CC_GOTO_CC_CMDLINE_H #define CPROVER_GOTO_CC_GOTO_CC_CMDLINE_H diff --git a/src/goto-cc/goto_cc_languages.cpp b/src/goto-sea-sea/goto_cc_languages.cpp similarity index 100% rename from src/goto-cc/goto_cc_languages.cpp rename to src/goto-sea-sea/goto_cc_languages.cpp diff --git a/src/goto-cc/goto_cc_main.cpp b/src/goto-sea-sea/goto_cc_main.cpp similarity index 98% rename from src/goto-cc/goto_cc_main.cpp rename to src/goto-sea-sea/goto_cc_main.cpp index 8d76e897c77..8872831db5b 100644 --- a/src/goto-cc/goto_cc_main.cpp +++ b/src/goto-sea-sea/goto_cc_main.cpp @@ -104,7 +104,7 @@ int main(int argc, const char **argv) } else if(base_name.find("goto-ld")!=std::string::npos) { - // this simulates "ld" for linking + // this simulates "ld" for inking ld_cmdlinet cmdline; gcc_modet gcc_mode(cmdline, base_name, true); return gcc_mode.main(argc, argv); diff --git a/src/goto-cc/goto_cc_mode.cpp b/src/goto-sea-sea/goto_cc_mode.cpp similarity index 96% rename from src/goto-cc/goto_cc_mode.cpp rename to src/goto-sea-sea/goto_cc_mode.cpp index b6802103f30..58a4c50bb5d 100644 --- a/src/goto-cc/goto_cc_mode.cpp +++ b/src/goto-sea-sea/goto_cc_mode.cpp @@ -47,7 +47,7 @@ void goto_cc_modet::help() std::cout << "\n" // NOLINTNEXTLINE(whitespace/line_length) - "* * goto-cc " CBMC_VERSION " - Copyright (C) 2006-2014 * *\n" + "* * goto-sea-sea " CBMC_VERSION " - Copyright (C) 2006-2014 * *\n" "* * Daniel Kroening, Christoph Wintersteiger * *\n" "* * kroening@kroening.com * *\n" "\n"; diff --git a/src/goto-cc/goto_cc_mode.h b/src/goto-sea-sea/goto_cc_mode.h similarity index 88% rename from src/goto-cc/goto_cc_mode.h rename to src/goto-sea-sea/goto_cc_mode.h index 6dbad84d3ce..1271326e646 100644 --- a/src/goto-cc/goto_cc_mode.h +++ b/src/goto-sea-sea/goto_cc_mode.h @@ -1,6 +1,6 @@ /*******************************************************************\ -Module: Command line interpretation for goto-cc. +Module: Command line interpretation for goto-sea-sea. Author: CM Wintersteiger @@ -9,7 +9,7 @@ Date: June 2006 \*******************************************************************/ /// \file -/// Command line interpretation for goto-cc. +/// Command line interpretation for goto-sea-sea. #ifndef CPROVER_GOTO_CC_GOTO_CC_MODE_H #define CPROVER_GOTO_CC_GOTO_CC_MODE_H diff --git a/src/goto-cc/ld_cmdline.cpp b/src/goto-sea-sea/ld_cmdline.cpp similarity index 100% rename from src/goto-cc/ld_cmdline.cpp rename to src/goto-sea-sea/ld_cmdline.cpp diff --git a/src/goto-cc/ld_cmdline.h b/src/goto-sea-sea/ld_cmdline.h similarity index 100% rename from src/goto-cc/ld_cmdline.h rename to src/goto-sea-sea/ld_cmdline.h diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-sea-sea/linker_script_merge.cpp similarity index 99% rename from src/goto-cc/linker_script_merge.cpp rename to src/goto-sea-sea/linker_script_merge.cpp index 72ec71f7ad3..ed0bfb9f384 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-sea-sea/linker_script_merge.cpp @@ -24,7 +24,7 @@ Author: Kareem Khazem , 2017 #include #include -#include +#include #include @@ -38,7 +38,7 @@ int linker_script_merget::add_linker_script_definitions() const std::string &elf_file=*elf_binaries.begin(); const std::string &goto_file=*goto_binaries.begin(); - temporary_filet linker_def_outfile("goto-cc-linker-info", ".json"); + temporary_filet linker_def_outfile("goto-sea-sea-linker-info", ".json"); std::list linker_defined_symbols; int fail= get_linker_script_data( @@ -677,7 +677,7 @@ int linker_script_merget::get_linker_script_data( debug() << "Linker-defined symbols: [" << linker_def_str.str() << "]\n" << eom; - temporary_filet linker_def_infile("goto-cc-linker-defs", ""); + temporary_filet linker_def_infile("goto-sea-sea-linker-defs", ""); std::ofstream linker_def_file(linker_def_infile()); linker_def_file << linker_def_str.str(); linker_def_file.close(); diff --git a/src/goto-cc/linker_script_merge.h b/src/goto-sea-sea/linker_script_merge.h similarity index 100% rename from src/goto-cc/linker_script_merge.h rename to src/goto-sea-sea/linker_script_merge.h diff --git a/src/goto-cc/ms_cl_cmdline.cpp b/src/goto-sea-sea/ms_cl_cmdline.cpp similarity index 100% rename from src/goto-cc/ms_cl_cmdline.cpp rename to src/goto-sea-sea/ms_cl_cmdline.cpp diff --git a/src/goto-cc/ms_cl_cmdline.h b/src/goto-sea-sea/ms_cl_cmdline.h similarity index 100% rename from src/goto-cc/ms_cl_cmdline.h rename to src/goto-sea-sea/ms_cl_cmdline.h diff --git a/src/goto-cc/ms_cl_mode.cpp b/src/goto-sea-sea/ms_cl_mode.cpp similarity index 100% rename from src/goto-cc/ms_cl_mode.cpp rename to src/goto-sea-sea/ms_cl_mode.cpp diff --git a/src/goto-cc/ms_cl_mode.h b/src/goto-sea-sea/ms_cl_mode.h similarity index 100% rename from src/goto-cc/ms_cl_mode.h rename to src/goto-sea-sea/ms_cl_mode.h diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index c000c3c5c0f..846755bb920 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -26,7 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include "goto_symex_state.h" diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp index 4b672574aab..2e2445a5c91 100644 --- a/src/goto-symex/symex_start_thread.cpp +++ b/src/goto-symex/symex_start_thread.cpp @@ -11,7 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_symex.h" -#include +#include void goto_symext::symex_start_thread(statet &state) { diff --git a/src/inking/CMakeLists.txt b/src/inking/CMakeLists.txt new file mode 100644 index 00000000000..d0247a41148 --- /dev/null +++ b/src/inking/CMakeLists.txt @@ -0,0 +1,6 @@ +file(GLOB_RECURSE sources "*.cpp" "*.h") +add_library(inking ${sources}) + +generic_includes(inking) + +target_link_libraries(inking util ansi-c) diff --git a/src/linking/Makefile b/src/inking/Makefile similarity index 73% rename from src/linking/Makefile rename to src/inking/Makefile index a2030500ec4..dcd7e5d0521 100644 --- a/src/linking/Makefile +++ b/src/inking/Makefile @@ -1,4 +1,4 @@ -SRC = linking.cpp \ +SRC = inking.cpp \ remove_internal_symbols.cpp \ static_lifetime_init.cpp \ zero_initializer.cpp \ @@ -9,11 +9,11 @@ INCLUDES= -I .. include ../config.inc include ../common -CLEANFILES = linking$(LIBEXT) +CLEANFILES = inking$(LIBEXT) -all: linking$(LIBEXT) +all: inking$(LIBEXT) ############################################################################### -linking$(LIBEXT): $(OBJ) +inking$(LIBEXT): $(OBJ) $(LINKLIB) diff --git a/src/linking/README.md b/src/inking/README.md similarity index 85% rename from src/linking/README.md rename to src/inking/README.md index 28c68ae21e6..abc28583186 100644 --- a/src/linking/README.md +++ b/src/inking/README.md @@ -1,7 +1,7 @@ \ingroup module_hidden -\defgroup linking linking +\defgroup inking inking -# Folder linking +# Folder inking \author Martin Brain diff --git a/src/linking/linking.cpp b/src/inking/linking.cpp similarity index 97% rename from src/linking/linking.cpp rename to src/inking/linking.cpp index e956867ebb0..ed531ca46e1 100644 --- a/src/linking/linking.cpp +++ b/src/inking/linking.cpp @@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// ANSI-C Linking -#include "linking.h" +#include "inking.h" #include #include @@ -24,9 +24,9 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "linking_class.h" +#include "inking_class.h" -std::string linkingt::expr_to_string( +std::string inkingt::expr_to_string( const namespacet &ns, const irep_idt &identifier, const exprt &expr) const @@ -34,7 +34,7 @@ std::string linkingt::expr_to_string( return from_expr(ns, identifier, expr); } -std::string linkingt::type_to_string( +std::string inkingt::type_to_string( const namespacet &ns, const irep_idt &identifier, const typet &type) const @@ -58,7 +58,7 @@ static const typet &follow_tags_symbols( return type; } -std::string linkingt::type_to_string_verbose( +std::string inkingt::type_to_string_verbose( const namespacet &ns, const symbolt &symbol, const typet &type) const @@ -112,7 +112,7 @@ std::string linkingt::type_to_string_verbose( return type_to_string(ns, symbol.name, type); } -void linkingt::detailed_conflict_report_rec( +void inkingt::detailed_conflict_report_rec( const symbolt &old_symbol, const symbolt &new_symbol, const typet &type1, @@ -366,7 +366,7 @@ void linkingt::detailed_conflict_report_rec( #endif } -void linkingt::link_error( +void inkingt::link_error( const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg) @@ -386,7 +386,7 @@ void linkingt::link_error( throw 0; } -void linkingt::link_warning( +void inkingt::link_warning( const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg) @@ -404,7 +404,7 @@ void linkingt::link_warning( << type_to_string_verbose(ns, new_symbol) << eom; } -irep_idt linkingt::rename(const irep_idt id) +irep_idt inkingt::rename(const irep_idt id) { unsigned cnt=0; @@ -422,13 +422,13 @@ irep_idt linkingt::rename(const irep_idt id) if(src_symbol_table.symbols.find(new_identifier)!= src_symbol_table.symbols.end()) - continue; // used by some earlier linking call already + continue; // used by some earlier inking call already return new_identifier; } } -bool linkingt::needs_renaming_non_type( +bool inkingt::needs_renaming_non_type( const symbolt &old_symbol, const symbolt &new_symbol) { @@ -442,7 +442,7 @@ bool linkingt::needs_renaming_non_type( return false; } -void linkingt::duplicate_code_symbol( +void inkingt::duplicate_code_symbol( symbolt &old_symbol, symbolt &new_symbol) { @@ -757,7 +757,7 @@ void linkingt::duplicate_code_symbol( } } -bool linkingt::adjust_object_type_rec( +bool inkingt::adjust_object_type_rec( const typet &t1, const typet &t2, adjust_type_infot &info) @@ -911,7 +911,7 @@ bool linkingt::adjust_object_type_rec( return true; } -bool linkingt::adjust_object_type( +bool inkingt::adjust_object_type( const symbolt &old_symbol, const symbolt &new_symbol, bool &set_to_new) @@ -926,7 +926,7 @@ bool linkingt::adjust_object_type( return result; } -void linkingt::duplicate_object_symbol( +void inkingt::duplicate_object_symbol( symbolt &old_symbol, symbolt &new_symbol) { @@ -1012,7 +1012,7 @@ void linkingt::duplicate_object_symbol( } } -void linkingt::duplicate_non_type_symbol( +void inkingt::duplicate_non_type_symbol( symbolt &old_symbol, symbolt &new_symbol) { @@ -1041,7 +1041,7 @@ void linkingt::duplicate_non_type_symbol( old_symbol.is_extern=old_symbol.is_extern && new_symbol.is_extern; } -void linkingt::duplicate_type_symbol( +void inkingt::duplicate_type_symbol( symbolt &old_symbol, const symbolt &new_symbol) { @@ -1118,7 +1118,7 @@ void linkingt::duplicate_type_symbol( "unexpected difference between type symbols"); } -bool linkingt::needs_renaming_type( +bool inkingt::needs_renaming_type( const symbolt &old_symbol, const symbolt &new_symbol) { @@ -1162,7 +1162,7 @@ bool linkingt::needs_renaming_type( return true; // different } -void linkingt::do_type_dependencies(id_sett &needs_to_be_renamed) +void inkingt::do_type_dependencies(id_sett &needs_to_be_renamed) { // Any type that uses a symbol that will be renamed also // needs to be renamed, and so on, until saturation. @@ -1214,7 +1214,7 @@ void linkingt::do_type_dependencies(id_sett &needs_to_be_renamed) } } -void linkingt::rename_symbols(const id_sett &needs_to_be_renamed) +void inkingt::rename_symbols(const id_sett &needs_to_be_renamed) { namespacet src_ns(src_symbol_table); @@ -1243,7 +1243,7 @@ void linkingt::rename_symbols(const id_sett &needs_to_be_renamed) } } -void linkingt::copy_symbols() +void inkingt::copy_symbols() { std::map src_symbols; // First apply the renaming @@ -1305,7 +1305,7 @@ void linkingt::copy_symbols() } } -void linkingt::typecheck() +void inkingt::typecheck() { // We do this in three phases. We first figure out which symbols need to // be renamed, and then build the renaming, and finally apply this @@ -1341,13 +1341,13 @@ void linkingt::typecheck() copy_symbols(); } -bool linking( +bool inking( symbol_tablet &dest_symbol_table, symbol_tablet &new_symbol_table, message_handlert &message_handler) { - linkingt linking( + inkingt inking( dest_symbol_table, new_symbol_table, message_handler); - return linking.typecheck_main(); + return inking.typecheck_main(); } diff --git a/src/linking/linking.h b/src/inking/linking.h similarity index 97% rename from src/linking/linking.h rename to src/inking/linking.h index b565a65231e..4079e2617e2 100644 --- a/src/linking/linking.h +++ b/src/inking/linking.h @@ -19,7 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com // applying appropriate renamings to symbols in "new_symbol_table" // when necessary. -bool linking( +bool inking( symbol_tablet &dest_symbol_table, symbol_tablet &new_symbol_table, message_handlert &message_handler); diff --git a/src/linking/linking_class.h b/src/inking/linking_class.h similarity index 98% rename from src/linking/linking_class.h rename to src/inking/linking_class.h index 70b59f59bc1..7cc1cbe8a26 100644 --- a/src/linking/linking_class.h +++ b/src/inking/linking_class.h @@ -18,10 +18,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -class linkingt:public typecheckt +class inkingt:public typecheckt { public: - linkingt( + inkingt( symbol_tablet &_main_symbol_table, symbol_tablet &_src_symbol_table, message_handlert &_message_handler): diff --git a/src/linking/remove_internal_symbols.cpp b/src/inking/remove_internal_symbols.cpp similarity index 100% rename from src/linking/remove_internal_symbols.cpp rename to src/inking/remove_internal_symbols.cpp diff --git a/src/linking/remove_internal_symbols.h b/src/inking/remove_internal_symbols.h similarity index 100% rename from src/linking/remove_internal_symbols.h rename to src/inking/remove_internal_symbols.h diff --git a/src/linking/static_lifetime_init.cpp b/src/inking/static_lifetime_init.cpp similarity index 99% rename from src/linking/static_lifetime_init.cpp rename to src/inking/static_lifetime_init.cpp index 8178f839ea1..020fe2fd5ea 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/src/inking/static_lifetime_init.cpp @@ -78,7 +78,7 @@ bool static_lifetime_init( identifier=="envp_size'") continue; - // just for linking + // just for inking if(has_prefix(id, CPROVER_PREFIX "architecture_")) continue; diff --git a/src/linking/static_lifetime_init.h b/src/inking/static_lifetime_init.h similarity index 100% rename from src/linking/static_lifetime_init.h rename to src/inking/static_lifetime_init.h diff --git a/src/linking/zero_initializer.cpp b/src/inking/zero_initializer.cpp similarity index 100% rename from src/linking/zero_initializer.cpp rename to src/inking/zero_initializer.cpp diff --git a/src/linking/zero_initializer.h b/src/inking/zero_initializer.h similarity index 100% rename from src/linking/zero_initializer.h rename to src/inking/zero_initializer.h diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 93a473cf9b4..b8e70c816c2 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -26,7 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include class java_bytecode_convert_classt:public messaget diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 7d4007add8a..daf5c4c81b6 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -31,7 +31,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include diff --git a/src/java_bytecode/java_bytecode_typecheck_expr.cpp b/src/java_bytecode/java_bytecode_typecheck_expr.cpp index 6fa16827fe9..498ed5cc42e 100644 --- a/src/java_bytecode/java_bytecode_typecheck_expr.cpp +++ b/src/java_bytecode/java_bytecode_typecheck_expr.cpp @@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include "java_pointer_casts.h" #include "java_types.h" diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index fb5561ae1c9..fdc068b571c 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -13,7 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index cad25eb6a16..3e5ce214b1f 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -23,7 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include diff --git a/src/java_bytecode/java_string_literals.cpp b/src/java_bytecode/java_string_literals.cpp index 5ec35ac0d6e..ef5daf5a3e9 100644 --- a/src/java_bytecode/java_string_literals.cpp +++ b/src/java_bytecode/java_string_literals.cpp @@ -11,7 +11,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include "java_types.h" #include "java_utils.h" -#include +#include #include #include diff --git a/src/jbmc/CMakeLists.txt b/src/jbmc/CMakeLists.txt index 4d29e360ad4..df33dd58182 100644 --- a/src/jbmc/CMakeLists.txt +++ b/src/jbmc/CMakeLists.txt @@ -14,13 +14,13 @@ target_link_libraries(jbmc-lib big-int cbmc-lib cpp - goto-instrument-lib + goto-inkstrument-lib goto-programs goto-symex java_bytecode json langapi - linking + inking pointer-analysis solvers util diff --git a/src/jbmc/Makefile b/src/jbmc/Makefile index 8d649d27731..2c1324c3710 100644 --- a/src/jbmc/Makefile +++ b/src/jbmc/Makefile @@ -4,7 +4,7 @@ SRC = jbmc_main.cpp \ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../java_bytecode/java_bytecode$(LIBEXT) \ - ../linking/linking$(LIBEXT) \ + ../inking/inking$(LIBEXT) \ ../big-int/big-int$(LIBEXT) \ ../goto-programs/goto-programs$(LIBEXT) \ ../goto-symex/goto-symex$(LIBEXT) \ @@ -17,19 +17,19 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../pointer-analysis/add_failed_symbols$(OBJEXT) \ ../pointer-analysis/rewrite_index$(OBJEXT) \ ../pointer-analysis/goto_program_dereference$(OBJEXT) \ - ../goto-instrument/full_slicer$(OBJEXT) \ - ../goto-instrument/reachability_slicer$(OBJEXT) \ - ../goto-instrument/nondet_static$(OBJEXT) \ - ../goto-instrument/cover$(OBJEXT) \ - ../goto-instrument/cover_basic_blocks$(OBJEXT) \ - ../goto-instrument/cover_filter$(OBJEXT) \ - ../goto-instrument/cover_instrument_branch$(OBJEXT) \ - ../goto-instrument/cover_instrument_condition$(OBJEXT) \ - ../goto-instrument/cover_instrument_decision$(OBJEXT) \ - ../goto-instrument/cover_instrument_location$(OBJEXT) \ - ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \ - ../goto-instrument/cover_instrument_other$(OBJEXT) \ - ../goto-instrument/cover_util$(OBJEXT) \ + ../goto-inkstrument/full_slicer$(OBJEXT) \ + ../goto-inkstrument/reachability_slicer$(OBJEXT) \ + ../goto-inkstrument/nondet_static$(OBJEXT) \ + ../goto-inkstrument/cover$(OBJEXT) \ + ../goto-inkstrument/cover_basic_blocks$(OBJEXT) \ + ../goto-inkstrument/cover_filter$(OBJEXT) \ + ../goto-inkstrument/cover_instrument_branch$(OBJEXT) \ + ../goto-inkstrument/cover_instrument_condition$(OBJEXT) \ + ../goto-inkstrument/cover_instrument_decision$(OBJEXT) \ + ../goto-inkstrument/cover_instrument_location$(OBJEXT) \ + ../goto-inkstrument/cover_instrument_mcdc$(OBJEXT) \ + ../goto-inkstrument/cover_instrument_other$(OBJEXT) \ + ../goto-inkstrument/cover_util$(OBJEXT) \ ../analyses/analyses$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ ../xmllang/xmllang$(LIBEXT) \ diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 25cce4cacd1..d26bca30f66 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -46,9 +46,9 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include -#include -#include +#include +#include +#include #include @@ -998,7 +998,36 @@ bool jbmc_parse_optionst::process_goto_functions( /// display command line help void jbmc_parse_optionst::help() { - std::cout << "\n" + std::cout << + "\n" + " _________ \n" + " _______. _ _ .___/ \ \n" + " / -_ / \ / \ / _ _ | \n" + " | _ _ \ | \/ | / / \/ \ | \n" + " | / \ / \| \ / | |.||.| / \n" + " | |.| |.|| \ / | \_/\_/ / \n" + " \_ \_/ \_// \ / \ ___ _/ \n" + " \ _/ \/ \_\_/ / \n" + " | \_/ ___\| / \n" + " ..____/_.. /.-_/o\____/.. \n" + " .. || o\o \~.o. //~ //..|| \\ .. \n" + " .. |/ .|| \\.. // || ..|| || .. \n" + " .. //o .o\\ || .. // // .. // || . \n" + " .. || .. \o \\ //. // .. || || .. \n" + " .. o// .. \\ ^\// .. // . |/ .\| .. \n" + " .. // .. || /\ .// .. // . \\ .. \n" + " .. |/ .. \| //\| || ../| .. || .. \n" + " o .. o l o //.. .|\ .. \\ .. \n" + " .. |/ .. |/ .. \| .. \n" + " o . o o \n" + " \n" + " ____________ ________ \n" + " |_ | ___ | \/ / __ \ \n" + " | | |_/ | . . | / \/ \n" + " | | ___ | |\/| | | \n" + " /\__/ | |_/ | | | | \__/\ \n" + " \____/\____/\_| |_/\____/ \n" + " \n" "* * JBMC " CBMC_VERSION " - Copyright (C) 2001-2018 "; std::cout << "(" << (sizeof(void *)*8) << "-bit version)"; diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h index 32f7e269465..9c5279a65d4 100644 --- a/src/jbmc/jbmc_parse_options.h +++ b/src/jbmc/jbmc_parse_options.h @@ -25,7 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include +#include #include diff --git a/src/linking/CMakeLists.txt b/src/linking/CMakeLists.txt deleted file mode 100644 index f33232fd156..00000000000 --- a/src/linking/CMakeLists.txt +++ /dev/null @@ -1,6 +0,0 @@ -file(GLOB_RECURSE sources "*.cpp" "*.h") -add_library(linking ${sources}) - -generic_includes(linking) - -target_link_libraries(linking util ansi-c) diff --git a/src/memory-models/Makefile b/src/memory-models/Makefile index 3b8587611c8..4fc595ca2e7 100644 --- a/src/memory-models/Makefile +++ b/src/memory-models/Makefile @@ -8,7 +8,7 @@ SRC = mm2cpp.cpp \ OBJ += ../big-int/big-int$(LIBEXT) \ ../ansi-c/ansi-c$(LIBEXT) \ - ../linking/linking$(LIBEXT) \ + ../inking/inking$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ ../util/util$(LIBEXT)