diffblue · tautschnig · Jun 23, 2022 · Jun 21, 2022 · Jun 23, 2022
@@ -467,7 +467,7 @@ $ goto-cc -o main.gb main.c
 
 $ goto-harness \
   --harness-function-name harness \
-  --harness-type initialise-with-memory-snapshot \
+  --harness-type initialize-with-memory-snapshot \
   --memory-snapshot snapshot.json \
   --initial-source-location main.c:46 \
   --havoc-variables x \

@@ -0,0 +1,133 @@
+.TH GOTO-HARNESS "1" "June 2022" "goto-harness-5.59.0" "User Commands"
+.SH NAME
+goto-harness \- Generate environments for symbolic analysis
+.SH SYNOPSIS
+.TP
+.B goto\-harness [\-?] [\-h] [\-\-help]
+show help
+.TP
+.B goto\-harness \fB\-\-version\fR
+show version
+.TP
+.B goto\-harness \fIin\fB \fIout\fB \-\-harness\-function\-name\ \fIname\fB \-\-harness\-type \fIharness\-type\fR [\fBharness-options\fR]
+build harness for \fIin\fR and write harness to \fIout\fR; the harness is
+printed as C code, if \fIout\fR has a .c suffix, else a goto binary including
+the harness is generated
+.SH DESCRIPTION
+\fBgoto\-harness\fR constructs functions that set up an appropriate environment
+before calling functions under analysis. This is most useful when trying to
+analyze an isolated unit of a program.
+.PP
+A typical sequence of tool invocations is
+as follows. Given a C program \fIprogram.c\fR, we generate a harness for
+function \fItest_function\fR:
+.EX
+.IP
+# Compile the program
+goto-cc program.c -o program.gb
+# Run goto-harness to produce harness file
+goto-harness --harness-type call-function --harness-function-name generated_harness_test_function
+  --function test_function program.gb harness.c
+# Run the checks targeting the generated harness
+cbmc --pointer-check harness.c --function generated_harness_test_function
+.EE
+.PP
+\fBgoto\-harness\fR has two main modes of operation. First,function-call harnesses,
+which automatically synthesize an environment without having any information
+about the program state. Second, memory-snapshot harnesses, in which case
+\fBgoto\-harness\fR loads an existing program state as generated by
+\fBmemory-analyzer\fR(1) and selectively havocs some variables.
+.SH OPTIONS
+.TP
+\fB\-\-harness\-function\-name\fR \fIname\fR
+Use \fIname\fR as the name of the harness function that is generated, i.e., the
+new entry point.
+.TP
+\fB\-\-harness\-type\fR [\fBcall-function\fR|\fBinitialize-with-memory-snapshot\fR]
+Select the type of harness to generate. In addition to options applicable to
+both harness generators, each of them also has dedicated options that are
+described below.
+.SS "Common generator options"
+.TP
+\fB\-\-min\-null\-tree\-depth\fR \fIN\fR
+Set the minimum level at which a pointer can first be \fBNULL\fR
+in a recursively non-deterministically initialized struct to \fIN\fR. Defaults
+to 1.
+.TP
+\fB\-\-max\-nondet\-tree\-depth\fR \fIN\fR
+Set the maximum height of the non-deterministic object tree to \fIN\fR. At that
+level, all pointers will be set to \fBNULL\fR. Defaults to 2.
+.TP
+\fB\-\-min\-array\-size\fR \fIN\fR
+Set the minimum size of arrays of non-constant size allocated by the harness to
+\fIN\fR. Defaults to 1.
+.TP
+\fB\-\-max\-array\-size\fR N
+Set the maximum size of arrays of non-constant size allocated by the harness to
+\fIN\fR. Defaults to 2.
+.TP
+\fB\-\-nondet\-globals\fR
+Set global variables to non-deterministic values in harness.
+.TP
+\fB\-\-havoc\-member\fR \fImember\-expr\fR
+Non-deterministically initialize \fImember\-expr\fR of some global object (may
+be given multiple times).
+.TP
+\fB\-\-function\-pointer\-can\-be\-null\fR \fIfunction\-name\fR
+Name of parameters of the target function or of global variables of
+function-pointer type that can non-deterministically be set to \fBNULL\fR.
+.SS "Function harness generator (\fB\-\-harness\-type call-function\fR):"
+.TP
+\fB\-\-function\fR \fIfunction\-name\fR
+Generate an environment to call function \fIfunction\-name\fR, which the harness
+will then call.
+.TP
+\fB\-\-treat\-pointer\-as\-array\fR \fIp\fR
+Treat the (pointer-typed) function parameter with name \fIp\fR as an array.
+.TP
+\fB\-\-associated\-array\-size\fR \fIarray_name\fR:\fIsize_name\fR
+Set the function parameter \fIsize_name\fR to the size of the array parameter
+\fIarray_name\fR (implies \fB\-\-treat\-pointer\-as\-array \fIarray_name\fR).
+.TP
+\fB\-\-treat\-pointers\-equal\fR \fIp\fR,\fIq\fR,\fIr\fR[;\fIs\fR,\fIt\fR]
+Assume the pointer-typed function parameters \fIq\fR and \fIr\fR are equal to
+parameter \fIp\fR, and \fIs\fR equal to \fIt\fR, and so on.
+.TP
+\fB\-\-treat\-pointers\-equal\-maybe\fR
+Function parameter equality is non\-deterministic.
+.TP
+\fB\-\-treat\-pointer\-as\-cstring\fR \fIp\fR
+Treat the function parameter with the name \fIp\fR as a string of characters.
+.SS "Memory snapshot harness generator (\fB\-\-harness\-type initialise\-from\-memory\-snapshot\fR):"
+.TP
+\fB\-\-memory\-snapshot\fR \fIfile\fR
+Initialize memory from JSON memory snapshot stored in \fIfile\fR.
+.TP
+\fB\-\-initial\-goto\-location\fR \fIfunc\fR[:\fIn\fR]
+Use function \fIfunc\fR and goto binary location number \fIn\fR as entry point.
+.TP
+\fB\-\-initial\-source\-location\fR \fIfile\R:\fIn\fR
+Use given file name \fIfile\fR and line number \fIn\R in that file as entry
+point.
+.TP
+\fB\-\-havoc\-variables\fR \fIvars\fR
+Non-deterministically initialize all symbols named \fIvars\fR.
+.TP
+\fB\-\-pointer\-as\-array\fR \fIp\fR
+Treat the global pointer with name \fIp\fR as an array.
+.TP
+\fB\-\-size\-of\-array\fR \fIarray_name\fR:\fIsize_name\fR
+Set the variable \fIsize_name\fR to the size of the array variable
+\fIarray_name\fR (implies \fB\-\-pointer\-as\-array \fIarray_name\fR).
+.SH ENVIRONMENT
+All tools honor the TMPDIR environment variable when generating temporary
+files and directories.
+.SH BUGS
+If you encounter a problem please create an issue at
+.B https://github.com/diffblue/cbmc/issues
+.SH SEE ALSO
+.BR cbmc (1),
+.BR goto-cc (1),
+.BR memory-analyzer (1)
+.SH COPYRIGHT
+2019, Diffblue
diff --git a/regression/goto-harness/havoc-global-int-01/test.desc b/regression/goto-harness/havoc-global-int-01/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0 --havoc-variables x
+--harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0 --havoc-variables x
 ^EXIT=10$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion x == 1: FAILURE

