Creating your project
Step 0: Write your project. You begin by writing your function in C++ with printf debugging. Make a directory where you would like to create your C++ project andcd to that directory.
myapp.cpp with the following content:
Using our SDK functions
Recall that the basic SDK workflow is- Include the C++ header file.
- Use SDK functions in your code.
- Compile and link your code.
- Deploy your build.
Step 1: Include the C++ header file
If this is your first time using the Antithesis C++ SDK, make a directory for it and clone it from github.Step 2. Use SDK functions in your code
You wrote a function to multiply numbers by ten. What sorts of properties should it have? The output should always be even. You should also make sure you are testing a wide variety of inputs, such as both even and odd numbers. Modify the code. The modifications are individually explained below.- Lines 2-3 You imported the Antithesis C++ SDK and Antithesis C++ coverage instrumentation.
-
You added two assertions to times10.
- Line 8 You assert that the result is even using an Always Assertion. This is a fairly conventional assertion.
- Line 6 You insert a Sometimes Assertion, or an assertion that something will happen at least once across the entire testing session. You assert that sometimes during testing, the function will be called with an odd argument. The two types of assertions complement one another: Always Assertions assert that the behavior is correct, whereas Sometimes Assertions assert that you are testing under wide enough conditions to surface any potential incorrect behavior. In this case, the output would trivially be even if you only passed it even inputs — you must ensure your properties are not being trivially satisfied!
- Lines 14-17 You use randomness to call the function with many random values (between 0 and 500). Previously, you called the function with hardcoded values but now you will pass the function random values and test that the output is always even. This approach is more powerful but makes Sometimes Assertions necessary — now you must test that you are passing the function odd values, whereas previously the tests were hardcoded so you were certain that you were passing it odd values.
-
You call the random function
get_randomto draw a random number, and then pass this random number totimes10. You use a loop to do this fifty times in a row. Every time thetimes10function is called in this loop, it triggers the assertions in lines 5 & 7. -
In summary: You’ll test
times10by passing it a random integer fifty times in a row. You’ve asserted that all fifty outputs must be even and that at least one random input must be odd.
Step 3: Build your code
To ensure Antithesis testing of this function is as thorough as possible, you’ll need to compile your code with coverage instrumentation. Change the compile command line as follows:- Line 2 adds the include path for the Antithesis C++ SDK.
- Line 3 uses C++ 20, which is required to use the SDK.
- Line 4 adds instrumentation
- Line 5 turns on (optional) debug symbols.
- Lines 1,3, and 4 are unchanged from the previous link command.
- Line 2 sends the
--build-idflag to the linker
Step 4. Deploy your build
You’re now ready to build your project. If you’re building for local deployment then you would be done here, but suppose instead you intend to send your project to Antithesis for testing. Antithesis will explore your software and search for violations of the properties you’ve defined. You must send us containers as described in getting started.- The executable should be included in your container. In this example,
myapp/myapp_executable. - The instrumentation symbols should be symlinked (or moved) into a directory named
/symbolsin the root of the appropriate container image. In this case, we’ve generated an unstripped binary, so we’ll just copy or symlinkmyapp/myapp_executableinto/symbolsin the appropriate image.
This example is simplified compared to what the full quickstart guide describes. Note that the function
main is the workload and times10 is the software itself. There are no dependencies. The instrumentation symbols will go in the configuration image as stated.