Skip to content

Commit d6032f1

Browse files
author
Daniel Kroening
committed
manual: provide download for "file2.c"
1 parent 344a074 commit d6032f1

File tree

2 files changed

+19
-5
lines changed

2 files changed

+19
-5
lines changed

doc/cprover-manual/cbmc-tutorial.md

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -135,16 +135,18 @@ In the example above, we used a program that starts with a `main`
135135
function. However, CBMC is aimed at embedded software, and these kinds
136136
of programs usually have different entry points. Furthermore, CBMC is
137137
also useful for verifying program modules. Consider the following
138-
example, called file2.c:
138+
example, called [file2.c](https://raw.githubusercontent.com/diffblue/cbmc/develop/doc/cprover-manual/file2.c):
139139

140140
```C
141141
int array[10];
142-
int sum() {
142+
143+
int sum()
144+
{
143145
unsigned i, sum;
144146

145-
sum=0;
146-
for(i=0; i<10; i++)
147-
sum+=array[i];
147+
sum = 0;
148+
for(i = 0; i < 10; i++)
149+
sum += array[i];
148150

149151
return sum;
150152
}

doc/cprover-manual/file2.c

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
int array[10];
2+
3+
int sum()
4+
{
5+
unsigned i, sum;
6+
7+
sum = 0;
8+
for(i = 0; i < 10; i++)
9+
sum += array[i];
10+
11+
return sum;
12+
}

0 commit comments

Comments
 (0)