File tree Expand file tree Collapse file tree 1 file changed +2
-2
lines changed Expand file tree Collapse file tree 1 file changed +2
-2
lines changed Original file line number Diff line number Diff line change @@ -24,7 +24,7 @@ suite generation functionality in CBMC, by means of a case study. The
24
24
following program is an excerpt from a real-time embedded benchmark
25
25
[ PapaBench] ( https://www.irit.fr/recherches/ARCHI/MARCH/rubrique.php3?id_rubrique=97 ) ,
26
26
and implements part of a fly-by-wire autopilot for an Unmanned Aerial
27
- Vehicle (UAV). We have adjusted slightly for our purposes.
27
+ Vehicle (UAV). We have adjusted it slightly for our purposes.
28
28
29
29
The aim of function ` climb_pid_run ` is to control the vertical climb of
30
30
the UAV. Details on the theory behind this operation are documented in
@@ -133,7 +133,7 @@ following command:
133
133
We'll describe those command line options one by one. The option ` --cover mcdc `
134
134
specifies the code coverage criterion. There
135
135
are four conditional statements in the PID function: in lines 41,
136
- 44, 48 and 49. To satisfy MC/DC, the test suite has to meet
136
+ 44, 48, and 49. To satisfy MC/DC, the test suite has to meet
137
137
multiple requirements. For instance, each conditional statement needs to
138
138
evaluate to * true* and * false* . Consider the condition
139
139
` "pprz>=0 && pprz<=MAX_PPRZ" ` in line 41. CBMC instruments three
You can’t perform that action at this time.
0 commit comments