Skip to content

Commit 024d06f

Browse files
karkhazkarkhaz
committed
Make CBMC more fun
Summary: ======== - Add octopus ASCII art logos to CBMC and JBMC frontends - Change the names of some directories: "goto-instrument" is now "goto-inkstrument", "linking" is now "inking", "goto-cc" is now "goto-sea-sea", etc. ``` _________ _______. _ _ .___/ \ / -_ / \ / \ / _ _ | | _ _ \ | \/ | / / \/ \ | | / \ / \| \ / | |.||.| / | |.| |.|| \ / | \_/\_/ / \_ \_/ \_// \ / \ ___ _/ \ _/ \/ \_\_/ / | \_/ ___\| / ..____/_.. /.-_/o\____/.. .. || o\o \~.o. //~ //..|| \\ .. .. |/ .|| \\.. // || ..|| || .. .. //o .o\\ || .. // // .. // || . .. || .. \o \\ //. // .. || || .. .. o// .. \\ ^\// .. // . |/ .\| .. . // .. || /\ .// .. // . \\ .. . |/ .. \| //\| || ../| .. || .. o .. o l o //.. .|\ .. \\ .. .. |/ .. |/ .. \| .. o . o o ______________ ________ / __ | ___ | \/ / __ \ | / \| |_/ | . . | / \/ | | | ___ | |\/| | | | \__/| |_/ | | | | \__/\ \____\____/\_| |_/\____/ ``` Logo information: ================= The octopus on the left is the "model-checking octopus," and the one on the right is the "path exploration octopus". Their lovemaking symbolises the retrofitting of path-exploration functionality to CBMC in diffblue#1641. Rationale: ========== We're hoping to boost CBMC's uptake and retention amongst customers by adding a fun logo. The "mating octopi" logo was crafted during a several-month long rebranding and outreach effort. We found that customers form positive associations with tech brands that [feature](https://en.wikipedia.org/wiki/Tux_(mascot)) [cute](https://en.wikipedia.org/wiki/Docker_(software)) [animals](https://github.com/logos) as opposed to [fruits](https://www.apple.com/) or [rectangles](https://www.microsoft.com/en-gb). Members of the verification community have responded warmly to this proposed logo; below are a selection of quotes: This is a charming logo, I hope to see it when using CBMC to verify my latest sorting algorithm! Just to think, if only I had devised such a magnificent logo for my process calculus in the 80s, it would not have been usurped by Robin's bald-faced ripoff. -- Tony I like the idea, but don't eight-legged animals have a very large footprint? The logo is also off-centre, adding a proper frame would help here. Finally, the octopuses appear to be hopelessly tangled up and ought to be separated. Fortunately, I came up with a neat trick back in 2001 that could help you with all of these problems... -- Peter You're adding a _logo_ to a _verification tool_? Goto hell. -- Edsgar
1 parent 6ca3272 commit 024d06f

File tree

254 files changed

+416
-359
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

254 files changed

+416
-359
lines changed

‎src/CMakeLists.txt

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -90,7 +90,7 @@ add_subdirectory(goto-symex)
9090
add_subdirectory(jsil)
9191
add_subdirectory(json)
9292
add_subdirectory(langapi)
93-
add_subdirectory(linking)
93+
add_subdirectory(inking)
9494
add_subdirectory(memory-models)
9595
add_subdirectory(pointer-analysis)
9696
add_subdirectory(solvers)
@@ -102,7 +102,7 @@ add_subdirectory(clobber)
102102

103103
add_subdirectory(cbmc)
104104
add_subdirectory(jbmc)
105-
add_subdirectory(goto-cc)
106-
add_subdirectory(goto-instrument)
105+
add_subdirectory(goto-sea-sea)
106+
add_subdirectory(goto-inkstrument)
107107
add_subdirectory(goto-analyzer)
108108
add_subdirectory(goto-diff)

