Add clarification to tests

diffblue · Nov 3, 2024 · c924ee6 · c924ee6
1 parent cfd9395
commit c924ee6
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 0 deletions.
diff --git a/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c
@@ -1,5 +1,8 @@
 void foo()
 {
+  // Initialize them with `nondet_int` to avoid them being ignored by DFCC.
+  // DFCC ignores variables that are not read/written to outside the loop
+  // or in the loop contracts.
   int nondet_var = nondet_int();
   int __VERIFIER_var = nondet_int();
   int __CPROVER_var = nondet_int();

diff --git a/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c
@@ -1,5 +1,8 @@
 void foo()
 {
+  // Initialize them with `nondet_int` to avoid them being ignored by DFCC.
+  // DFCC ignores variables that are not read/written to outside the loop
+  // or in the loop contracts.
   int nondet_var = nondet_int();
   int __VERIFIER_var = nondet_int();
   int __CPROVER_var = nondet_int();