Name		Name	Last commit message	Last commit date
parent directory ..
GetLink.png		GetLink.png
README.md		README.md
binsearch.c		binsearch.c
c_to_ir.svg		c_to_ir.svg
cbmc_style.css		cbmc_style.css
cegar-1.png		cegar-1.png
counter.c		counter.c
driver.c		driver.c
driver.h		driver.h
expr.c		expr.c
expr.dot		expr.dot
expr.svg		expr.svg
file1.c		file1.c
file2.c		file2.c
gcc-wrap.c		gcc-wrap.c
goto_program.svg		goto_program.svg
ireptree.svg		ireptree.svg
kdev_t.h		kdev_t.h
lock-example-fixed.c		lock-example-fixed.c
lock-example.c		lock-example.c
modules.h		modules.h
pid.c		pid.c
pid.png		pid.png
refinement.png		refinement.png
ring_buffer1.c		ring_buffer1.c
ring_buffer2.c		ring_buffer2.c
spec.c		spec.c
states.png		states.png
xml_spec.md		xml_spec.md
xml_spec.tex		xml_spec.tex
xml_spec.xsd		xml_spec.xsd

README.md

This folder contains resources for the documentation.

XML Spec

The folllowing files relate to the specification of the XML trace output when using the --xml-ui flag.

xml_spec.xsd

Thexml_spec.xsd file is an XSD specification of the trace. You can validate an output xml file from CBMC using the following invocation:

$ cbmc --xml-ui main.c | \
  xmllint --schema xml_spec.xsd --xpath "cprover/result/goto_trace" -

xml_spec.tex

This is a LaTeX document describing the specification of the trace. It can be compiled to pdf using:

$ pdflatex -shell-escape xml_spec.tex

This requires:

texlive-latex-base
texlive-latex-extra (for minted package)