Skip to content

Commit 9ee880b

Browse files
tautschnigtautschnig
committed
Use get_fresh_aux_symbol to construct dynamic objects
This avoids use of a global variable and reuses central infrastructure instead of repeated local work. Note that this changes the names of dynamic objects as the suffix now includes a $ character, and need not have any suffix, as well as moving the counter out of the middle of C++/Java dynamic_X_array objects.
1 parent c9733f3 commit 9ee880b

File tree

22 files changed

+130
-142
lines changed

22 files changed

+130
-142
lines changed

‎jbmc/regression/jbmc-generics/constant_propagation/test.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ Test
33
--function Test.main --show-vcc
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\{-\d+\} symex_dynamic::dynamic_object1#2\.\.@Generic\.\[email protected]\.\.@class_identifier = "java::GenericSub"$
7-
^\{-\d+\} symex_dynamic::dynamic_object1#2\.\.@Generic\.\.key = NULL$
8-
^\{-\d+\} symex_dynamic::dynamic_object1#3\.\.@Generic\.\.x = 5$
6+
^\{-\d+\} symex_dynamic::dynamic_object#2\.\.@Generic\.\[email protected]\.\.@class_identifier = "java::GenericSub"$
7+
^\{-\d+\} symex_dynamic::dynamic_object#2\.\.@Generic\.\.key = NULL$
8+
^\{-\d+\} symex_dynamic::dynamic_object#3\.\.@Generic\.\.x = 5$
99
--
1010
byte_extract_(big|little)_endian
1111
--

‎jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-fail.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,9 @@ StringBuilderConstructors01
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
dynamic_object2=\{\s*\}
7+
dynamic_object\$0=\{\s*\}
88
--
99
^warning: ignoring
1010
--
11-
The check for dynamic_object2 is to make sure the array is created empty and
11+
The check for dynamic_object\$0 is to make sure the array is created empty and
1212
is not given arbitrary content before its final assignment.

‎jbmc/regression/jbmc-strings/long_string/test_abort.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Test
33
--function Test.checkAbort --trace --max-nondet-string-length 100000000
44
^EXIT=10$
55
^SIGNAL=0$
6-
dynamic_object[0-9]*=\(assignment removed\)
6+
dynamic_object\$?[0-9]*=\(assignment removed\)
77
--
88
--
99
This tests that the object does not appear in the trace, because concretizing

‎jbmc/regression/jbmc/VarLengthArrayTrace1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ VarLengthArrayTrace1
33
--trace --function VarLengthArrayTrace1.main
44
^EXIT=10$
55
^SIGNAL=0$
6-
dynamic_3_array\[1.*\]=10
6+
dynamic_array\$?\d*\[1.*\]=10
77
--
88
^warning: ignoring
99
assignment removed

‎jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,17 @@
11
CORE
22
Test
33
--function Test.main --show-vcc --max-field-sensitivity-array-size 10
4-
symex_dynamic::dynamic_2_array#2\[\[0\]\] =
5-
symex_dynamic::dynamic_2_array#2\[\[1\]\] =
6-
symex_dynamic::dynamic_2_array#2\[\[2\]\] =
7-
symex_dynamic::dynamic_2_array#2\[\[3\]\] =
8-
symex_dynamic::dynamic_2_array#2\[\[4\]\] =
9-
symex_dynamic::dynamic_2_array#2\[\[5\]\] =
10-
symex_dynamic::dynamic_2_array#2\[\[6\]\] =
11-
symex_dynamic::dynamic_2_array#2\[\[7\]\] =
12-
symex_dynamic::dynamic_2_array#2\[\[8\]\] =
13-
symex_dynamic::dynamic_2_array#2\[\[9\]\] =
14-
symex_dynamic::dynamic_2_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1
4+
symex_dynamic::dynamic_array#2\[\[0\]\] =
5+
symex_dynamic::dynamic_array#2\[\[1\]\] =
6+
symex_dynamic::dynamic_array#2\[\[2\]\] =
7+
symex_dynamic::dynamic_array#2\[\[3\]\] =
8+
symex_dynamic::dynamic_array#2\[\[4\]\] =
9+
symex_dynamic::dynamic_array#2\[\[5\]\] =
10+
symex_dynamic::dynamic_array#2\[\[6\]\] =
11+
symex_dynamic::dynamic_array#2\[\[7\]\] =
12+
symex_dynamic::dynamic_array#2\[\[8\]\] =
13+
symex_dynamic::dynamic_array#2\[\[9\]\] =
14+
symex_dynamic::dynamic_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1
1515
^EXIT=0$
1616
^SIGNAL=0$
1717
--

