American spelling: initialise-with-memory-snapshot -> initialize-with-memory-snapshot

All documentation and code has been updated to change the name of the
goto-harness command-line option.

Author: tautschnig

doc/architectural/goto-harness.md

@@ -43,7 +43,7 @@ about the program state. Second, memory-snapshot harnesses, in which case
 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|\fBinitialise-with-memory-snapshot\fR]
+\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.

doc/man/goto-harness.1

@@ -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

regression/goto-harness/havoc-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-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$

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-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

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-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$

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-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

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 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

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 ../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

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=10$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS

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=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

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: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

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 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

regression/goto-harness/load-snapshot-static-global-pointer-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

regression/snapshot-harness/arrays_01/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

regression/snapshot-harness/arrays_02/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

regression/snapshot-harness/dynamic-array-int-ordering/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

regression/snapshot-harness/dynamic-array-int/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

regression/snapshot-harness/function_pointer_01/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

regression/snapshot-harness/function_pointer_02/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

regression/snapshot-harness/function_pointer_03/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

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 --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

regression/snapshot-harness/pointer-function-parameters-struct-mutual-recursion/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

regression/snapshot-harness/pointer-to-array-char/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

regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/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

regression/snapshot-harness/pointer-to-array-int/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

regression/snapshot-harness/pointer_01/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

regression/snapshot-harness/pointer_02/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

regression/snapshot-harness/pointer_03/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

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

regression/snapshot-harness/pointer_05/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

regression/snapshot-harness/pointer_06/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

regression/snapshot-harness/pointer_07/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

regression/snapshot-harness/pointer_to_struct_01/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-global_var --harness-type initialise-with-memory-snapshot --initial-source-location main.c:20
+global_var --harness-type initialize-with-memory-snapshot --initial-source-location main.c:20
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[foo.assertion.1\] line [0-9]+ assertion global_var == 0: SUCCESS$

regression/snapshot-harness/simple-source-location/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-tmp,first,second,array_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+tmp,first,second,array_size --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
 ^SIGNAL=0$
 ^EXIT=0$
 VERIFICATION SUCCESSFUL

regression/snapshot-harness/static-array-char/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 main.c
-array,iterator1,iterator2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+array,iterator1,iterator2 --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=10$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion \*iterator1 \>= 1.10 \&\& \*iterator1 \<= 1.12: SUCCESS

regression/snapshot-harness/static-array-float/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-array,iterator1,iterator2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+array,iterator1,iterator2 --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

regression/snapshot-harness/static-array-int/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-st,p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+st,p --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion st.c1 \+ 2 == st.c2: SUCCESS

regression/snapshot-harness/structs_01/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-st,p --harness-type initialise-with-memory-snapshot --initial-source-location main.c:27
+st,p --harness-type initialize-with-memory-snapshot --initial-source-location main.c:27
 ^EXIT=0$
 ^SIGNAL=0$
 \[foo.assertion.1\] line [0-9]+ assertion st.c1 \+ 2 == st.c2: SUCCESS

regression/snapshot-harness/structs_02/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
-un,ip,fp --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+un,ip,fp --harness-type initialize-with-memory-snapshot --initial-goto-location main:4
 ^EXIT=0$
 ^SIGNAL=0$
 \[main.assertion.1\] line [0-9]+ assertion ip == \&un.i: SUCCESS

regression/snapshot-harness/union_01/test.desc

@@ -256,7 +256,7 @@ goto_harness_generator_factoryt goto_harness_parse_optionst::make_factory()
       ui_message_handler);
   });
 
-  factory.register_generator("initialise-with-memory-snapshot", [this]() {
+  factory.register_generator("initialize-with-memory-snapshot", [this]() {
     return util_make_unique<memory_snapshot_harness_generatort>(
       ui_message_handler);
   });

src/goto-harness/goto_harness_parse_options.cpp

@@ -111,7 +111,7 @@ void memory_snapshot_harness_generatort::validate_options(
   {
     throw invalid_command_line_argument_exceptiont(
       "option --memory_snapshot is required",
-      "--harness-type initialise-with-memory-snapshot");
+      "--harness-type initialize-with-memory-snapshot");
   }
 
   if(initial_source_location_line.empty() == initial_goto_location_line.empty())

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -33,7 +33,7 @@ Author: Diffblue Ltd.
 // clang-format off
 #define MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP                                 \
   "memory snapshot harness generator (--harness-type\n"                        \
-  "  initialise-with-memory-snapshot)\n\n"                                     \
+  "  initialize-with-memory-snapshot)\n\n"                                     \
   "--" MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT " <file>      initialise memory "  \
   "from JSON memory snapshot\n"                                                \
   "--" MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT " <func[:<n>]>\n"          \