‎src/Makefile

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
1-
DIRS = ansi-c big-int cbmc jbmc cpp goto-cc goto-instrument goto-programs \
2-
goto-symex langapi pointer-analysis solvers util linking xmllang \
1+
DIRS = ansi-c big-int cbmc jbmc cpp goto-sea-sea goto-inkstrument goto-programs \
2+
goto-symex langapi pointer-analysis solvers util inking xmllang \
33
assembler analyses java_bytecode \
44
json goto-analyzer jsil goto-diff clobber \
55
memory-models miniz
66

7-
all: cbmc.dir jbmc.dir goto-cc.dir goto-instrument.dir \
7+
all: cbmc.dir jbmc.dir goto-sea-sea.dir goto-inkstrument.dir \
88
goto-analyzer.dir goto-diff.dir
99

1010
###############################################################################
@@ -17,32 +17,32 @@ $(patsubst %, %.dir, $(filter-out big-int util, $(DIRS))): util.dir
1717
.PHONY: languages
1818
.PHONY: clean
1919

20-
cpp.dir: ansi-c.dir linking.dir
20+
cpp.dir: ansi-c.dir inking.dir
2121

2222
java_bytecode.dir: miniz.dir
2323

2424
languages: util.dir langapi.dir \
2525
cpp.dir ansi-c.dir xmllang.dir assembler.dir java_bytecode.dir \
2626
jsil.dir
2727

28-
goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \
29-
goto-symex.dir linking.dir analyses.dir solvers.dir \
28+
goto-inkstrument.dir: languages goto-programs.dir pointer-analysis.dir \
29+
goto-symex.dir inking.dir analyses.dir solvers.dir \
3030
json.dir
3131

3232
cbmc.dir: languages solvers.dir goto-symex.dir analyses.dir \
33-
pointer-analysis.dir goto-programs.dir linking.dir \
34-
goto-instrument.dir
33+
pointer-analysis.dir goto-programs.dir inking.dir \
34+
goto-inkstrument.dir
3535

3636
jbmc.dir: java_bytecode.dir cbmc.dir
3737

38-
goto-analyzer.dir: languages analyses.dir goto-programs.dir linking.dir \
39-
json.dir goto-instrument.dir
38+
goto-analyzer.dir: languages analyses.dir goto-programs.dir inking.dir \
39+
json.dir goto-inkstrument.dir
4040

4141
goto-diff.dir: languages goto-programs.dir pointer-analysis.dir \
42-
linking.dir analyses.dir goto-instrument.dir \
42+
inking.dir analyses.dir goto-inkstrument.dir \
4343
solvers.dir json.dir goto-symex.dir
4444

45-
goto-cc.dir: languages pointer-analysis.dir goto-programs.dir linking.dir
45+
goto-sea-sea.dir: languages pointer-analysis.dir goto-programs.dir inking.dir
4646

4747
# building for a particular directory
4848

