File tree 3 files changed +42
-0
lines changed
jbmc/regression/jbmc/array-cell-sensitivity1 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