File tree Expand file tree Collapse file tree 3 files changed +42
-0
lines changed
jbmc/regression/jbmc/array-cell-sensitivity1 Expand file tree Collapse file tree 3 files changed +42
-0
lines changed Original file line number Diff line number Diff line change 1+ CORE
2+ Test.class
3+ --function Test.main --show-vcc --max-field-sensitivity-array-size 10
4+ symex_dynamic::dynamic_2_array#2\[\[0\]\] = symex_dynamic::dynamic_2_array#2\[0\]
5+ symex_dynamic::dynamic_2_array#2\[\[1\]\] = symex_dynamic::dynamic_2_array#2\[1\]
6+ symex_dynamic::dynamic_2_array#2\[\[2\]\] = symex_dynamic::dynamic_2_array#2\[2\]
7+ symex_dynamic::dynamic_2_array#2\[\[3\]\] = symex_dynamic::dynamic_2_array#2\[3\]
8+ symex_dynamic::dynamic_2_array#2\[\[4\]\] = symex_dynamic::dynamic_2_array#2\[4\]
9+ symex_dynamic::dynamic_2_array#2\[\[5\]\] = symex_dynamic::dynamic_2_array#2\[5\]
10+ symex_dynamic::dynamic_2_array#2\[\[6\]\] = symex_dynamic::dynamic_2_array#2\[6\]
11+ symex_dynamic::dynamic_2_array#2\[\[7\]\] = symex_dynamic::dynamic_2_array#2\[7\]
12+ symex_dynamic::dynamic_2_array#2\[\[8\]\] = symex_dynamic::dynamic_2_array#2\[8\]
13+ symex_dynamic::dynamic_2_array#2\[\[9\]\] = symex_dynamic::dynamic_2_array#2\[9\]
14+ symex_dynamic::dynamic_2_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1
15+ ^EXIT=0$
16+ ^SIGNAL=0$
17+ --
18+ --
19+ This checks that field sensitvity is still applied to an array of size 10
20+ when the max is set to 10.
Original file line number Diff line number Diff line change 1+ CORE
2+ Test.class
3+ --function Test.main --show-vcc --max-field-sensitivity-array-size 9
4+ ^EXIT=0$
5+ ^SIGNAL=0$
6+ symex_dynamic::dynamic_2_array#[0-9]\[1\]
7+ --
8+ symex_dynamic::dynamic_2_array#[0-9]\[\[[0-9]\]\]
9+ --
10+ This checks that field sensitvity is not applied to an array of size 10
11+ when the max is set to 9.
Original file line number Diff line number Diff line change 1+ CORE
2+ Test.class
3+ --function Test.main --show-vcc --no-array-field-sensitivity
4+ ^EXIT=0$
5+ ^SIGNAL=0$
6+ symex_dynamic::dynamic_2_array#[0-9]\[1\]
7+ --
8+ symex_dynamic::dynamic_2_array#[0-9]\[\[[0-9]\]\]
9+ --
10+ This checks that field sensitvity is not applied to arrays when
11+ no-array-field-sensitivity is used.
You can’t perform that action at this time.
0 commit comments