Did a couple other tweaks/clarifications

README.md

@@ -55,7 +55,7 @@ In the `examples` folder, run the following commands. We are including output fi
     ./so_parse.py xen/fsimage > xen/fsimage/results.txt
     ./so_parse.py xen/python > xen/python/results.txt
 
-As with the statistics for full binaries, the results are in a tab-separated form with headers that can easily be pasted into a spreadsheet for manipulation. However, due to the amount of information present, we also provide a summary of the results on a per-library level at the end of each `results.txt` file, which are the numbers that we have worked off of. The statistics for the `lib` results can be summed up to obtain the `lib` table entry while the ones for `fsimage` result in the `xenfsimage` entry. Finally, the results file for `xen/python` is split into two entries. The numbers for `xenfsimage.so` alone are the entry for `dist-packages` (*not* `xenfsimage`) in Table 1 while the numbers for `xc.so` and `xs.so` are combined to obtain the results for `lowlevel` in the table. As before, the indirection count minus the number of unresolved jumps and calls will produce the number of resolved indirections.
+As with the statistics for full binaries, the results are in a tab-separated form with headers that can easily be pasted into a spreadsheet for manipulation. However, due to the amount of information present, we also provide a summary of the results on a per-library level at the end of each `results.txt` file, which are the numbers that we have worked off of. In this case, the count of successful analyses and the number of functions analyzed are listed in the results themselves; still as before, failures must be examined to determine why they failed. The statistics for the `lib` results can be summed up to obtain the `lib` table entry while the ones for `fsimage` result in the `xenfsimage` entry. Finally, the results file for `xen/python` is split into two entries. The numbers for `xenfsimage.so` alone are the entry for `dist-packages` (*not* `xenfsimage`) in Table 1 while the numbers for `xc.so` and `xs.so` are combined to obtain the results for `lowlevel` in the table. As before, the indirection count minus the number of unresolved jumps and calls will produce the number of resolved indirections.
 
 # Isabelle proofs
 The folder `isabelle` contains Isabelle/HOL proofs and examples. The README in that folder provides instructions for how to utilize Isabelle to verify the proofs in the `isabelle/examples` folder. Currently we do not have a setup to automatically extract the statistics to reproduce Table 2; the main focus of this artifact is the results produced by the `construct-ssm` program.

examples/xen/lib/results.txt

@@ -1950,7 +1950,7 @@ fsip_fs_offset		2	2	0	0	0	0:00:00.010000
 fsip_fs_set_data		2	2	0	0	0	0:00:00.010000
 	=COUNTIF(B1:B30, "TRUE")	=SUM(C1:C30)	=SUM(D1:D30)	=SUM(E1:E30)	=SUM(F1:F30)	=SUM(G1:G30)	=SUM(H1:H30)	=SUM(I1:I30)
 
-Done	Total	Insts	Symbolic states	Indirection	Unresolved jumps	Unresolved calls	Time to Analyze (h:m:s)
+	Done	Total	Insts	Symbolic states	Indirection	Unresolved jumps	Unresolved calls	Time to Analyze (h:m:s)
 libxencall.so.1.2	14	14	738	754	0	0	0	0:02:06.570000
 libxenctrl.so.4.12.0	396	398	26183	26193	23	4	19	0:45:50.060000
 libxendevicemodel.so.1.3	24	24	6332	6332	0	0	0	0:10:37.190000