Recent doxygen versions generate references for constants that are named
in the text. Since we do not produce a constant table in the manual
(neither markdown nor tex), these references point to nowhere and
produce a KeyError in the ref_dict on lookup.
The corresponding xml nodes are of this form:
<ref kindref="member"
refid="include_2sel4_2constants_8h_1a9a3...">seL4_TCBFlag</ref>
Ignore such dangling references and return the content (seL4_TCBFlag in
the example) instead. Run text escape on the content to cover
underscores etc in LaTeX.
Does not produce a warning since we expect this to be normal behaviour.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add flags to tcb_t and the seL4_TCBFlag_fpuDisabled flag.
Enums are signed, make TCB flags word_t to make it unsigned.
Signed-off-by: Indan Zupancic <indan@nul.nu>
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
Migrate documentation of the API docs generation process here from the
docsite where it is too much out of view. Here it is closer to where it
is needed an more likely to get updated when things change.
Compared to the docsite version, this has applied:
- standard wrap column
- markdown lints
- adjusted headings
- `object-api-sel4-arch.xml` etc renames
- include RISC-V in structure
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
When evaluating XML condition expressions, properly treat undefined
values as undefined, not as False. Otherwise, the negation of an
undefined value may make an entire expression true and incorrectly
label some methods as MCS methods.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This adds `seL4_CapSMC` to table 9.1 and updates section 9.1 so
that to be in line with latest upstream code.
Signed-off-by: Yanfeng Liu <yfliu2008@qq.com>
Before, some object API XML files conflicted when the include,
arch_include, and sel4_arch_include directories were combined:
- include/interfaces/sel4.xml
- arch_include/*/interfaces/sel4arch.xml
- sel4_arch_include/*/interfaces/sel4arch.xml
This commit renames them to:
- include/interfaces/object-api.xml
- arch_include/*/interfaces/object-api-arch.xml
- sel4_arch_include/*/interfaces/object-api-sel4-arch.xml
Now, when the include, arch_include, and sel4_arch_include directories
are combined, we are left with:
- interfaces/object-api.xml
- interfaces/object-api-arch.xml
- interfaces/object-api-sel4-arch.xml
Signed-off-by: Nick Spinale <nick@nickspinale.com>
Add a glossary with seL4-specific terms and their
definitions.
Remove chapter number from bibliography
Tweak Makefile for glossary
Signed-off-by: Birgit Brecknell <bbrcknl@gmail.com>
This way common error codes can be in their own file.
To use, add the xmlns:xi="http://www.w3.org/2001/XInclude
attribute to the top level node and use:
<xi:include href="file-to-include.xml"/>
The content of the file will be included verbatim.
Include files must be complete XML documents, but without
<?xml version="1.0" ?> at the top. Practically this means
all nodes within the file need to be contained in one root
element.
Caveat: There is no proper dependency for Xincludes files in
the Makefile, so you need to do make clean after changing an
included XML file!
Signed-off-by: Indan Zupancic <indan@nul.nu>
Put MCS-only invocations into their own groups and files. This solves
the problem that doxygen gets confused by duplicate function names with
the same parameters.
MCS/non-MCS is distinguished by evaluating the <condition> field in the
API XML definition. If the condition evaluates to true when
CONFIG_KERNEL_MCS is set, it is an MCS-only method, otherwise it is
assumed to be non-MCS or present in both configs.
Fixes#558
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
HTML_TIMESTAMP and LATEX_TIMESTAMP have been removed in more recent
doxygen versions. Since we are using the defaults, they are safe to
remove in our config file.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Different API groups may contain the same function name, for instance
IRQ_Control GetTrigger for RISC-V vs the same for ARM. Duplicate
function names with identical parameter lists confuse doxygen, leading
it to generate a single merged xml entry for both, which means one of
the entires will be missing and the other will be potentially wrong.
When the functions are placed in different files and different groups
at the same time, doxygen no longer is confused in all cases.
Therefore:
- generate a separate file for each API group
- generate a separate file group_defs.h that contains group definitions
and declares group nesting
Unfortunately, this does not seem to always work (e.g. the toplevel
MCS/non-MCS syscalls), so manual inspection is still necessary when
adding new calls and separate doxygen runs for duplicate function names
may be necessary. Generating separate files as above enables this
option, should it become necessary in the future.
Fixes#530
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Explicitly select xml parser (instead of html) via "lxml-xml" in
BeatifulSoup to avoid warning.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Provide seL4_BootInfoFrameSize (and seL4_BootInfoFrameBits) for
userland, to there is no longer a need to hard-code the 4 KiByte
assumption.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Guard the new implementation of 64-bit x86 guests behind a config
option. This is done so that existing projects that use x86_64 hosts
with ia32-bit guests can continue to be supported until either the old
feature is preferred to be deprecated, or support can be added to
support both simmultaneously.
Signed-off-by: Kent McLeod <kent@kry10.com>
Using the same cap twice on the same slot is possible for remapping,
but using the same cap twice in different tables or VSpaces will result
in an error.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Describe the difference in 3 and 4 level configs for AArch64 and point
to the libsel4 macros that abstract from the distinction.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Remove previous mix of \texttt and \obj, use \obj consistently when
referring to kernel objects.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- clarify terminology (cap vs object) in ASID Control and ASID pool
- same for page sharing
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Adjusting for VSpace object clarification and making sure terminology
is used consistently.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Rework the intro to the VSpace section for slightly improved clarity
and a more explicit definition of the distinctions between VSpace and
VSpace object, and between frame object and page capability.
Addresses #564
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- use a marker file to get a time stamp for when doxygen output was
last generated. Use that as a file target instead of a phony target
to avoid rebuilds when there is nothing to do.
- use static pattern rules so that `make` creates files instead of
giving up when the prerequisite of a pattern rule does not exist yet.
- remove file list duplication (needed because the static pattern
rules also need to mention these files)
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Remove options that are obsolete in doxygen >= 1.9. We only use default
values here, so everything should keep working as before in doxygen 1.8.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- fix broken links in the document
- small tweaks to make latex complain less:
- increase headheight by 2pt
- give small possible stretch value to parskip for filling pages
- use \sloppy for TOC to avoid unnecessary overfull hboxes
- make table placement more explicit (it currently doesn't fit
where [h] wants to place it, so allow it to go to the top of
the next page)
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
