File tree Expand file tree Collapse file tree 3 files changed +9
-9
lines changed Expand file tree Collapse file tree 3 files changed +9
-9
lines changed Original file line number Diff line number Diff line change @@ -18,22 +18,22 @@ goto\-cc \- C/C++ to goto compiler
18
18
19
19
.SH DESCRIPTION
20
20
.B goto\- cc
21
- reads source code, and generates a goto- binary. Its
21
+ reads source code, and generates a GOTO binary. Its
22
22
command-line interface is designed to mimic that of
23
23
.BR gcc (1).
24
24
Note in particular that \fB goto-cc \fR distinguishes between compiling
25
- and linking phases, just as \fB gcc \fR (1) does. \fB cbmc \fR (1) expects a goto- binary
25
+ and linking phases, just as \fB gcc \fR (1) does. \fB cbmc \fR (1) expects a GOTO binary
26
26
for which linking has been completed.
27
27
.PP
28
28
The basename of the file that is used to invoke \fB goto-cc \fR controls which
29
29
behavior will be emulated. This is typically accomplished by using symbolic
30
30
links.
31
31
.IP
32
32
\fB goto-cc \fR : invokes the default system compiler as preprocessor and just
33
- builds a goto- binary.
33
+ builds a GOTO binary.
34
34
.IP
35
35
\fB goto-gcc \fR : invokes \fB gcc \fR (1) as preprocessor and builds an \fB elf \fR (5)
36
- object file including an additional \fI goto-cc \fR section that holds the goto
36
+ object file including an additional \fI goto-cc \fR section that holds the GOTO
37
37
binary.
38
38
.IP
39
39
\fB goto-ld \fR : only performs linking, and also builds an \fB elf \fR (5) object as
Original file line number Diff line number Diff line change @@ -11,7 +11,7 @@ show version
11
11
.TP
12
12
.B goto\-harness \fI in \fB \fI out \fB \-\- harness \- function \- name \ \fI name \fB \-\- harness \- type \fI harness \- type \fR [\fB harness-options \fR ]
13
13
build harness for \fI in \fR and write harness to \fI out \fR ; the harness is
14
- printed as C code, if \fI out \fR has a .c suffix, else a goto binary including
14
+ printed as C code, if \fI out \fR has a .c suffix, else a GOTO binary including
15
15
the harness is generated
16
16
.SH DESCRIPTION
17
17
\fB goto \- harness \fR constructs functions that set up an appropriate environment
@@ -104,7 +104,7 @@ Treat the function parameter with the name \fIp\fR as a string of characters.
104
104
Initialize memory from JSON memory snapshot stored in \fI file \fR .
105
105
.TP
106
106
\fB \-\- initial \- goto \- location \fR \fI func \fR [:\fI n \fR ]
107
- Use function \fI func \fR and goto binary location number \fI n \fR as entry point.
107
+ Use function \fI func \fR and GOTO binary location number \fI n \fR as entry point.
108
108
.TP
109
109
\fB \-\- initial \- source \- location \fR \fI file \R :\fI n \fR
110
110
Use given file name \fI file \fR and line number \fI n \R in that file as entry
Original file line number Diff line number Diff line change 1
1
.TH SYMTAB2GB "1" "June 2022" "symtab2gb-5.59.0" "User Commands"
2
2
.SH NAME
3
- symtab2gb \- Compile JSON symbol tables to a goto binary
3
+ symtab2gb \- Compile JSON symbol tables to a GOTO binary
4
4
.SH SYNOPSIS
5
5
.TP
6
6
.B symtab2gb [\-?] [\-h] [\-\- help]
7
7
show help
8
8
.TP
9
9
.B symtab2gb \fI json \- symtab \- file \fR + [\fB\-\-out \fI outfile \fR ]
10
10
compile symbol tables in JSON format
11
- to a single goto binary
11
+ to a single GOTO binary
12
12
.SH DESCRIPTION
13
- This utility is to compile a \fB cbmc \fR (1) symbols table (in JSON format) into a goto binary.
13
+ This utility is to compile a \fB cbmc \fR (1) symbols table (in JSON format) into a GOTO binary.
14
14
This is to support integration of external language frontends, such as Ada
15
15
(using GNAT2GOTO: https://github.com/diffblue/gnat2goto) or Rust (using Kani:
16
16
https://github.com/model-checking/kani).
You can’t perform that action at this time.
0 commit comments