diff options
Diffstat (limited to 'chapters/hls.tex')
| -rw-r--r-- | chapters/hls.tex | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/chapters/hls.tex b/chapters/hls.tex index f39afd3..dcdf2b2 100644 --- a/chapters/hls.tex +++ b/chapters/hls.tex @@ -1320,9 +1320,9 @@ $B_1$ and $B_2$ must be the same. \startplacetable[reference={tab:proof-statistics},title={Statistics about the numbers of lines of code in the proof and implementation of Vericert.}] \starttabulate[|l|r|r|r|r|r|] - \FL - \NC \NS[1][c] {\bf Coq code} \NS[1][c] {\bf Spec} \NC {\bf Total} \NC \NR - \ML + \HL + \NC \NC {\bf Coq code} \NC \NC {\bf Spec} \NC \NC {\bf Total} \NC \NR + \HL \NC Data structures and libraries \NC 280 \NC --- \NC --- \NC 500 \NC 780 \NC \NR \NC Integers and values \NC 98 \NC --- \NC 15 \NC 968 \NC 1081 \NC \NR \NC HTL semantics \NC 50 \NC --- \NC 181 \NC 65 \NC 296 \NC \NR @@ -1331,9 +1331,9 @@ $B_1$ and $B_2$ must be the same. \NC Verilog semantics \NC 78 \NC --- \NC 431 \NC 235 \NC 744 \NC \NR \NC Verilog generation \NC 104 \NC --- \NC --- \NC 486 \NC 590 \NC \NR \NC Top-level driver, pretty printers \NC 318 \NC 775 \NC --- \NC 189 \NC 1282 \NC \NR - \LL + \HL \NC {\bf Total} \NC 1721 \NC 775 \NC 693 \NC 8355 \NC 11544 \NC \NR - \BL + \HL \stoptabulate \stopplacetable |