cbmc pid.c --cover mcdc --unwind 6 --trace --xml-ui
+cbmc pid.c --cover mcdc --unwind 6 --xml-ui
@@ -173,11 +173,11 @@ pprz >= (float)0 && pprz <= (float)(16 * 600) id="climb_pid_run.coverage.3"
The "id" of each coverage goal is automatically assigned by CBMC. For every
-coverage goal, a trace (if there exists) of the program execution that
-satisfies such a goal is printed out in XML format, as the parameters
---trace --xml-ui are given. Multiple coverage goals can share a
-trace, when the corresponding execution of the program satisfies all these
-goals at the same time. Each trace corresponds to a test case.
+coverage goal, a test suite (if there exists) that
+satisfies such a goal is printed out in XML format, as the parameter
+--xml-ui is given. Multiple coverage goals can share a
+test suite, when the corresponding execution of the program satisfies all these
+goals at the same time.
@@ -185,6 +185,10 @@ In the end, the following test suites are automatically generated for testing th
A test suite consists of a sequence of input parameters that are
passed to the PID function climb_pid_run at each loop iteration.
For example, Test 1 covers the MC/DC goal with id="climb_pid_run.coverage.1".
+The complete output from CBMC is in
+pid_test_suites.xml, where every test suite and the coverage goals it is for
+are clearly described.
+
Test suite:
Test 1.
(iteration 1) desired_climb=-1.000000f, estimator_z_dot=1.000000f
diff --git a/doc/html-manual/pid_test_suites.xml b/doc/html-manual/pid_test_suites.xml
new file mode 100644
index 00000000000..014fea12294
--- /dev/null
+++ b/doc/html-manual/pid_test_suites.xml
@@ -0,0 +1,500 @@
+
+
+CBMC 5.5
+
+ CBMC version 5.5 64-bit x86_64 macos
+
+
+
+ Parsing pid.c
+
+
+
+ Converting
+
+
+
+ Type-checking pid
+
+
+
+ function `nondet_float' is not declared
+
+
+
+ Generating GOTO Program
+
+
+
+ Adding CPROVER library (x86_64)
+
+
+
+ Removal of function pointers and virtual functions
+
+
+
+ Partial Inlining
+
+
+
+ Generic Property Instrumentation
+
+
+criterion: mcdc
+
+
+ Instrumenting coverage goals
+
+
+
+ Starting Bounded Model Checking
+
+
+
+ Unwinding loop main.0 iteration 1 (6 max) file pid.c line 56 function main thread 0
+
+
+
+ Unwinding loop main.0 iteration 2 (6 max) file pid.c line 56 function main thread 0
+
+
+
+ Unwinding loop main.0 iteration 3 (6 max) file pid.c line 56 function main thread 0
+
+
+
+ Unwinding loop main.0 iteration 4 (6 max) file pid.c line 56 function main thread 0
+
+
+
+ Unwinding loop main.0 iteration 5 (6 max) file pid.c line 56 function main thread 0
+
+
+
+ Not unwinding loop main.0 iteration 6 (6 max) file pid.c line 56 function main thread 0
+
+
+
+ size of program expression: 416 steps
+
+
+
+ Generated 114 VCC(s), 108 remaining after simplification
+
+
+
+ Passing problem to propositional reduction
+
+
+
+ converting SSA
+
+
+
+ Aiming to cover 19 goal(s)
+
+
+
+ Running propositional reduction
+
+
+
+ Post-processing
+
+
+
+ Solving with MiniSAT 2.2.1 with simplifier
+
+
+
+ 131818 variables, 553801 clauses
+
+
+
+ SAT checker: instance is SATISFIABLE
+
+
+
+ Covered decision/condition `1 != 0' true
+
+
+
+ Solving with MiniSAT 2.2.1 with simplifier
+
+
+
+ 131818 variables, 395675 clauses
+
+
+
+ SAT checker: instance is SATISFIABLE
+
+
+
+ Covered MC/DC independence condition `!(pprz >= (float)0) && pprz <= (float)(16 * 600)'
+
+
+
+ Covered decision `pprz >= (float)0 && pprz <= (float)(16 * 600)' false
+
+
+
+ Covered condition `pprz >= (float)0' false
+
+
+
+ Covered decision/condition `pprz > (float)(16 * 600)' false
+
+
+
+ Covered condition `pprz <= (float)(16 * 600)' true
+
+
+
+ Covered decision/condition `desired_climb > (float)0' false
+
+
+
+ Covered decision/condition `climb_sum_err > (float)10' false
+
+
+
+ Covered decision/condition `climb_sum_err < (float)-10' false
+
+
+
+ Solving with MiniSAT 2.2.1 with simplifier
+
+
+
+ 131818 variables, 393279 clauses
+
+
+
+ SAT checker: instance is SATISFIABLE
+
+
+
+ Covered MC/DC independence condition `pprz >= (float)0 && !(pprz <= (float)(16 * 600))'
+
+
+
+ Covered condition `pprz >= (float)0' true
+
+
+
+ Covered decision/condition `pprz > (float)(16 * 600)' true
+
+
+
+ Covered condition `pprz <= (float)(16 * 600)' false
+
+
+
+ Covered decision/condition `desired_climb > (float)0' true
+
+
+
+ Solving with MiniSAT 2.2.1 with simplifier
+
+
+
+ 131818 variables, 391285 clauses
+
+
+
+ SAT checker: instance is SATISFIABLE
+
+
+
+ Covered MC/DC independence condition `pprz >= (float)0 && pprz <= (float)(16 * 600)'
+
+
+
+ Covered decision `pprz >= (float)0 && pprz <= (float)(16 * 600)' true
+
+
+
+ Solving with MiniSAT 2.2.1 with simplifier
+
+
+
+ 131818 variables, 390122 clauses
+
+
+
+ SAT checker: instance is SATISFIABLE
+
+
+
+ Covered decision/condition `climb_sum_err < (float)-10' true
+
+
+
+ Solving with MiniSAT 2.2.1 with simplifier
+
+
+
+ 131818 variables, 390121 clauses
+
+
+
+ SAT checker: instance is SATISFIABLE
+
+
+
+ Covered decision/condition `climb_sum_err > (float)10' true
+
+
+
+ Solving with MiniSAT 2.2.1 with simplifier
+
+
+
+ 131818 variables, 387493 clauses
+
+
+
+ SAT checker inconsistent: instance is UNSATISFIABLE
+
+
+
+ Runtime decision procedure: 3.806s
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ -1.000000
+
+
+ 1.000000
+
+
+
+
+
+
+
+ -1.000000
+
+
+ 1.000000
+
+
+ 1.000000
+
+
+ -1.000000
+
+
+
+
+
+
+
+ 0.000000
+
+
+ -1.000000
+
+
+ 1.000000
+
+
+ -1.000000
+
+
+
+
+
+
+
+ 1.000000
+
+
+ -1.000000
+
+
+ 1.000000
+
+
+ -1.000000
+
+
+ 1.000000
+
+
+ -1.000000
+
+
+ 1.000000
+
+
+ -1.000000
+
+
+ 0.000000
+
+
+ -1.000000
+
+
+ 1.000000
+
+
+ -1.000000
+
+
+
+
+
+
+
+ -1.000000
+
+
+ 1.000000
+
+
+ -1.000000
+
+
+ 1.000000
+
+
+ -1.000000
+
+
+ 1.000000
+
+
+ -1.000000
+
+
+ 1.000000
+
+
+ -1.000000
+
+
+ 1.000000
+
+
+ -1.000000
+
+
+ 1.000000
+
+
+
+
+
+ ** 18 of 19 covered (94.7%)
+
+
+
+ ** Used 7 iterations
+
+
+