diff --git a/regression/goto-harness/havoc-global-int-02/test.desc b/regression/goto-harness/havoc-global-int-02/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-y-snapshot.json --initial-goto-location main:7 --havoc-variables y
+harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-y-snapshot.json --initial-goto-location main:7 --havoc-variables y
 ^\[main.assertion.1\] line \d+ assertion y \+ 2 > y: FAILURE$
 ^\[main.assertion.2\] line \d+ assertion 0: FAILURE$
 ^EXIT=10$

diff --git a/regression/goto-harness/havoc-global-int-03/test.desc b/regression/goto-harness/havoc-global-int-03/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-source-location main.c:6 --havoc-variables x
+harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-source-location main.c:6 --havoc-variables x
 ^EXIT=10$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS

diff --git a/regression/goto-harness/havoc-global-struct/test.desc b/regression/goto-harness/havoc-global-struct/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-struct-snapshot.json --initial-goto-location main:3 --havoc-variables simple
+harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-struct-snapshot.json --initial-goto-location main:3 --havoc-variables simple
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] line \d+ assertion simple.j > simple.i: FAILURE$

diff --git a/regression/goto-harness/load-snapshot-recursive-static-global-int-01/test.desc b/regression/goto-harness/load-snapshot-recursive-static-global-int-01/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:1
+harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:1
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

