Skip to content

Commit f57f2b8

Browse files
authored
Merge pull request #3696 from diffblue/fix-doc-examples
Fix code examples in the documentation
2 parents 225e18d + d54d63b commit f57f2b8

File tree

1 file changed

+4
-1
lines changed

1 file changed

+4
-1
lines changed

doc/cprover-manual/cbmc-tutorial.md

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -145,6 +145,8 @@ int sum() {
145145
sum=0;
146146
for(i=0; i<10; i++)
147147
sum+=array[i];
148+
149+
return sum;
148150
}
149151
```
150152

@@ -216,6 +218,7 @@ is an example of a program with a user-specified property:
216218

217219
```C
218220
_Bool nondet_bool();
221+
unsigned int nondet_unsigned_int();
219222
_Bool LOCK = 0;
220223

221224
_Bool lock()
@@ -239,7 +242,7 @@ void unlock()
239242
int main()
240243
{
241244
unsigned got_lock = 0;
242-
int times;
245+
unsigned times = nondet_unsigned_int();
243246

244247
while(times > 0)
245248
{

0 commit comments

Comments
 (0)