Skip to content

Commit 1445da9

Browse files
committed
Cleanup memory analyzer documentation
Update example formatting in the man page to make it consistent with our other man pages, and remove now-redundant Markdown file (all its content was moved to the man page).
1 parent d94c1cf commit 1445da9

File tree

3 files changed

+9
-93
lines changed

3 files changed

+9
-93
lines changed

doc/architectural/front-page.md

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,6 @@ Overview of Documentation
6565
you can access it <a href=
6666
"https://svn.cprover.org/wiki/doku.php?id=cprover_tutorial">here</a>.
6767

68-
* \subpage memory-analyzer
6968
* \subpage memory-bounds-checking
7069
* \subpage satabs
7170

doc/architectural/memory-analyzer.md

Lines changed: 0 additions & 84 deletions
This file was deleted.

doc/man/memory-analyzer.1

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -42,18 +42,18 @@ option is necessary when compiling for the program symbols to be visible.
4242
.PP
4343
Take for example the following program:
4444
.EX
45-
.IP
46-
// main.c
47-
void checkpoint() {}
45+
.in +4n
46+
\fB// main.c\fP
47+
void \fBcheckpoint\fP() {}
4848
4949
int array[] = {1, 2, 3};
5050
51-
int main()
52-
{
51+
int \fBmain\fP() {
5352
array[1] = 4;
54-
checkpoint();
55-
return 0;
53+
\fBcheckpoint\fP();
54+
\fBreturn\fP 0;
5655
}
56+
.in
5757
.EE
5858
.PP
5959
Say we are interested in the evaluation of \fIarray\fR at the call-site of
@@ -70,10 +70,11 @@ memory-analyzer --breakpoint checkpoint --symbols array main_exe
7070
.PP
7171
to obtain as output the human readable list of values for each requested symbol:
7272
.EX
73-
.IP
73+
.in +4n
7474
{
7575
array = { 1, 4, 3 };
7676
}
77+
.in
7778
.EE
7879
.PP
7980
The above result is useful for the user and their preliminary analysis but does

0 commit comments

Comments
 (0)