From 38ff68f43e378baa4d15e7a2f6e90d6e5dd98f57 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 21 Jun 2022 09:04:57 +0000 Subject: [PATCH 1/2] Add goto-harness man page This was built using help2man and then manually expanded. In the process of preparing it, several errors in existing goto-harness documentation were found and fixed as well. --- doc/man/goto-harness.1 | 134 +++++++++++++++++- .../memory_snapshot_harness_generator.cpp | 2 +- ...emory_snapshot_harness_generator_options.h | 2 +- 3 files changed, 135 insertions(+), 3 deletions(-) mode change 120000 => 100644 doc/man/goto-harness.1 diff --git a/doc/man/goto-harness.1 b/doc/man/goto-harness.1 deleted file mode 120000 index ea093bce1a5..00000000000 --- a/doc/man/goto-harness.1 +++ /dev/null @@ -1 +0,0 @@ -cbmc.1 \ No newline at end of file diff --git a/doc/man/goto-harness.1 b/doc/man/goto-harness.1 new file mode 100644 index 00000000000..8e450353425 --- /dev/null +++ b/doc/man/goto-harness.1 @@ -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|\fBinitialise-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/src/goto-harness/memory_snapshot_harness_generator.cpp b/src/goto-harness/memory_snapshot_harness_generator.cpp index 715991ceda5..e2e4a99aeba 100644 --- a/src/goto-harness/memory_snapshot_harness_generator.cpp +++ b/src/goto-harness/memory_snapshot_harness_generator.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-from-memory-snapshot"); + "--harness-type initialise-with-memory-snapshot"); } if(initial_source_location_line.empty() == initial_goto_location_line.empty()) diff --git a/src/goto-harness/memory_snapshot_harness_generator_options.h b/src/goto-harness/memory_snapshot_harness_generator_options.h index 14a32946fb7..93f8b56a43d 100644 --- a/src/goto-harness/memory_snapshot_harness_generator_options.h +++ b/src/goto-harness/memory_snapshot_harness_generator_options.h @@ -33,7 +33,7 @@ Author: Diffblue Ltd. // clang-format off #define MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP \ "memory snapshot harness generator (--harness-type\n" \ - " initialise-from-memory-snapshot)\n\n" \ + " initialise-with-memory-snapshot)\n\n" \ "--" MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT " initialise memory " \ "from JSON memory snapshot\n" \ "--" MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT " ]>\n" \ From f23992519e81827d435e18d4887f88fb1eec50bf Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 23 Jun 2022 08:24:31 +0000 Subject: [PATCH 2/2] 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. --- doc/architectural/goto-harness.md | 2 +- doc/man/goto-harness.1 | 2 +- regression/goto-harness/havoc-global-int-01/test.desc | 2 +- regression/goto-harness/havoc-global-int-02/test.desc | 2 +- regression/goto-harness/havoc-global-int-03/test.desc | 2 +- regression/goto-harness/havoc-global-struct/test.desc | 2 +- .../load-snapshot-recursive-static-global-int-01/test.desc | 2 +- .../goto-harness/load-snapshot-static-global-array-01/test.desc | 2 +- .../goto-harness/load-snapshot-static-global-int-01/test.desc | 2 +- .../goto-harness/load-snapshot-static-global-int-02/test.desc | 2 +- .../goto-harness/load-snapshot-static-global-int-03/test.desc | 2 +- .../goto-harness/load-snapshot-static-global-int-04/test.desc | 2 +- .../load-snapshot-static-global-pointer-01/test.desc | 2 +- regression/snapshot-harness/arrays_01/test.desc | 2 +- regression/snapshot-harness/arrays_02/test.desc | 2 +- .../snapshot-harness/dynamic-array-int-ordering/test.desc | 2 +- regression/snapshot-harness/dynamic-array-int/test.desc | 2 +- regression/snapshot-harness/function_pointer_01/test.desc | 2 +- regression/snapshot-harness/function_pointer_02/test.desc | 2 +- regression/snapshot-harness/function_pointer_03/test.desc | 2 +- .../snapshot-harness/nondet_initialize_static_arrays/test.desc | 2 +- .../test.desc | 2 +- regression/snapshot-harness/pointer-to-array-char/test.desc | 2 +- .../test.desc | 2 +- regression/snapshot-harness/pointer-to-array-int/test.desc | 2 +- regression/snapshot-harness/pointer_01/test.desc | 2 +- regression/snapshot-harness/pointer_02/test.desc | 2 +- regression/snapshot-harness/pointer_03/test.desc | 2 +- regression/snapshot-harness/pointer_04/test.desc | 2 +- regression/snapshot-harness/pointer_05/test.desc | 2 +- regression/snapshot-harness/pointer_06/test.desc | 2 +- regression/snapshot-harness/pointer_07/test.desc | 2 +- regression/snapshot-harness/pointer_to_struct_01/test.desc | 2 +- regression/snapshot-harness/simple-source-location/test.desc | 2 +- regression/snapshot-harness/static-array-char/test.desc | 2 +- regression/snapshot-harness/static-array-float/test.desc | 2 +- regression/snapshot-harness/static-array-int/test.desc | 2 +- regression/snapshot-harness/structs_01/test.desc | 2 +- regression/snapshot-harness/structs_02/test.desc | 2 +- regression/snapshot-harness/union_01/test.desc | 2 +- src/goto-harness/goto_harness_parse_options.cpp | 2 +- src/goto-harness/memory_snapshot_harness_generator.cpp | 2 +- src/goto-harness/memory_snapshot_harness_generator_options.h | 2 +- 43 files changed, 43 insertions(+), 43 deletions(-) diff --git a/doc/architectural/goto-harness.md b/doc/architectural/goto-harness.md index 35c496273ad..c602e65de98 100644 --- a/doc/architectural/goto-harness.md +++ b/doc/architectural/goto-harness.md @@ -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 \ diff --git a/doc/man/goto-harness.1 b/doc/man/goto-harness.1 index 8e450353425..cb5cf242b77 100644 --- a/doc/man/goto-harness.1 +++ b/doc/man/goto-harness.1 @@ -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. diff --git a/regression/goto-harness/havoc-global-int-01/test.desc b/regression/goto-harness/havoc-global-int-01/test.desc index 78c0bc19716..5f817b5fb71 100644 --- 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 index d1bf5c6601a..fe3abf4614d 100644 --- 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 index 5c9eb104a84..a9a39694e7e 100644 --- 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 index 12ebe2d7452..acea3f2c367 100644 --- 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 index ada15063c50..aabcd925525 100644 --- 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 index ebe62c653c7..b9be03e032d 100644 --- 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 index 5d8f5f01966..cbfab21c496 100644 --- 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 index 50e01a8e8ca..255126954dc 100644 --- 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 index 5d8f5f01966..cbfab21c496 100644 --- 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 index ada15063c50..aabcd925525 100644 --- 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 index ebe62c653c7..b9be03e032d 100644 --- 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 index d8d645bc264..911c0766bcb 100644 --- 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 index a496c42f2bd..3095758682c 100644 --- 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 index 4ea73d4857e..cc65ba43d83 100644 --- 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 index 33be9fcc748..3178475a0ba 100644 --- 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 index f02a7c92e98..8147567054d 100644 --- 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 index 027490a5501..1d5b9679ad4 100644 --- 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 index d75465af125..d8e8cd4cc92 100644 --- 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 index 89948d9dd6b..925dfd35e26 100644 --- 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 index c855462b45a..9c5f5417310 100644 --- 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 index bdb6acc6ed4..ceaacf1adec 100644 --- 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 index 32219e6e450..0a875116588 100644 --- 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 index 3ccfd8158b9..069bbbb0ec7 100644 --- 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 index 9abc6f6229d..05228b82757 100644 --- 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 index 7cd419bf4ea..39080609502 100644 --- 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 index 81c527e79ea..0ae19ee4abd 100644 --- 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 index 18f47d6d72d..90c0ade0aa0 100644 --- 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 index ee2f3ec2e4a..48992d614b9 100644 --- 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 index 5e133f5604d..205ea21fb34 100644 --- 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 index f358ff4c113..fafadf41fe8 100644 --- 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 index e020c764c1b..a72fe61325d 100644 --- 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 diff --git a/regression/snapshot-harness/simple-source-location/test.desc b/regression/snapshot-harness/simple-source-location/test.desc index 494200a52e5..bc069a7d361 100644 --- a/regression/snapshot-harness/simple-source-location/test.desc +++ b/regression/snapshot-harness/simple-source-location/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$ diff --git a/regression/snapshot-harness/static-array-char/test.desc b/regression/snapshot-harness/static-array-char/test.desc index bb0b9de5cf9..e01f011cc96 100644 --- a/regression/snapshot-harness/static-array-char/test.desc +++ b/regression/snapshot-harness/static-array-char/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 diff --git a/regression/snapshot-harness/static-array-float/test.desc b/regression/snapshot-harness/static-array-float/test.desc index 23f45c15428..4a4cfd4a21c 100644 --- a/regression/snapshot-harness/static-array-float/test.desc +++ b/regression/snapshot-harness/static-array-float/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 diff --git a/regression/snapshot-harness/static-array-int/test.desc b/regression/snapshot-harness/static-array-int/test.desc index 3d4dfd4d7ab..88728ba395d 100644 --- a/regression/snapshot-harness/static-array-int/test.desc +++ b/regression/snapshot-harness/static-array-int/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 diff --git a/regression/snapshot-harness/structs_01/test.desc b/regression/snapshot-harness/structs_01/test.desc index 281cf74b85e..6ce303c8e4e 100644 --- a/regression/snapshot-harness/structs_01/test.desc +++ b/regression/snapshot-harness/structs_01/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 diff --git a/regression/snapshot-harness/structs_02/test.desc b/regression/snapshot-harness/structs_02/test.desc index 6a156d320f2..0692bd27eb5 100644 --- a/regression/snapshot-harness/structs_02/test.desc +++ b/regression/snapshot-harness/structs_02/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 diff --git a/regression/snapshot-harness/union_01/test.desc b/regression/snapshot-harness/union_01/test.desc index acf6141b85d..9532a600116 100644 --- a/regression/snapshot-harness/union_01/test.desc +++ b/regression/snapshot-harness/union_01/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 diff --git a/src/goto-harness/goto_harness_parse_options.cpp b/src/goto-harness/goto_harness_parse_options.cpp index cf3d26687ee..a48db51ba45 100644 --- a/src/goto-harness/goto_harness_parse_options.cpp +++ b/src/goto-harness/goto_harness_parse_options.cpp @@ -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( ui_message_handler); }); diff --git a/src/goto-harness/memory_snapshot_harness_generator.cpp b/src/goto-harness/memory_snapshot_harness_generator.cpp index e2e4a99aeba..00a958a4df7 100644 --- a/src/goto-harness/memory_snapshot_harness_generator.cpp +++ b/src/goto-harness/memory_snapshot_harness_generator.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()) diff --git a/src/goto-harness/memory_snapshot_harness_generator_options.h b/src/goto-harness/memory_snapshot_harness_generator_options.h index 93f8b56a43d..8f95bcdb7c7 100644 --- a/src/goto-harness/memory_snapshot_harness_generator_options.h +++ b/src/goto-harness/memory_snapshot_harness_generator_options.h @@ -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 " initialise memory " \ "from JSON memory snapshot\n" \ "--" MEMORY_SNAPSHOT_HARNESS_INITIAL_GOTO_LOC_OPT " ]>\n" \