Skip to content

Commit ade1af1

Browse files
author
Remi Delmas
committed
CONTRACTS: use vars auxiliary for DFCC
The `is_auxiliary` flag is now set for instrumentation variables created for DFCC. This will reduce noise in counter examples.
1 parent 0484d76 commit ade1af1

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -105,6 +105,7 @@ const symbolt &dfcc_utilst::create_symbol(
105105
symbol.is_state_var = true;
106106
symbol.is_thread_local = true;
107107
symbol.is_file_local = true;
108+
symbol.is_auxiliary = true;
108109
symbol.is_parameter = is_parameter;
109110
return symbol;
110111
}
@@ -134,6 +135,7 @@ const symbolt &dfcc_utilst::create_static_symbol(
134135
symbol.is_state_var = true;
135136
symbol.is_thread_local = true;
136137
symbol.is_file_local = true;
138+
symbol.is_auxiliary = true;
137139
symbol.is_parameter = false;
138140
return symbol;
139141
}

0 commit comments

Comments
 (0)