CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
example.c
Go to the documentation of this file.
1// File just to allow smoke testing of Rust API while tests are run.
2
3int main(int argc, char *argv[])
4{
5 int arr[] = {0, 1, 2, 3};
6 __CPROVER_assert(arr[3] != 3, "expected failure: arr[3] == 3");
7}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
void __CPROVER_assert(__CPROVER_bool assertion, const char *description)
int main()
Definition example.cpp:18