How to calculate the TCB size

[Norman Feske]

Hello,

>> Do I need to check all files listed in each .d files in “var/libcache” or is there any efficient way to count the number of lines for the TCB?
> 
> By default we calculate our LOC values via 'sloccount <SRC_DIR>' called
> for each source directory that is used. Of course, this way you have to
> evaluate manually which sources (repos, components, libs, specs) are
> used in your scenario. At least, I do not know a way to automate this
> step.

one way to automate this is to grep for the source files in the output
of 'objdump -ld <binary>'. This produces a list of the source files that
contributed code to the binary. This step must be repeated for all the
binaries of interest. Of course, the resulting list contains duplicates
(source files used by multiple components). To remove those duplicates,
pipe the list through 'sort | uniq'. The resulting list can then be
passed to sloccount.

Note, however, that might be the rare case where a header file is used
during the compilation but not present in the output of 'objdump -ld'.
This happens when the content of the header contains sole data
structures but no code ending up in the binary. Fortunately, there are -
no my knowledge - no such headers in Genode. But I'd advise you to
double-check.

Cheers
Norman

-- 
Dr.-Ing. Norman Feske
Genode Labs

http://www.genode-labs.com · http://genode.org

Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden
Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth