Content of RPM cbmc-5.3-1.fc23.i686.rpm :
/usr/bin/cbmc
/usr/bin/goto-cc
/usr/bin/goto-instrument
/usr/share/doc/cbmc
/usr/share/doc/cbmc/CBMC-guide.pdf
/usr/share/doc/cbmc/CHANGELOG
/usr/share/doc/cbmc/html-manual
/usr/share/doc/cbmc/html-manual/api.shtml
/usr/share/doc/cbmc/html-manual/architecture.shtml
/usr/share/doc/cbmc/html-manual/binsearch.c
/usr/share/doc/cbmc/html-manual/boop-example
/usr/share/doc/cbmc/html-manual/boop-example/driver.c
/usr/share/doc/cbmc/html-manual/boop-example/driver.h
/usr/share/doc/cbmc/html-manual/boop-example/kdev_t.h
/usr/share/doc/cbmc/html-manual/boop-example/modules.h
/usr/share/doc/cbmc/html-manual/boop-example/spec.c
/usr/share/doc/cbmc/html-manual/cbmc-loops.shtml
/usr/share/doc/cbmc/html-manual/cbmc.shtml
/usr/share/doc/cbmc/html-manual/cegar-1.png
/usr/share/doc/cbmc/html-manual/counter.c
/usr/share/doc/cbmc/html-manual/counter.v
/usr/share/doc/cbmc/html-manual/expr.c
/usr/share/doc/cbmc/html-manual/file1.c
/usr/share/doc/cbmc/html-manual/file2.c
/usr/share/doc/cbmc/html-manual/footer.inc
/usr/share/doc/cbmc/html-manual/gcc-wrap.c
/usr/share/doc/cbmc/html-manual/goto-cc-apache.shtml
/usr/share/doc/cbmc/html-manual/goto-cc-linux.shtml
/usr/share/doc/cbmc/html-manual/goto-cc-rockbox.shtml
/usr/share/doc/cbmc/html-manual/goto-cc-variants.shtml
/usr/share/doc/cbmc/html-manual/goto-cc-visual-studio.shtml
/usr/share/doc/cbmc/html-manual/goto-cc.shtml
/usr/share/doc/cbmc/html-manual/header.inc
/usr/share/doc/cbmc/html-manual/hwsw-inputs.shtml
/usr/share/doc/cbmc/html-manual/hwsw-mapping.shtml
/usr/share/doc/cbmc/html-manual/hwsw-tutorial.shtml
/usr/share/doc/cbmc/html-manual/hwsw.shtml
/usr/share/doc/cbmc/html-manual/index.shtml
/usr/share/doc/cbmc/html-manual/installation-cbmc.shtml
/usr/share/doc/cbmc/html-manual/installation-plugin.shtml
/usr/share/doc/cbmc/html-manual/installation-satabs.shtml
/usr/share/doc/cbmc/html-manual/introduction.shtml
/usr/share/doc/cbmc/html-manual/libraries.shtml
/usr/share/doc/cbmc/html-manual/lock-example-fixed.c
/usr/share/doc/cbmc/html-manual/lock-example.c
/usr/share/doc/cbmc/html-manual/modeling-assertions.shtml
/usr/share/doc/cbmc/html-manual/modeling-floating-point.shtml
/usr/share/doc/cbmc/html-manual/modeling-nondet.shtml
/usr/share/doc/cbmc/html-manual/modeling-pointers.shtml
/usr/share/doc/cbmc/html-manual/properties.shtml
/usr/share/doc/cbmc/html-manual/refinement.png
/usr/share/doc/cbmc/html-manual/ring_buffer1.c
/usr/share/doc/cbmc/html-manual/ring_buffer2.c
/usr/share/doc/cbmc/html-manual/satabs-aeon.shtml
/usr/share/doc/cbmc/html-manual/satabs-background.shtml
/usr/share/doc/cbmc/html-manual/satabs-driver.shtml
/usr/share/doc/cbmc/html-manual/satabs-tutorials.shtml
/usr/share/doc/cbmc/html-manual/satabs.shtml
/usr/share/doc/cbmc/html-manual/states.png
/usr/share/licenses/cbmc
/usr/share/licenses/cbmc/LICENSE
/usr/share/man/man1/cbmc.1.gz
/usr/share/man/man1/goto-cc.1.gz
/usr/share/man/man1/goto-instrument.1.gz
3793335