‎jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-9.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ Test
33
--function Test.main --show-vcc --max-field-sensitivity-array-size 9
44
^EXIT=0$
55
^SIGNAL=0$
6-
symex_dynamic::dynamic_2_array#[0-9]\[1\]
6+
symex_dynamic::dynamic_array#[0-9]\[1\]
77
--
8-
symex_dynamic::dynamic_2_array#[0-9]\[\[[0-9]\]\]
8+
symex_dynamic::dynamic_array#[0-9]\[\[[0-9]\]\]
99
--
1010
This checks that field sensitvity is not applied to an array of size 10
11-
when the max is set to 9.
11+
when the max is set to 9.

‎jbmc/regression/jbmc/array-cell-sensitivity1/test-no-array-field-sensitivity.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ Test
33
--function Test.main --show-vcc --no-array-field-sensitivity
44
^EXIT=0$
55
^SIGNAL=0$
6-
symex_dynamic::dynamic_2_array#[0-9]\[1\]
6+
symex_dynamic::dynamic_array#[0-9]\[1\]
77
--
8-
symex_dynamic::dynamic_2_array#[0-9]\[\[[0-9]\]\]
8+
symex_dynamic::dynamic_array#[0-9]\[\[[0-9]\]\]
99
--
1010
This checks that field sensitvity is not applied to arrays when
11-
no-array-field-sensitivity is used.
11+
no-array-field-sensitivity is used.

‎jbmc/regression/jbmc/array-cell-sensitivity1/test.desc

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,21 @@
11
CORE
22
Test
33
--function Test.main --show-vcc
4-
symex_dynamic::dynamic_2_array#2\[\[0\]\] =
5-
symex_dynamic::dynamic_2_array#2\[\[1\]\] =
6-
symex_dynamic::dynamic_2_array#2\[\[2\]\] =
7-
symex_dynamic::dynamic_2_array#2\[\[3\]\] =
8-
symex_dynamic::dynamic_2_array#2\[\[4\]\] =
9-
symex_dynamic::dynamic_2_array#2\[\[5\]\] =
10-
symex_dynamic::dynamic_2_array#2\[\[6\]\] =
11-
symex_dynamic::dynamic_2_array#2\[\[7\]\] =
12-
symex_dynamic::dynamic_2_array#2\[\[8\]\] =
13-
symex_dynamic::dynamic_2_array#2\[\[9\]\] =
14-
symex_dynamic::dynamic_2_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1
4+
symex_dynamic::dynamic_array#2\[\[0\]\] =
5+
symex_dynamic::dynamic_array#2\[\[1\]\] =
6+
symex_dynamic::dynamic_array#2\[\[2\]\] =
7+
symex_dynamic::dynamic_array#2\[\[3\]\] =
8+
symex_dynamic::dynamic_array#2\[\[4\]\] =
9+
symex_dynamic::dynamic_array#2\[\[5\]\] =
10+
symex_dynamic::dynamic_array#2\[\[6\]\] =
11+
symex_dynamic::dynamic_array#2\[\[7\]\] =
12+
symex_dynamic::dynamic_array#2\[\[8\]\] =
13+
symex_dynamic::dynamic_array#2\[\[9\]\] =
14+
symex_dynamic::dynamic_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1
1515
^EXIT=0$
1616
^SIGNAL=0$
1717
--
18-
symex_dynamic::dynamic_2_array#3\[\[[023456789]\]\] =
18+
symex_dynamic::dynamic_array#3\[\[[023456789]\]\] =
1919
--
2020
This checks that a write to a Java array with an unknown index uses a whole-array
2121
write followed by array-cell expansion, but one targeting a constant index uses