‎src/ansi-c/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -123,4 +123,4 @@ set_source_files_properties(
123123

124124
generic_includes(ansi-c)
125125

126-
target_link_libraries(ansi-c util linking goto-programs assembler)
126+
target_link_libraries(ansi-c util inking goto-programs assembler)

‎src/ansi-c/ansi_c_entry_point.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ Author: Daniel Kroening, [email protected]
2323
#include <util/symbol.h>
2424

2525
#include <goto-programs/goto_functions.h>
26-
#include <linking/static_lifetime_init.h>
26+
#include <inking/static_lifetime_init.h>
2727

2828
#include "c_nondet_symbol_factory.h"
2929

‎src/ansi-c/ansi_c_language.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,8 @@ Author: Daniel Kroening, [email protected]
1515
#include <util/config.h>
1616
#include <util/get_base_name.h>
1717

18-
#include <linking/linking.h>
19-
#include <linking/remove_internal_symbols.h>
18+
#include <inking/inking.h>
19+
#include <inking/remove_internal_symbols.h>
2020

2121
#include "ansi_c_entry_point.h"
2222
#include "ansi_c_typecheck.h"
@@ -118,7 +118,7 @@ bool ansi_c_languaget::typecheck(
118118

119119
remove_internal_symbols(new_symbol_table);
120120

121-
if(linking(symbol_table, new_symbol_table, get_message_handler()))
121+
if(inking(symbol_table, new_symbol_table, get_message_handler()))
122122
return true;
123123

124124
return false;

‎src/ansi-c/c_nondet_symbol_factory.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ Author: Diffblue Ltd.
2525
#include <util/std_types.h>
2626
#include <util/string_constant.h>
2727

28-
#include <linking/zero_initializer.h>
28+
#include <inking/zero_initializer.h>
2929

3030
#include <goto-programs/goto_functions.h>
3131

‎src/ansi-c/c_typecheck_base.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,7 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol)
5959
if(symbol.is_file_local)
6060
{
6161
// file-local stuff -- stays as is
62-
// collisions are resolved during linking
62+
// collisions are resolved during inking
6363
}
6464
else if(symbol.is_extern && !is_function)
6565
{

‎src/ansi-c/c_typecheck_code.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ Author: Daniel Kroening, [email protected]
1212
#include "c_typecheck_base.h"
1313

1414
#include <util/config.h>
15-
#include <linking/zero_initializer.h>
15+
#include <inking/zero_initializer.h>
1616

1717
#include "ansi_c_declaration.h"
1818

‎src/ansi-c/c_typecheck_initializer.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ Author: Daniel Kroening, [email protected]
2020
#include <util/string_constant.h>
2121
#include <util/type_eq.h>
2222

23-
#include <linking/zero_initializer.h>
23+
#include <inking/zero_initializer.h>
2424

2525
#include "anonymous_member.h"
2626

‎src/ansi-c/library/jsa.h

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -391,7 +391,7 @@ __CPROVER_jsa_inline _Bool __CPROVER_jsa__internal_is_in_valid_list(
391391
;
392392
#endif
393393

394-
__CPROVER_jsa_inline void __CPROVER_jsa__internal_assume_linking_correct(
394+
__CPROVER_jsa_inline void __CPROVER_jsa__internal_assume_inking_correct(
395395
const __CPROVER_jsa_abstract_heapt * const heap,
396396
const __CPROVER_jsa_node_id_t node_id,
397397
const __CPROVER_jsa_node_id_t prev,
@@ -419,7 +419,7 @@ __CPROVER_jsa_inline void __CPROVER_jsa__internal_assume_linking_correct(
419419
;
420420
#endif
421421

422-
__CPROVER_jsa_inline void __CPROVER_jsa__internal_assume_valid_iterator_linking(
422+
__CPROVER_jsa_inline void __CPROVER_jsa__internal_assume_valid_iterator_inking(
423423
const __CPROVER_jsa_abstract_heapt * const h,
424424
const __CPROVER_jsa_list_id_t list,
425425
const __CPROVER_jsa_node_id_t node_id,
@@ -596,7 +596,7 @@ __CPROVER_jsa_inline void __CPROVER_jsa_assume_valid_heap(
596596
__CPROVER_jsa_assume(h->list_head_nodes[node_list] == cnode);
597597
__CPROVER_jsa_assume(__CPROVER_jsa__internal_is_valid_node_id(nxt));
598598
__CPROVER_jsa_assume(__CPROVER_jsa__internal_is_valid_node_id(prev));
599-
__CPROVER_jsa__internal_assume_linking_correct(h, cnode, prev, nxt);
599+
__CPROVER_jsa__internal_assume_inking_correct(h, cnode, prev, nxt);
600600
}
601601
}
602602
#if 0 < __CPROVER_JSA_MAX_ABSTRACT_NODES
@@ -610,7 +610,7 @@ __CPROVER_jsa_inline void __CPROVER_jsa_assume_valid_heap(
610610
__CPROVER_jsa_assume(__CPROVER_jsa__internal_is_valid_node_id(prev));
611611
const __CPROVER_jsa_id_t nid=
612612
__CPROVER_jsa__internal_get_abstract_node_id(anode);
613-
__CPROVER_jsa__internal_assume_linking_correct(h, nid, prev, nxt);
613+
__CPROVER_jsa__internal_assume_inking_correct(h, nid, prev, nxt);
614614
}
615615
#endif
616616
#if 0 < __CPROVER_JSA_MAX_ABSTRACT_RANGES
@@ -644,9 +644,9 @@ __CPROVER_jsa_inline void __CPROVER_jsa_assume_valid_heap(
644644
else
645645
{
646646
__CPROVER_jsa_assume(list < h->list_count);
647-
__CPROVER_jsa__internal_assume_valid_iterator_linking(
647+
__CPROVER_jsa__internal_assume_valid_iterator_inking(
648648
h, list, next_node, next_index);
649-
__CPROVER_jsa__internal_assume_valid_iterator_linking(
649+
__CPROVER_jsa__internal_assume_valid_iterator_inking(
650650
h, list, prev_node, prev_index);
651651
if(__CPROVER_jsa_null!=next_node && __CPROVER_jsa_null != prev_node)
652652
__CPROVER_jsa__internal_assume_is_neighbour(

‎src/cbmc/CMakeLists.txt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,13 +13,13 @@ target_link_libraries(cbmc-lib
1313
assembler
1414
big-int
1515
cpp
16-
goto-instrument-lib
16+
goto-inkstrument-lib
1717
goto-programs
1818
goto-symex
1919
java_bytecode
2020
json
2121
langapi
22-
linking
22+
inking
2323
pointer-analysis
2424
solvers
2525
util

‎src/cbmc/Makefile

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ SRC = all_properties.cpp \
1818
OBJ += ../ansi-c/ansi-c$(LIBEXT) \
1919
../cpp/cpp$(LIBEXT) \
2020
../java_bytecode/java_bytecode$(LIBEXT) \
21-
../linking/linking$(LIBEXT) \
21+
../inking/inking$(LIBEXT) \
2222
../big-int/big-int$(LIBEXT) \
2323
../goto-programs/goto-programs$(LIBEXT) \
2424
../goto-symex/goto-symex$(LIBEXT) \
@@ -31,19 +31,19 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
3131
../pointer-analysis/add_failed_symbols$(OBJEXT) \
3232
../pointer-analysis/rewrite_index$(OBJEXT) \
3333
../pointer-analysis/goto_program_dereference$(OBJEXT) \
34-
../goto-instrument/reachability_slicer$(OBJEXT) \
35-
../goto-instrument/full_slicer$(OBJEXT) \
36-
../goto-instrument/nondet_static$(OBJEXT) \
37-
../goto-instrument/cover$(OBJEXT) \
38-
../goto-instrument/cover_basic_blocks$(OBJEXT) \
39-
../goto-instrument/cover_filter$(OBJEXT) \
40-
../goto-instrument/cover_instrument_branch$(OBJEXT) \
41-
../goto-instrument/cover_instrument_condition$(OBJEXT) \
42-
../goto-instrument/cover_instrument_decision$(OBJEXT) \
43-
../goto-instrument/cover_instrument_location$(OBJEXT) \
44-
../goto-instrument/cover_instrument_mcdc$(OBJEXT) \
45-
../goto-instrument/cover_instrument_other$(OBJEXT) \
46-
../goto-instrument/cover_util$(OBJEXT) \
34+
../goto-inkstrument/reachability_slicer$(OBJEXT) \
35+
../goto-inkstrument/full_slicer$(OBJEXT) \
36+
../goto-inkstrument/nondet_static$(OBJEXT) \
37+
../goto-inkstrument/cover$(OBJEXT) \
38+
../goto-inkstrument/cover_basic_blocks$(OBJEXT) \
39+
../goto-inkstrument/cover_filter$(OBJEXT) \
40+
../goto-inkstrument/cover_instrument_branch$(OBJEXT) \
41+
../goto-inkstrument/cover_instrument_condition$(OBJEXT) \
42+
../goto-inkstrument/cover_instrument_decision$(OBJEXT) \
43+
../goto-inkstrument/cover_instrument_location$(OBJEXT) \
44+
../goto-inkstrument/cover_instrument_mcdc$(OBJEXT) \
45+
../goto-inkstrument/cover_instrument_other$(OBJEXT) \
46+
../goto-inkstrument/cover_util$(OBJEXT) \
4747
../analyses/analyses$(LIBEXT) \
4848
../langapi/langapi$(LIBEXT) \
4949
../xmllang/xmllang$(LIBEXT) \

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 32 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -54,10 +54,10 @@ Author: Daniel Kroening, [email protected]
5454
#include <goto-symex/rewrite_union.h>
5555
#include <goto-symex/adjust_float_expressions.h>
5656

57-
#include <goto-instrument/reachability_slicer.h>
58-
#include <goto-instrument/full_slicer.h>
59-
#include <goto-instrument/nondet_static.h>
60-
#include <goto-instrument/cover.h>
57+
#include <goto-inkstrument/reachability_slicer.h>
58+
#include <goto-inkstrument/full_slicer.h>
59+
#include <goto-inkstrument/nondet_static.h>
60+
#include <goto-inkstrument/cover.h>
6161

6262
#include <pointer-analysis/add_failed_symbols.h>
6363

@@ -876,6 +876,34 @@ void cbmc_parse_optionst::help()
876876
// clang-format off
877877
std::cout <<
878878
"\n"
879+
" _________ \n"
880+
" _______. _ _ .___/ \ \n"
881+
" / -_ / \ / \ / _ _ | \n"
882+
" | _ _ \ | \/ | / / \/ \ | \n"
883+
" | / \ / \| \ / | |.||.| / \n"
884+
" | |.| |.|| \ / | \_/\_/ / \n"
885+
" \_ \_/ \_// \ / \ ___ _/ \n"
886+
" \ _/ \/ \_\_/ / \n"
887+
" | \_/ ___\| / \n"
888+
" ..____/_.. /.-_/o\____/.. \n"
889+
" .. || o\o \~.o. //~ //..|| \\ .. \n"
890+
" .. |/ .|| \\.. // || ..|| || .. \n"
891+
" .. //o .o\\ || .. // // .. // || . \n"
892+
" .. || .. \o \\ //. // .. || || .. \n"
893+
" .. o// .. \\ ^\// .. // . |/ .\| .. \n"
894+
" .. // .. || /\ .// .. // . \\ .. \n"
895+
" .. |/ .. \| //\| || ../| .. || .. \n"
896+
" o .. o l o //.. .|\ .. \\ .. \n"
897+
" .. |/ .. |/ .. \| .. \n"
898+
" o . o o \n"
899+
" \n"
900+
" ______________ ________ \n"
901+
" / __ | ___ | \/ / __ \ \n"
902+
" | / \| |_/ | . . | / \/ \n"
903+
" | | | ___ | |\/| | | \n"
904+
" | \__/| |_/ | | | | \__/\ \n"
905+
" \____\____/\_| |_/\____/ \n"
906+
" \n"
879907
"* * CBMC " CBMC_VERSION " - Copyright (C) 2001-2018 ";
880908

881909
std::cout << "(" << (sizeof(void *)*8) << "-bit version)";

‎src/cbmc/dist-linux

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -12,17 +12,17 @@ DEB_ARCH=`dpkg --print-architecture`
1212

1313
echo $VERSION_FILE
1414

15-
(cd ../goto-cc; make; strip goto-cc)
16-
(cd ../goto-instrument; make; strip goto-instrument)
15+
(cd ../goto-sea-sea; make; strip goto-sea-sea)
16+
(cd ../goto-inkstrument; make; strip goto-inkstrument)
1717

1818
mkdir /tmp/cbmc-dist
19-
cp ../cbmc/cbmc ../goto-cc/goto-cc \
20-
../goto-instrument/goto-instrument /tmp/cbmc-dist/
19+
cp ../cbmc/cbmc ../goto-sea-sea/goto-sea-sea \
20+
../goto-inkstrument/goto-inkstrument /tmp/cbmc-dist/
2121
cp ../../LICENSE /tmp/cbmc-dist/
2222
cp ../../doc/man/cbmc.1 /tmp/cbmc-dist/
2323
cd /tmp/cbmc-dist
2424
tar cfz cbmc-${VERSION_FILE}-linux-${BITS}.tgz cbmc \
25-
goto-cc goto-instrument LICENSE
25+
goto-sea-sea goto-inkstrument LICENSE
2626

2727
mkdir debian
2828
mkdir debian/DEBIAN
@@ -31,7 +31,7 @@ mkdir debian/usr/bin
3131
mkdir debian/usr/share
3232
mkdir debian/usr/share/man
3333
mkdir debian/usr/share/man/man1
34-
cp cbmc goto-cc goto-instrument \
34+
cp cbmc goto-sea-sea goto-inkstrument \
3535
debian/usr/bin/
3636
cp cbmc.1 debian/usr/share/man/man1
3737

‎src/cbmc/dist-macos

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ umask u=rwx,g=rx,o=rx
55

66
make cbmc-mac-signed
77

8-
(cd ../goto-cc; make goto-cc-mac-signed)
9-
(cd ../goto-instrument; make goto-instrument-mac-signed)
8+
(cd ../goto-sea-sea; make goto-sea-sea-mac-signed)
9+
(cd ../goto-inkstrument; make goto-inkstrument-mac-signed)
1010

1111
VERSION=`./cbmc --version`
1212
VERSION_FILE=`echo $VERSION | sed "y/./-/"`
@@ -22,8 +22,8 @@ mkdir /tmp/cbmc-dist/package-root/usr/local/bin
2222
mkdir /tmp/cbmc-dist/resources
2323
mkdir /tmp/cbmc-dist/resources/en.lproj
2424

25-
cp ../cbmc/cbmc ../goto-cc/goto-cc \
26-
../goto-instrument/goto-instrument /tmp/cbmc-dist/package-root/usr/local/bin/
25+
cp ../cbmc/cbmc ../goto-sea-sea/goto-sea-sea \
26+
../goto-inkstrument/goto-inkstrument /tmp/cbmc-dist/package-root/usr/local/bin/
2727
cp ../../LICENSE /tmp/cbmc-dist/resources/license.html
2828
cp distribution.xml /tmp/cbmc-dist/
2929

‎src/cbmc/dist-win

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,19 +8,19 @@ VERSION_FILE=`echo $VERSION | sed "y/./-/"`
88

99
echo $VERSION_FILE
1010

11-
(cd ../goto-cc; make; strip goto-cc.exe ; cp goto-cc.exe goto-cl.exe)
12-
(cd ../goto-instrument; make; strip goto-instrument.exe)
11+
(cd ../goto-sea-sea; make; strip goto-sea-sea.exe ; cp goto-sea-sea.exe goto-cl.exe)
12+
(cd ../goto-inkstrument; make; strip goto-inkstrument.exe)
1313

1414
mkdir /tmp/cbmc-dist
1515
cp ../cbmc/cbmc.exe \
16-
../goto-cc/goto-cl.exe ../goto-instrument/goto-instrument.exe \
16+
../goto-sea-sea/goto-cl.exe ../goto-inkstrument/goto-inkstrument.exe \
1717
/tmp/cbmc-dist/
1818
cp ~/progr/cbmc.vs64/src/cbmc/cbmc.exe /tmp/cbmc-dist/cbmc64.exe
1919
cp ../../LICENSE /tmp/cbmc-dist/LICENSE.txt
2020
unix2dos /tmp/cbmc-dist/LICENSE.txt
2121
cd /tmp/cbmc-dist
2222
zip -9 cbmc-${VERSION_FILE}-win.zip cbmc.exe \
23-
cbmc64.exe goto-instrument.exe goto-cl.exe LICENSE.txt
23+
cbmc64.exe goto-inkstrument.exe goto-cl.exe LICENSE.txt
2424

2525
echo Copying.
2626
scp cbmc-${VERSION_FILE}-win.zip [email protected]:/srv/www/cprover.org/cbmc/download/

‎src/clobber/CMakeLists.txt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ generic_includes(clobber-lib)
1010
target_link_libraries(clobber-lib
1111
ansi-c
1212
cpp
13-
linking
13+
inking
1414
big-int
1515
goto-programs
1616
analyses
@@ -21,7 +21,7 @@ target_link_libraries(clobber-lib
2121
util
2222
goto-symex
2323
pointer-analysis
24-
goto-instrument-lib
24+
goto-inkstrument-lib
2525
)
2626

2727
add_if_library(clobber-lib bv_refinement)

0 commit comments

Comments
 (0)