Skip to content

Commit 0a68835

Browse files
committed
C_hide is no longer in use
The C_hide mechanism was removed in diffblue/cbmc@4e5bf6ea2bd03 As we cannot test hw-cbmc right now, the code is commented out.
1 parent ccfc907 commit 0a68835

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/hw-cbmc/set_inputs.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -71,6 +71,6 @@ void add_set_inputs(
7171
symbol.value=block;
7272

7373
// hide and inline
74-
symbol.type.set(ID_C_hide, true);
74+
// symbol.type.set(ID_C_hide, true);
7575
symbol.type.set(ID_C_inlined, true);
7676
}

0 commit comments

Comments
 (0)