nidhugg/benchmarks_tacas2015
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
# Quick info The ./run script (without arguments) can be used to select benchmarks and generate a table. # Files description benchmarks : source files for benchmarks cbmc : should be linked to the desired cbmc version convert : AWK script to convert ./run's output to a LaTex table. Used by texify data.tex : The data part of the latex table, generated by convert dporc : should be linked to the desired dporc version goto-instr : Script to connect the components needed to evaluate with goto-instrument metadata : comments from ./run's output. Used by texify originals : original version of benchmarks results : directory containing benchmark run results. ./run writes there run : Main script. Also calls texify. table.pdf : default name of the report generated by texify. table.tex : template to include data.tex. texify : single argument script, converts any of run's reports to data.tex and metadata # Regarding goto-instrument To run a benchmark under goto-instrument we used four components: - goto-cc : A compiler from C to GOTO programs - goto-instrument: A tool that converts a GOTO program to another GOTO program, including memory architecture constructs - satabs: A tool that abstracts the GOTO program into a Boolean program which can be fed to a model checker - boom: A model checker The ./goto-instr script connects all these components correctly. Due to incompatibilities between the available versions of the tools we used the following combination: 'Binary' refers to : http://www.cprover.org/satabs/download/satabs-3-2-linux-32.tgz 'Source' refers to : svn co http://www.cprover.org/svn/cbmc/releases/cbmc-4.5 - goto-cc : From the Binary - goto-instrument : Compiled from Source, to have the --minimum-interference option and fixes for some assertion failures. - satabs : From the Binary - boom : From the Binary
About
No description, website, or topics provided.
Resources
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published