Skip to content

Commit b0a390e

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 [https://www.apple.com/](fruits) or [https://www.microsoft.com/en-gb](rectangles). 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 have soundly beaten 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 b0a390e

File tree

262 files changed

+540
-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.

262 files changed

+540
-359
lines changed

‎regression/cbmc-path-strategies/if/fifo.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
main.c
3+
--paths fifo
4+
activate-multi-line-match
5+
EXIT=0
6+
SIGNAL=0
7+
BMC at file[^\n]+line 4 function \w+\nSaving next instruction 'file[^\n]+line 5 function \w+'\nSaving jump target 'file[^\n]+line 7 function \w+'(.|\n)+BMC at file[^\n]+line 4 function \w+\nResuming from next instruction 'file[^\n]+line 5 function \w+'\nBMC at file[^\n]+line 5 function \w+(.|\n)+VERIFICATION SUCCESSFUL(.|\n)+BMC at file[^\n]+line 4 function \w+\nResuming from jump target 'file[^\n]+line 7 function \w+'\nBMC at file[^\n]+line 7 function \w+(.|\n)+VERIFICATION SUCCESSFUL\n
8+
--
9+
^warning: ignoring
10+
--
11+
This tests that the next path is resumed before the jump path.
12+
13+
WARNING:
14+
This .desc file is automatically generated
15+
from the file 'if/fifo.in'.
16+
Do not modify this file.

‎regression/cbmc-path-strategies/if/progressive-fifo.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
main.c
3+
--paths progressive-fifo
4+
activate-multi-line-match
5+
EXIT=0
6+
SIGNAL=0
7+
BMC at file[^\n]+line 4 function \w+\nSaving next instruction 'file[^\n]+line 5 function \w+'\nSaving jump target 'file[^\n]+line 7 function \w+'(.|\n)+BMC at file[^\n]+line 4 function \w+\nResuming from jump target 'file[^\n]+line 7 function \w+'\nBMC at file[^\n]+line 7 function \w+(.|\n)+VERIFICATION SUCCESSFUL(.|\n)+BMC at file[^\n]+line 4 function \w+\nResuming from next instruction 'file[^\n]+line 5 function \w+'\nBMC at file[^\n]+line 5 function \w+(.|\n)+VERIFICATION SUCCESSFUL\n
8+
--
9+
^warning: ignoring
10+
--
11+
This tests that the next path is resumed before the jump path.
12+
13+
WARNING:
14+
This .desc file is automatically generated
15+
from the file 'if/progressive-fifo.in'.
16+
Do not modify this file.

‎regression/cbmc-path-strategies/loop-functional-correctness/fifo.desc

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE
2+
main.c
3+
--unwind 2 --paths fifo
4+
activate-multi-line-match
5+
SIGNAL=0
6+
EXIT=10
7+
BMC at file[^\n]+line 6 function \w+\nSaving next instruction 'file[^\n]+line 7 function \w+'\nSaving jump target 'file[^\n]+line 9 function \w+'(.|\n)+BMC at file[^\n]+line 6 function \w+\nResuming from next instruction 'file[^\n]+line 7 function \w+'\nBMC at file[^\n]+line 7 function \w+(.|\n)+Saving next instruction 'file[^\n]+line 7 function \w+'\nSaving jump target 'file[^\n]+line 9 function \w+'(.|\n)+BMC at file[^\n]+line 6 function \w+\nResuming from jump target 'file[^\n]+line 9 function \w+'\nBMC at file[^\n]+line 9 function \w+(.|\n)+VERIFICATION SUCCESSFUL(.|\n)+BMC at file[^\n]+line 6 function \w+\nResuming from next instruction 'file[^\n]+line 7 function \w+'\nBMC at file[^\n]+line 7 function \w+(.|\n)+VERIFICATION SUCCESSFUL(.|\n)+BMC at file[^\n]+line 6 function \w+\nResuming from jump target 'file[^\n]+line 9 function \w+'\nBMC at file[^\n]+line 9 function \w+(.|\n)+VERIFICATION FAILED\n[^.]
8+
--
9+
^warning: ignoring
10+
--
11+
12+
WARNING:
13+
This .desc file is automatically generated
14+
from the file 'loop-functional-correctness/fifo.in'.
15+
Do not modify this file.

‎regression/cbmc-path-strategies/loop-functional-correctness/progressive-fifo.desc

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE
2+
main.c
3+
--unwind 2 --paths progressive-fifo
4+
activate-multi-line-match
5+
SIGNAL=0
6+
EXIT=10
7+
BMC at file[^\n]+line 6 function \w+\nSaving next instruction 'file[^\n]+line 7 function \w+'\nSaving jump target 'file[^\n]+line 9 function \w+'(.|\n)+BMC at file[^\n]+line 6 function \w+\nResuming from jump target 'file[^\n]+line 9 function \w+'\nBMC at file[^\n]+line 9 function \w+(.|\n)+VERIFICATION SUCCESSFUL(.|\n)+BMC at file[^\n]+line 6 function \w+\nResuming from next instruction 'file[^\n]+line 7 function \w+'\nBMC at file[^\n]+line 7 function \w+(.|\n)+Saving next instruction 'file[^\n]+line 7 function \w+'\nSaving jump target 'file[^\n]+line 9 function \w+'(.|\n)+BMC at file[^\n]+line 6 function \w+\nResuming from jump target 'file[^\n]+line 9 function \w+'\nBMC at file[^\n]+line 9 function \w+(.|\n)+VERIFICATION FAILED(.|\n)+BMC at file[^\n]+line 6 function \w+\nResuming from next instruction 'file[^\n]+line 7 function \w+'\nBMC at file[^\n]+line 7 function \w+(.|\n)+VERIFICATION SUCCESSFUL\n[^.]
8+
--
9+
^warning: ignoring
10+
--
11+
This strategy differs from 'fifo' because the failed path is the second
12+
one, not the last one.
13+
14+
WARNING:
15+
This .desc file is automatically generated
16+
from the file 'loop-functional-correctness/progressive-fifo.in'.
17+
Do not modify this file.

‎regression/cbmc-path-strategies/nested-if/fifo.desc

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE
2+
main.c
3+
--paths fifo
4+
activate-multi-line-match
5+
EXIT=0
6+
SIGNAL=0
7+
BMC at file[^\n]+line 4 function \w+\nSaving next instruction 'file[^\n]+line 6 function \w+'\nSaving jump target 'file[^\n]+line 13 function \w+'(.|\n)+BMC at file[^\n]+line 4 function \w+\nResuming from next instruction 'file[^\n]+line 6 function \w+'\nBMC at file[^\n]+line 6 function \w+\nSaving next instruction 'file[^\n]+line 7 function \w+'\nSaving jump target 'file[^\n]+line 9 function \w+'(.|\n)+BMC at file[^\n]+line 4 function \w+\nResuming from jump target 'file[^\n]+line 13 function \w+'\nBMC at file[^\n]+line 13 function \w+\nSaving next instruction 'file[^\n]+line 14 function \w+'\nSaving jump target 'file[^\n]+line 16 function \w+'(.|\n)+BMC at file[^\n]+line 6 function \w+\nResuming from next instruction 'file[^\n]+line 7 function \w+'\nBMC at file[^\n]+line 7 function \w+(.|\n)+VERIFICATION SUCCESSFUL(.|\n)+BMC at file[^\n]+line 6 function \w+\nResuming from jump target 'file[^\n]+line 9 function \w+'\nBMC at file[^\n]+line 9 function \w+(.|\n)+VERIFICATION SUCCESSFUL(.|\n)+BMC at file[^\n]+line 13 function \w+\nResuming from next instruction 'file[^\n]+line 14 function \w+'\nBMC at file[^\n]+line 14 function \w+(.|\n)+VERIFICATION SUCCESSFUL(.|\n)+BMC at file[^\n]+line 13 function \w+\nResuming from jump target 'file[^\n]+line 16 function \w+'\nBMC at file[^\n]+line 16 function \w+(.|\n)+VERIFICATION SUCCESSFUL\n[^.]
8+
--
9+
^warning: ignoring
10+
--
11+
12+
WARNING:
13+
This .desc file is automatically generated
14+
from the file 'nested-if/fifo.in'.
15+
Do not modify this file.

‎regression/cbmc-path-strategies/nested-if/progressive-fifo.desc

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE
2+
main.c
3+
--paths progressive-fifo
4+
activate-multi-line-match
5+
EXIT=0
6+
SIGNAL=0
7+
BMC at file[^\n]+line 4 function \w+\nSaving next instruction 'file[^\n]+line 6 function \w+'\nSaving jump target 'file[^\n]+line 13 function \w+'(.|\n)+BMC at file[^\n]+line 4 function \w+\nResuming from jump target 'file[^\n]+line 13 function \w+'\nBMC at file[^\n]+line 13 function \w+\nSaving next instruction 'file[^\n]+line 14 function \w+'\nSaving jump target 'file[^\n]+line 16 function \w+'(.|\n)+BMC at file[^\n]+line 13 function \w+\nResuming from jump target 'file[^\n]+line 16 function \w+'\nBMC at file[^\n]+line 16 function \w+(.|\n)+VERIFICATION SUCCESSFUL(.|\n)+BMC at file[^\n]+line 4 function \w+\nResuming from next instruction 'file[^\n]+line 6 function \w+'\nBMC at file[^\n]+line 6 function \w+\nSaving next instruction 'file[^\n]+line 7 function \w+'\nSaving jump target 'file[^\n]+line 9 function \w+'(.|\n)+BMC at file[^\n]+line 6 function \w+\nResuming from jump target 'file[^\n]+line 9 function \w+'\nBMC at file[^\n]+line 9 function \w+(.|\n)+VERIFICATION SUCCESSFUL(.|\n)+BMC at file[^\n]+line 13 function \w+\nResuming from next instruction 'file[^\n]+line 14 function \w+'\nBMC at file[^\n]+line 14 function \w+(.|\n)+VERIFICATION SUCCESSFUL(.|\n)+BMC at file[^\n]+line 6 function \w+\nResuming from next instruction 'file[^\n]+line 7 function \w+'\nBMC at file[^\n]+line 7 function \w+(.|\n)+VERIFICATION SUCCESSFUL\n[^.]
8+
--
9+
^warning: ignoring
10+
--
11+
12+
WARNING:
13+
This .desc file is automatically generated
14+
from the file 'nested-if/progressive-fifo.in'.
15+
Do not modify this file.

‎regression/cbmc-path-strategies/simple-loop/fifo.desc

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE
2+
main.c
3+
--unwind 2 --paths fifo
4+
activate-multi-line-match
5+
EXIT=0
6+
SIGNAL=0
7+
Saving next instruction 'file[^\n]+line 6 function \w+'\nSaving jump target 'file[^\n]+line 8 function \w+'(.|\n)+BMC at file[^\n]+line 4 function \w+\nResuming from next instruction 'file[^\n]+line 6 function \w+'\nBMC at file[^\n]+line 6 function \w+(.|\n)+Saving next instruction 'file[^\n]+line 6 function \w+'\nSaving jump target 'file[^\n]+line 8 function \w+'(.|\n)+BMC at file[^\n]+line 4 function \w+\nResuming from jump target 'file[^\n]+line 8 function \w+'(.|\n)+VERIFICATION SUCCESSFUL(.|\n)+BMC at file[^\n]+line 4 function \w+\nResuming from next instruction 'file[^\n]+line 6 function \w+'\nBMC at file[^\n]+line 6 function \w+(.|\n)+VERIFICATION SUCCESSFUL(.|\n)+BMC at file[^\n]+line 4 function \w+\nResuming from jump target 'file[^\n]+line 8 function \w+'\nBMC at file[^\n]+line 8 function \w+(.|\n)+VERIFICATION SUCCESSFUL\n
8+
--
9+
^warning: ignoring
10+
--
11+
12+
WARNING:
13+
This .desc file is automatically generated
14+
from the file 'simple-loop/fifo.in'.
15+
Do not modify this file.

‎regression/cbmc-path-strategies/simple-loop/progressive-fifo.desc

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE
2+
main.c
3+
--unwind 2 --paths progressive-fifo
4+
activate-multi-line-match
5+
EXIT=0
6+
SIGNAL=0
7+
BMC at file[^\n]+line 4 function \w+\nSaving next instruction 'file[^\n]+line 6 function \w+'\nSaving jump target 'file[^\n]+line 8 function \w+'(.|\n)+BMC at file[^\n]+line 4 function \w+\nResuming from jump target 'file[^\n]+line 8 function \w+'\nBMC at file[^\n]+line 8 function \w+(.|\n)+VERIFICATION SUCCESSFUL(.|\n)+BMC at file[^\n]+line 4 function \w+\nResuming from next instruction 'file[^\n]+line 6 function \w+'\nBMC at file[^\n]+line 6 function \w+(.|\n)+Saving next instruction 'file[^\n]+line 6 function \w+'\nSaving jump target 'file[^\n]+line 8 function \w+'(.|\n)+BMC at file[^\n]+line 4 function \w+\nResuming from jump target 'file[^\n]+line 8 function \w+'\nBMC at file[^\n]+line 8 function \w+(.|\n)+VERIFICATION SUCCESSFUL(.|\n)+BMC at file[^\n]+line 4 function \w+\nResuming from next instruction 'file[^\n]+line 6 function \w+'\nBMC at file[^\n]+line 6 function \w+(.|\n)+VERIFICATION SUCCESSFUL\n[^.]
8+
--
9+
^warning: ignoring
10+
--
11+
12+
WARNING:
13+
This .desc file is automatically generated
14+
from the file 'simple-loop/progressive-fifo.in'.
15+
Do not modify this file.

‎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) \

0 commit comments

Comments
 (0)