File tree 3 files changed +12
-21
lines changed
jbmc/regression/jbmc/array_nonconstsize_nonconstaccess 3 files changed +12
-21
lines changed Original file line number Diff line number Diff line change 1
- KNOWNBUG
1
+ CORE
2
2
FloatMultidim1.class
3
3
--function FloatMultidim1.f --cover location --unwind 3
4
4
\d+ of \d+ covered
5
5
^EXIT=0$
6
6
^SIGNAL=0$
7
- --
8
- --
9
- This crashes during symex, with error 'cannot unpack array of nonconst size'
10
- when trying to access the element of the array. Symex uses byte_extract_little
11
- _endian to access the element which does not get simplified (it seems the
12
- problem is that the types in the instruction do not match). TG-1121
7
+ y=1$
8
+ y=[2-4]$
9
+ y=([05-9]|[1-9][0-9]+|-[1-9][0-9]*)$
Original file line number Diff line number Diff line change 1
- KNOWNBUG
1
+ CORE
2
2
RefMultidim1.class
3
3
--function RefMultidim1.f --cover location --unwind 3
4
4
\d+ of \d+ covered
5
5
^EXIT=0$
6
6
^SIGNAL=0$
7
- --
8
- --
9
- This crashes during symex, with error 'cannot unpack array of nonconst size'
10
- when trying to access the element of the array. Symex uses byte_extract_little
11
- _endian to access the element which does not get simplified (it seems the
12
- problem is that the types in the instruction do not match). TG-1121
7
+ y=1$
8
+ y=[2-4]$
9
+ y=([05-9]|[1-9][0-9]+|-[1-9][0-9]*)$
Original file line number Diff line number Diff line change 1
- KNOWNBUG
1
+ CORE
2
2
RefMultidim2.class
3
3
--function RefMultidim2.f --cover location --unwind 3
4
4
\d+ of \d+ covered
5
5
^EXIT=0$
6
6
^SIGNAL=0$
7
- --
8
- --
9
- This crashes during symex, with error 'cannot unpack array of nonconst size'
10
- when trying to access the element of the array. Symex uses byte_extract_little
11
- _endian to access the element which does not get simplified (it seems the
12
- problem is that the types in the instruction do not match). TG-1121
7
+ y=1$
8
+ y=[2-4]$
9
+ y=([05-9]|[1-9][0-9]+|-[1-9][0-9]*)$
You can’t perform that action at this time.
0 commit comments