Skip to content

Commit c924ee6

Browse files
committed
Add clarification to tests
1 parent cfd9395 commit c924ee6

File tree

2 files changed

+6
-0
lines changed
  • regression/contracts-dfcc
    • dont_skip_cprover_prefixed_vars_fail
    • dont_skip_cprover_prefixed_vars_pass

2 files changed

+6
-0
lines changed

regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,8 @@
11
void foo()
22
{
3+
// Initialize them with `nondet_int` to avoid them being ignored by DFCC.
4+
// DFCC ignores variables that are not read/written to outside the loop
5+
// or in the loop contracts.
36
int nondet_var = nondet_int();
47
int __VERIFIER_var = nondet_int();
58
int __CPROVER_var = nondet_int();

regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,8 @@
11
void foo()
22
{
3+
// Initialize them with `nondet_int` to avoid them being ignored by DFCC.
4+
// DFCC ignores variables that are not read/written to outside the loop
5+
// or in the loop contracts.
36
int nondet_var = nondet_int();
47
int __VERIFIER_var = nondet_int();
58
int __CPROVER_var = nondet_int();

0 commit comments

Comments
 (0)