doc: times should have a value

Daniel Kroening · Daniel Kroening · commit d54d63b2a739 · 2019-01-06T12:51:25.000Z
diff --git a/doc/cprover-manual/cbmc-tutorial.md b/doc/cprover-manual/cbmc-tutorial.md
@@ -218,6 +218,7 @@ is an example of a program with a user-specified property:
 
 ```C
 _Bool nondet_bool();
+unsigned int nondet_unsigned_int();
 _Bool LOCK = 0;
 
 _Bool lock()
@@ -241,7 +242,7 @@ void unlock()
 int main()
 {
   unsigned got_lock = 0;
-  int times;
+  unsigned times = nondet_unsigned_int();
 
   while(times > 0)
   {

Original file line number	Diff line number	Diff line change
`@@ -218,6 +218,7 @@ is an example of a program with a user-specified property:`
`218`	`218`
`219`	`219`	```C
`220`	`220`	`_Bool nondet_bool();`
	`221`	`+unsigned int nondet_unsigned_int();`
`221`	`222`	`_Bool LOCK = 0;`
`222`	`223`
`223`	`224`	`_Bool lock()`
`@@ -241,7 +242,7 @@ void unlock()`
`241`	`242`	`int main()`
`242`	`243`	`{`
`243`	`244`	`unsigned got_lock = 0;`
`244`		`- int times;`
	`245`	`+ unsigned times = nondet_unsigned_int();`
`245`	`246`
`246`	`247`	`while(times > 0)`
`247`	`248`	`{`