‎jbmc/regression/jbmc/array-cell-sensitivity2/test.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,13 @@
11
CORE
22
Test
33
--function Test.main --show-vcc
4-
symex_dynamic::dynamic_object6#3\.\.data =
5-
symex_dynamic::dynamic_object3#3\.\.data =
4+
symex_dynamic::dynamic_object\$3#3\.\.data =
5+
symex_dynamic::dynamic_object\$1#3\.\.data =
66
^EXIT=0$
77
^SIGNAL=0$
88
--
9-
symex_dynamic::dynamic_object6#3\.\.data = symex_dynamic::dynamic_object6#3\.data
10-
symex_dynamic::dynamic_object3#3\.\.data = symex_dynamic::dynamic_object3#3\.data
9+
symex_dynamic::dynamic_object\$3#3\.\.data = symex_dynamic::dynamic_object\$3#3\.data
10+
symex_dynamic::dynamic_object\$1#3\.\.data = symex_dynamic::dynamic_object\$1#3\.data
1111
--
1212
This checks that a write using a mix of field and array accessors uses a field-sensitive
1313
symbol (the data field of the possible ultimate target objects) rather than using

‎jbmc/regression/jbmc/json_trace3/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Test
44
activate-multi-line-match
55
^EXIT=10$
66
^SIGNAL=0$
7-
"lhs": "dynamic_object3\[1L?\]",\n *"mode": "java",\n *"sourceLocation": \{\n *"bytecodeIndex": "18",\n *"file": "Test\.java",\n *"function": "java::Test\.main:\(\[J\)V",\n *"line": "8"\n *\},\n *"stepType": "assignment",\n *"thread": 0,\n *"value": \{\n *"binary": "0000000000000000000000000000000000000000000000000000000000000001",\n *"data": "1L",\n *"name": "integer",\n *"type": "long",\n *"width": 64
7+
"lhs": "dynamic_object\$?\d*\[1L?\]",\n *"mode": "java",\n *"sourceLocation": \{\n *"bytecodeIndex": "18",\n *"file": "Test\.java",\n *"function": "java::Test\.main:\(\[J\)V",\n *"line": "8"\n *\},\n *"stepType": "assignment",\n *"thread": 0,\n *"value": \{\n *"binary": "0000000000000000000000000000000000000000000000000000000000000001",\n *"data": "1L",\n *"name": "integer",\n *"type": "long",\n *"width": 64
88
--
99
"name": "unknown"
1010
^warning: ignoring

‎jbmc/regression/jbmc/throwing-function-return-value/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
Test
33
--function Test.main --show-vcc
4-
java::Test\.main:\(Z\)V::14::t1!0@1#\d+ = address_of\(symex_dynamic::dynamic_object\d+\)
4+
java::Test\.main:\(Z\)V::14::t1!0@1#\d+ = address_of\(symex_dynamic::dynamic_object\$1\)
55
java::Test\.main:\(Z\)V::9::x!0@1#\d+ = java::Test\.main:\(Z\)V::9::x!0@1#\d+ \+ 5
66
java::Test\.g:\(\)I#return_value!0#[0-9]+ = 5
77
^EXIT=0$

‎jbmc/regression/strings-smoke-tests/java_parseint/test4.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Test4
55
^SIGNAL=0$
66
^\[.*assertion.1\].* line 6.* FAILURE$
77
^\[.*assertion.2\].* line 9.* FAILURE$
8-
dynamic_object2=\{ '5', '0' \}
9-
dynamic_object2=\{ 'X', 'Y', 'Z', 'W' \}
8+
dynamic_object\$0=\{ '5', '0' \}
9+
dynamic_object\$0=\{ 'X', 'Y', 'Z', 'W' \}
1010
--
1111
non equal types

‎jbmc/regression/strings-smoke-tests/java_parselong/test_other_branches_possible.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Test_other_branches_possible
55
^SIGNAL=0$
66
^\[.*assertion.1\].* line 6.* FAILURE$
77
^\[.*assertion.2\].* line 9.* FAILURE$
8-
dynamic_object2=\{ '5', '0' \}
9-
dynamic_object2=\{ 'X', 'Y', 'Z', 'W' \}
8+
dynamic_object\$0=\{ '5', '0' \}
9+
dynamic_object\$0=\{ 'X', 'Y', 'Z', 'W' \}
1010
--
1111
non equal types

‎regression/cbmc/array-cell-sensitivity5/test.desc

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,20 +1,20 @@
11
CORE
22
test.c
33
--show-vcc
4-
symex_dynamic::dynamic_object1#2\[\[1\]\] =
5-
symex_dynamic::dynamic_object1#2\[\[2\]\] =
6-
symex_dynamic::dynamic_object1#2\[\[3\]\] =
7-
symex_dynamic::dynamic_object1#2\[\[4\]\] =
8-
symex_dynamic::dynamic_object1#2\[\[5\]\] =
9-
symex_dynamic::dynamic_object1#2\[\[6\]\] =
10-
symex_dynamic::dynamic_object1#2\[\[7\]\] =
11-
symex_dynamic::dynamic_object1#2\[\[8\]\] =
12-
symex_dynamic::dynamic_object1#2\[\[9\]\] =
13-
symex_dynamic::dynamic_object1#3\[\[1\]\] =
4+
symex_dynamic::dynamic_object#2\[\[1\]\] =
5+
symex_dynamic::dynamic_object#2\[\[2\]\] =
6+
symex_dynamic::dynamic_object#2\[\[3\]\] =
7+
symex_dynamic::dynamic_object#2\[\[4\]\] =
8+
symex_dynamic::dynamic_object#2\[\[5\]\] =
9+
symex_dynamic::dynamic_object#2\[\[6\]\] =
10+
symex_dynamic::dynamic_object#2\[\[7\]\] =
11+
symex_dynamic::dynamic_object#2\[\[8\]\] =
12+
symex_dynamic::dynamic_object#2\[\[9\]\] =
13+
symex_dynamic::dynamic_object#3\[\[1\]\] =
1414
^EXIT=0$
1515
^SIGNAL=0$
1616
--
17-
symex_dynamic::dynamic_object1#[3-9]\[[0-9]+\]
17+
symex_dynamic::dynamic_object#[3-9]\[[0-9]+\]
1818
--
1919
This checks that a write with a non-constant index leads to a whole-array
2020
operation followed by expansion into individual array cells, while a write with

‎regression/cbmc/array-cell-sensitivity6/test.desc

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,20 +1,20 @@
11
CORE
22
test.c
33
--show-vcc
4-
symex_dynamic::dynamic_object1#2\[\[1\]\] =
5-
symex_dynamic::dynamic_object1#2\[\[2\]\] =
6-
symex_dynamic::dynamic_object1#2\[\[3\]\] =
7-
symex_dynamic::dynamic_object1#2\[\[4\]\] =
8-
symex_dynamic::dynamic_object1#2\[\[5\]\] =
9-
symex_dynamic::dynamic_object1#2\[\[6\]\] =
10-
symex_dynamic::dynamic_object1#2\[\[7\]\] =
11-
symex_dynamic::dynamic_object1#2\[\[8\]\] =
12-
symex_dynamic::dynamic_object1#2\[\[9\]\] =
13-
symex_dynamic::dynamic_object1#3\[\[1\]\] =
4+
symex_dynamic::dynamic_object#2\[\[1\]\] =
5+
symex_dynamic::dynamic_object#2\[\[2\]\] =
6+
symex_dynamic::dynamic_object#2\[\[3\]\] =
7+
symex_dynamic::dynamic_object#2\[\[4\]\] =
8+
symex_dynamic::dynamic_object#2\[\[5\]\] =
9+
symex_dynamic::dynamic_object#2\[\[6\]\] =
10+
symex_dynamic::dynamic_object#2\[\[7\]\] =
11+
symex_dynamic::dynamic_object#2\[\[8\]\] =
12+
symex_dynamic::dynamic_object#2\[\[9\]\] =
13+
symex_dynamic::dynamic_object#3\[\[1\]\] =
1414
^EXIT=0$
1515
^SIGNAL=0$
1616
--
17-
symex_dynamic::dynamic_object1#[3-9]\[[0-9]+\]
17+
symex_dynamic::dynamic_object#[3-9]\[[0-9]+\]
1818
--
1919
This checks that a write with a non-constant index leads to a whole-array
2020
operation followed by expansion into individual array cells, while a write with

‎regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
double_deref_with_pointer_arithmetic.c
33
--show-vcc
4-
^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \{ symex_dynamic::dynamic_object1#3\[\[0\]\], symex_dynamic::dynamic_object1#3\[\[1\]\] \}\[cast\(mod\(main::argc!0@1#1, 2\), signedbv\[64\]\)\]
5-
^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 2 : \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)\)
4+
^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \{ symex_dynamic::dynamic_object#3\[\[0\]\], symex_dynamic::dynamic_object#3\[\[1\]\] \}\[cast\(mod\(main::argc!0@1#1, 2\), signedbv\[64\]\)\]
5+
^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object\$[01]\) \? main::argc!0@1#1 = 2 : \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object\$[01]\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)\)
66
^EXIT=0$
77
^SIGNAL=0$
88
--

‎regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
double_deref_with_pointer_arithmetic_single_alias.c
33
--show-vcc
4-
\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object2\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)
4+
\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object\$0\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)
55
^EXIT=0$
66
^SIGNAL=0$
77
--

