Below are the source files for the examples used in the CAV 2010 paper. Each source file contains a description of what the example does, and what features of McVETO it stresses. The results are available on the left.

Some examples contain the function MakeChoice(). MakeChoice() is a special function used to signal to McVETO that the code makes a choice based on a non-deterministic number here. McVETO replaces return values from this function with random numbers.

Self Modififying Code

McVeto also supports self modifying code (SMC). An x86 SMC example is available (src x86 listing). Results for this testcase are available with the current results.

CAV '10 testcases

Below are the source code and assembly listings for the test cases used in the CAV 2010 paper.

Last edited: 2010-04-19