Merge pull request #5826 from tautschnig/gb-suffix

Documentation: consistently use .gb suffix for goto binaries

Author: tautschnig

doc/architectural/howto.md

@@ -76,10 +76,10 @@ If you built using CMake on Unix, you should be able to run the
 Find or write a moderately-interesting C program; we'll call it `main.c`.
 Run the following commands:
 
-    goto-gcc -o main.goto main.c
+    goto-gcc -o main.gb main.c
     cc -o main.exe main.c
 
-Invoke `./main.goto` and `./main.exe` and observe that they run identically.
+Invoke `./main.gb` and `./main.exe` and observe that they run identically.
 The version that was compiled with `goto-gcc` is larger, though:
 
     du -hs *.{goto,exe}
@@ -95,7 +95,7 @@ is (informally) called a *goto-program*.
 `goto-instrument` is a Swiss army knife for viewing goto-programs and
 performing single program analyses on them.  Run the following command:
 
-    goto-instrument --show-goto-functions main.goto
+    goto-instrument --show-goto-functions main.gb
 
 Many of the instructions in the goto-program intermediate representation
 are similar to their C counterparts.  `if` and `goto` statements replace
@@ -105,7 +105,7 @@ Find or write a small C program (2 or 3 functions, each containing a few
 varied statements).  Compile it using `goto-gcc` as above into an object
 file called `main`. You can write the diagram to a file and then view it:
 
-    goto-instrument --dot main.goto | tail -n +2 | dot -Tpng > main.png
+    goto-instrument --dot main.gb | tail -n +2 | dot -Tpng > main.png
     open main.png
 
 (the invocation of `tail` is used to filter out the first line of
@@ -143,7 +143,7 @@ At some point in that function, there will be a long sequence of `if` statements
 **Task:** Add a `--greet` switch to `goto-instrument`, taking an optional
 argument, with the following behaviour:
 
-    $ goto-instrument --greet main.goto
+    $ goto-instrument --greet main.gb
     hello, world!
     $ goto-instrument --greet Leperina main
     hello, Leperina!

doc/cprover-manual/properties.md

@@ -227,14 +227,14 @@ Now, we can compile the program and detect that the error functions are indeed
 called by invoking these commands:
 
 ```
-goto-cc error_example.c -o error_example.goto
+goto-cc error_example.c -o error_example.gb
 # Replace all functions ending with _error
 # (Excluding those starting with __)
 # With ones that have an assert(false) body
-goto-instrument error_example.goto error_example_replaced.goto \
+goto-instrument error_example.gb error_example_replaced.gb \
   --generate-function-body '(?!__).*_error' \
   --generate-function-body-options assert-false
-cbmc error_example_replaced.goto
+cbmc error_example_replaced.gb
 ```
 
 This generates the following output:
@@ -277,7 +277,7 @@ int do_something_with_complex(struct Complex *complex);
 And the command line
 
 ```
-goto-instrument in.goto out.goto
+goto-instrument in.gb out.gb
   --generate-function-body do_something_with_complex
   --generate-function-body-options
     'havoc,params:.*,globals:AGlobalComplex'