diff --git a/regression/goto-harness/load-snapshot-static-global-array-01/test.desc b/regression/goto-harness/load-snapshot-static-global-array-01/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:0
+harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:0
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

diff --git a/regression/goto-harness/load-snapshot-static-global-int-01/test.desc b/regression/goto-harness/load-snapshot-static-global-int-01/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0
+harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

diff --git a/regression/goto-harness/load-snapshot-static-global-int-02/test.desc b/regression/goto-harness/load-snapshot-static-global-int-02/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0
+harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0
 ^EXIT=10$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS

diff --git a/regression/goto-harness/load-snapshot-static-global-int-03/test.desc b/regression/goto-harness/load-snapshot-static-global-int-03/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0
+harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:0
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

diff --git a/regression/goto-harness/load-snapshot-static-global-int-04/test.desc b/regression/goto-harness/load-snapshot-static-global-int-04/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:1
+harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-goto-location main:1
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

diff --git a/regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc b/regression/goto-harness/load-snapshot-static-global-pointer-01/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-harness.gb --harness-type initialise-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:0
+harness.gb --harness-type initialize-with-memory-snapshot --memory-snapshot snapshot.json --initial-goto-location main:0
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

diff --git a/regression/snapshot-harness/arrays_01/test.desc b/regression/snapshot-harness/arrays_01/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-array,p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+array,p,q --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion p == \&\(array\[1\]\): SUCCESS

diff --git a/regression/snapshot-harness/arrays_02/test.desc b/regression/snapshot-harness/arrays_02/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+p,q --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion p == q: SUCCESS

diff --git a/regression/snapshot-harness/dynamic-array-int-ordering/test.desc b/regression/snapshot-harness/dynamic-array-int-ordering/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-a,a1,iterator1,a2,a3,iterator2,a4,a5,iterator3,a6,a7,array2,a8 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+a,a1,iterator1,a2,a3,iterator2,a4,a5,iterator3,a6,a7,array2,a8 --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=10$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion \*iterator1 == 1: SUCCESS

diff --git a/regression/snapshot-harness/dynamic-array-int/test.desc b/regression/snapshot-harness/dynamic-array-int/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-array,iterator1,iterator2,iterator3 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+array,iterator1,iterator2,iterator3 --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=10$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion \*iterator1 == 1: SUCCESS

diff --git a/regression/snapshot-harness/function_pointer_01/test.desc b/regression/snapshot-harness/function_pointer_01/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-fun_ptr --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+fun_ptr --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion fun_ptr == \&foo: SUCCESS

diff --git a/regression/snapshot-harness/function_pointer_02/test.desc b/regression/snapshot-harness/function_pointer_02/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-fun_ptr1,fun_ptr2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+fun_ptr1,fun_ptr2 --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion fun_ptr1 == \&plus: SUCCESS

