From ac3e40c4232c2f1f955c74c1fa096063fa1006a6 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 11 Nov 2022 21:48:11 +0000 Subject: [PATCH] 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. --- src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp index b11cdad6f22..4366c0e8a4a 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp @@ -105,6 +105,7 @@ const symbolt &dfcc_utilst::create_symbol( symbol.is_state_var = true; symbol.is_thread_local = true; symbol.is_file_local = true; + symbol.is_auxiliary = true; symbol.is_parameter = is_parameter; return symbol; } @@ -134,6 +135,7 @@ const symbolt &dfcc_utilst::create_static_symbol( symbol.is_state_var = true; symbol.is_thread_local = true; symbol.is_file_local = true; + symbol.is_auxiliary = true; symbol.is_parameter = false; return symbol; }