File: exists_in_forall.c

package info (click to toggle)
cbmc 6.6.0-4
  • links: PTS
  • area: main
  • in suites: forky, sid, trixie
  • size: 153,852 kB
  • sloc: cpp: 386,459; ansic: 114,466; java: 28,405; python: 6,003; yacc: 4,552; makefile: 4,041; lex: 2,487; xml: 2,388; sh: 2,050; perl: 557; pascal: 184; javascript: 163; ada: 36
file content (14 lines) | stat: -rw-r--r-- 378 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
 
#include <stdlib.h>

// clang-format off
int main(int argc, char **argv)
{
    int *i = malloc(sizeof(int));
    *i = 1;

    __CPROVER_assert(
        __CPROVER_forall { int z; (0 < z && z < 10) ==>
            __CPROVER_exists { int y; ( 10 < y && y < 20) && y == z + 10 && y > *i } },
        "for all z, there exists a y so that y = z + 10 and y > 1");
}
// clang-format on