diff --git a/regression/snapshot-harness/function_pointer_03/test.desc b/regression/snapshot-harness/function_pointer_03/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-fun_array,fun_ptr1,fun_ptr2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+fun_array,fun_ptr1,fun_ptr2 --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion fun_ptr1 == \&plus: SUCCESS

diff --git a/regression/snapshot-harness/nondet_initialize_static_arrays/test.desc b/regression/snapshot-harness/nondet_initialize_static_arrays/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --min-null-tree-depth 10 --max-nondet-tree-depth 4 --havoc-variables p
+p --harness-type initialize-with-memory-snapshot --initial-goto-location main:4 --min-null-tree-depth 10 --max-nondet-tree-depth 4 --havoc-variables p
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

diff --git a/regression/snapshot-harness/pointer-function-parameters-struct-mutual-recursion/test.desc b/regression/snapshot-harness/pointer-function-parameters-struct-mutual-recursion/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables p --min-null-tree-depth 10 --max-nondet-tree-depth 3
+p --harness-type initialize-with-memory-snapshot --initial-goto-location main:4 --havoc-variables p --min-null-tree-depth 10 --max-nondet-tree-depth 3
 ^SIGNAL=0$
 ^EXIT=0$
 VERIFICATION SUCCESSFUL

diff --git a/regression/snapshot-harness/pointer-to-array-char/test.desc b/regression/snapshot-harness/pointer-to-array-char/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-first,second,array_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+first,second,array_size --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
 ^SIGNAL=0$
 ^EXIT=0$
 VERIFICATION SUCCESSFUL

diff --git a/regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc b/regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-first,second,string_size,prefix --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix --size-of-array prefix:prefix_size --max-array-size 5
+first,second,string_size,prefix --harness-type initialize-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix --size-of-array prefix:prefix_size --max-array-size 5
 ^SIGNAL=0$
 ^EXIT=0$
 VERIFICATION SUCCESSFUL

diff --git a/regression/snapshot-harness/pointer-to-array-int/test.desc b/regression/snapshot-harness/pointer-to-array-int/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-first,second,array_size,prefix,prefix_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix --size-of-array prefix:prefix_size --max-array-size 4
+first,second,array_size,prefix,prefix_size --harness-type initialize-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix --size-of-array prefix:prefix_size --max-array-size 4
 ^SIGNAL=0$
 ^EXIT=0$
 VERIFICATION SUCCESSFUL

diff --git a/regression/snapshot-harness/pointer_01/test.desc b/regression/snapshot-harness/pointer_01/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-x,p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+x,p --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion \*p == x: SUCCESS

diff --git a/regression/snapshot-harness/pointer_02/test.desc b/regression/snapshot-harness/pointer_02/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-x,p1,p2,p3 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+x,p1,p2,p3 --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=10$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion \*p2 == x: SUCCESS

diff --git a/regression/snapshot-harness/pointer_03/test.desc b/regression/snapshot-harness/pointer_03/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-x,p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+x,p --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion \*\(int \*\)p == 3: SUCCESS

diff --git a/regression/snapshot-harness/pointer_04/test.desc b/regression/snapshot-harness/pointer_04/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-x,p1,p2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+x,p1,p2 --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion \&p1 == \*p2: SUCCESS

diff --git a/regression/snapshot-harness/pointer_05/test.desc b/regression/snapshot-harness/pointer_05/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-x,p1,p2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+x,p1,p2 --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion \*p1 == \*p2: SUCCESS

diff --git a/regression/snapshot-harness/pointer_06/test.desc b/regression/snapshot-harness/pointer_06/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+p,q --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion p == q: SUCCESS

diff --git a/regression/snapshot-harness/pointer_07/test.desc b/regression/snapshot-harness/pointer_07/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-p1 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+p1 --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=10$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion p1\[0\] == 1: SUCCESS

diff --git a/regression/snapshot-harness/pointer_to_struct_01/test.desc b/regression/snapshot-harness/pointer_to_struct_01/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-st,p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+st,p,q --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion p == \&st: SUCCESS