‎regression/cbmc/trace-values/trace-values.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ trace-values.c
1010
^ my_nested\[0.*\].array\[1.*\]=4 .*$
1111
^ my_nested\[1.*\].f=5 .*$
1212
^ junk\$object=7 .*$
13-
^ dynamic_object1\[1.*\]=8 .*$
13+
^ dynamic_object\[1.*\]=8 .*$
1414
^ my_nested\[1.*\](=\{ )?.f=0[ ,]
1515
^ my_nested\[1.*\](=\{ .f=0, )?.array=\{ 0, 4, 0 \}
1616
^ s\.f=42 \([0 ]+ 00101010\)$

‎src/goto-symex/auto_objects.cpp

Lines changed: 15 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -9,29 +9,28 @@ Author: Daniel Kroening, [email protected]
99
/// \file
1010
/// Symbolic Execution of ANSI-C
1111

12-
#include "goto_symex.h"
13-
12+
#include <util/fresh_symbol.h>
1413
#include <util/pointer_expr.h>
1514
#include <util/prefix.h>
1615
#include <util/std_code.h>
1716
#include <util/std_expr.h>
1817

18+
#include "goto_symex.h"
19+
1920
exprt goto_symext::make_auto_object(const typet &type, statet &state)
2021
{
21-
dynamic_counter++;
22-
2322
// produce auto-object symbol
24-
symbolt symbol;
25-
26-
symbol.base_name="auto_object"+std::to_string(dynamic_counter);
27-
symbol.name="symex::"+id2string(symbol.base_name);
28-
symbol.is_lvalue=true;
29-
symbol.type=type;
30-
symbol.mode=ID_C;
31-
32-
state.symbol_table.add(symbol);
33-
34-
return symbol_exprt(symbol.name, symbol.type);
23+
symbolt &symbol = get_fresh_aux_symbol(
24+
type,
25+
"symex",
26+
"auto_object",
27+
state.source.pc->source_location(),
28+
ID_C,
29+
state.symbol_table);
30+
symbol.is_thread_local = false;
31+
symbol.is_file_local = false;
32+
33+
return symbol.symbol_expr();
3534
}
3635

3736
void goto_symext::initialize_auto_object(const exprt &expr, statet &state)
@@ -85,7 +84,7 @@ void goto_symext::trigger_auto_object(const exprt &expr, statet &state)
8584
{
8685
const symbolt &symbol = ns.lookup(obj_identifier);
8786

88-
if(has_prefix(id2string(symbol.base_name), "auto_object"))
87+
if(has_prefix(id2string(symbol.base_name), "symex::auto_object"))
8988
{
9089
// done already?
9190
if(!state.get_level2().current_names.has_key(

‎src/goto-symex/goto_symex.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -29,8 +29,6 @@ Author: Daniel Kroening, [email protected]
2929

3030
#include <climits>
3131

32-
unsigned goto_symext::dynamic_counter=0;
33-
3432
void goto_symext::do_simplify(exprt &expr)
3533
{
3634
if(symex_config.simplify_opt)

‎src/goto-symex/goto_symex.h

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -776,9 +776,6 @@ class goto_symext
776776
/// \param code: The cleaned up output instruction
777777
virtual void symex_output(statet &state, const codet &code);
778778

779-
/// A monotonically increasing index for each created dynamic object
780-
static unsigned dynamic_counter;
781-
782779
void rewrite_quantifiers(exprt &, statet &);
783780

784781
/// \brief Symbolic execution paths to be resumed later

0 commit comments

Comments
 (0)