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
1818
1919.SH DESCRIPTION
2020.B goto\- cc
21- reads source code, and generates a goto- binary. Its
21+ reads source code, and generates a GOTO binary. Its
2222command-line interface is designed to mimic that of
2323.BR gcc (1).
2424Note 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
2626for which linking has been completed.
2727.PP
2828The basename of the file that is used to invoke \fB goto-cc \fR controls which
2929behavior will be emulated. This is typically accomplished by using symbolic
3030links.
3131.IP
3232\fB goto-cc \fR : invokes the default system compiler as preprocessor and just
33- builds a goto- binary.
33+ builds a GOTO binary.
3434.IP
3535\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
3737binary.
3838.IP
3939\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
1111.TP
1212.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 ]
1313build 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
1515the harness is generated
1616.SH DESCRIPTION
1717\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.
104104Initialize memory from JSON memory snapshot stored in \fI file \fR .
105105.TP
106106\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.
108108.TP
109109\fB \-\- initial \- source \- location \fR \fI file \R :\fI n \fR
110110Use 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 11.TH SYMTAB2GB "1" "June 2022" "symtab2gb-5.59.0" "User Commands"
22.SH NAME
3- symtab2gb \- Compile JSON symbol tables to a goto binary
3+ symtab2gb \- Compile JSON symbol tables to a GOTO binary
44.SH SYNOPSIS
55.TP
66.B symtab2gb [\-?] [\-h] [\-\- help]
77show help
88.TP
99.B symtab2gb \fI json \- symtab \- file \fR + [\fB\-\-out \fI outfile \fR ]
1010compile symbol tables in JSON format
11- to a single goto binary
11+ to a single GOTO binary
1212.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.
1414This is to support integration of external language frontends, such as Ada
1515(using GNAT2GOTO: https://github.com/diffblue/gnat2goto) or Rust (using Kani:
1616https://github.com/model-checking/kani).
You can’t perform that action at this time.
0 commit comments