diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index d5efd0d937..47f42ca830 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -299,7 +299,7 @@ class arrayVisitor = object inherit nopCilVisitor method! vvrbl info = - if not @@ (hasAttribute "goblint_array_domain" info.vattr || AutoTune0.is_large_array info.vtype) then + if Cil.isArrayType info.vtype && not @@ (hasAttribute "goblint_array_domain" info.vattr || AutoTune0.is_large_array info.vtype) then info.vattr <- addAttribute (Attr ("goblint_array_domain", [AStr "unroll"]) ) info.vattr; DoChildren end diff --git a/tests/regression/55-loop-unrolling/01-simple-cases.t b/tests/regression/55-loop-unrolling/01-simple-cases.t index a05ee4d010..4baf3c13d4 100644 --- a/tests/regression/55-loop-unrolling/01-simple-cases.t +++ b/tests/regression/55-loop-unrolling/01-simple-cases.t @@ -10,7 +10,7 @@ [Info] unrolling loop at 01-simple-cases.c:157:2-165:2 with factor 5 [Info] unrolling loop at 01-simple-cases.c:174:2-178:2 with factor 5 [Info] unrolling loop at 01-simple-cases.c:187:2-194:2 with factor 5 - extern void __goblint_check(int exp ) __attribute__((__goblint_array_domain__("unroll"))) ; + extern void __goblint_check(int exp ) ; extern void __goblint_assume(int exp ) ; extern void __goblint_assert(int exp ) ; extern void __goblint_assume_join() ; @@ -50,7 +50,7 @@ void example1(void) { int a[5] ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; { i = 0; @@ -106,7 +106,7 @@ void example2(void) { int a[5] ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; { i = 0; @@ -162,7 +162,7 @@ void example3(void) { int a[10] ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; { i = 0; @@ -219,8 +219,8 @@ void example4(void) { int a[10] ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; - int first_iteration __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; + int first_iteration ; { i = 0; @@ -319,8 +319,8 @@ void example5(void) { int a[4] ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; - int top __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; + int top ; { i = 0; @@ -414,7 +414,7 @@ void example6(void) { int a[5] ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; int top ; { @@ -476,7 +476,6 @@ return; } } - int update(int i ) __attribute__((__goblint_array_domain__("unroll"))) ; int update(int i ) { @@ -492,8 +491,8 @@ void example7(void) { int a[10] ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; - int tmp __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; + int tmp ; { i = 0; @@ -556,8 +555,8 @@ { int a[5] ; int b[5] ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; - int j __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; + int j ; { b[0] = 0; @@ -886,7 +885,7 @@ void example9(void) { int a[5] ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; { i = 0; @@ -958,7 +957,7 @@ void example10(void) { int a[5] ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; { i = 0; diff --git a/tests/regression/55-loop-unrolling/02-break.t b/tests/regression/55-loop-unrolling/02-break.t index 5f6928002a..cd94f32d6e 100644 --- a/tests/regression/55-loop-unrolling/02-break.t +++ b/tests/regression/55-loop-unrolling/02-break.t @@ -10,8 +10,8 @@ extern void __goblint_bounded(unsigned long long exp ) ; int main(void) { - int r __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int r ; + int i ; { r = 5; diff --git a/tests/regression/55-loop-unrolling/03-break-right-place.t b/tests/regression/55-loop-unrolling/03-break-right-place.t index bc183b00c1..e4d15ae90e 100644 --- a/tests/regression/55-loop-unrolling/03-break-right-place.t +++ b/tests/regression/55-loop-unrolling/03-break-right-place.t @@ -10,8 +10,8 @@ extern void __goblint_bounded(unsigned long long exp ) ; int main(void) { - int i __attribute__((__goblint_array_domain__("unroll"))) ; - int j __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; + int j ; { i = 0; diff --git a/tests/regression/55-loop-unrolling/04-simple.t b/tests/regression/55-loop-unrolling/04-simple.t index 49f5cc7e46..da38fd7b13 100644 --- a/tests/regression/55-loop-unrolling/04-simple.t +++ b/tests/regression/55-loop-unrolling/04-simple.t @@ -11,7 +11,7 @@ void main(void) { int a[5] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; { i = 0; diff --git a/tests/regression/55-loop-unrolling/05-continue.t b/tests/regression/55-loop-unrolling/05-continue.t index 6b1601c833..16731ad4e6 100644 --- a/tests/regression/55-loop-unrolling/05-continue.t +++ b/tests/regression/55-loop-unrolling/05-continue.t @@ -10,8 +10,8 @@ extern void __goblint_bounded(unsigned long long exp ) ; void main(void) { - int j __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int j ; + int i ; { j = 0; diff --git a/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t b/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t index ae6c4ba147..52fd7d868b 100644 --- a/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t +++ b/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t @@ -10,7 +10,7 @@ [Info] unrolling loop at 06-simple-cases-unrolled.c:157:2-165:2 with factor 5 [Info] unrolling loop at 06-simple-cases-unrolled.c:174:2-178:2 with factor 5 [Info] unrolling loop at 06-simple-cases-unrolled.c:187:2-194:2 with factor 5 - extern void __goblint_check(int exp ) __attribute__((__goblint_array_domain__("unroll"))) ; + extern void __goblint_check(int exp ) ; extern void __goblint_assume(int exp ) ; extern void __goblint_assert(int exp ) ; extern void __goblint_assume_join() ; @@ -50,7 +50,7 @@ void example1(void) { int a[5] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; { i = 0; @@ -106,7 +106,7 @@ void example2(void) { int a[5] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; { i = 0; @@ -162,7 +162,7 @@ void example3(void) { int a[10] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; { i = 0; @@ -219,8 +219,8 @@ void example4(void) { int a[10] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; - int first_iteration __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; + int first_iteration ; { i = 0; @@ -319,8 +319,8 @@ void example5(void) { int a[4] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; - int top __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; + int top ; { i = 0; @@ -414,7 +414,7 @@ void example6(void) { int a[5] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; int top ; { @@ -476,7 +476,6 @@ return; } } - int update(int i ) __attribute__((__goblint_array_domain__("unroll"))) ; int update(int i ) { @@ -492,8 +491,8 @@ void example7(void) { int a[10] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; - int tmp __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; + int tmp ; { i = 0; @@ -556,8 +555,8 @@ { int a[5] __attribute__((__goblint_array_domain__("unroll"))) ; int b[5] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; - int j __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; + int j ; { b[0] = 0; @@ -886,7 +885,7 @@ void example9(void) { int a[5] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; { i = 0; @@ -958,7 +957,7 @@ void example10(void) { int a[5] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; { i = 0; diff --git a/tests/regression/55-loop-unrolling/07-nested-unroll.t b/tests/regression/55-loop-unrolling/07-nested-unroll.t index a5c1c2f590..03455b7c8d 100644 --- a/tests/regression/55-loop-unrolling/07-nested-unroll.t +++ b/tests/regression/55-loop-unrolling/07-nested-unroll.t @@ -3,7 +3,7 @@ [Info] unrolling loop at 07-nested-unroll.c:6:5-10:5 with factor 5 [Info] unrolling loop at 07-nested-unroll.c:13:9-15:9 with factor 5 [Info] unrolling loop at 07-nested-unroll.c:12:5-16:5 with factor 5 - extern void __goblint_check(int exp ) __attribute__((__goblint_array_domain__("unroll"))) ; + extern void __goblint_check(int exp ) ; extern void __goblint_assume(int exp ) ; extern void __goblint_assert(int exp ) ; extern void __goblint_assume_join() ; @@ -14,10 +14,10 @@ int main(void) { int arr[10][10] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; - int j __attribute__((__goblint_array_domain__("unroll"))) ; - int i___0 __attribute__((__goblint_array_domain__("unroll"))) ; - int j___0 __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; + int j ; + int i___0 ; + int j___0 ; { i = 0; diff --git a/tests/regression/55-loop-unrolling/09-weird.t b/tests/regression/55-loop-unrolling/09-weird.t index 606f59acd8..502847c46e 100644 --- a/tests/regression/55-loop-unrolling/09-weird.t +++ b/tests/regression/55-loop-unrolling/09-weird.t @@ -10,8 +10,8 @@ extern void __goblint_bounded(unsigned long long exp ) ; void main(void) { - int j __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int j ; + int i ; { j = 0; diff --git a/tests/regression/55-loop-unrolling/10-continue-right-place.t b/tests/regression/55-loop-unrolling/10-continue-right-place.t index 3313122f03..1daab03c52 100644 --- a/tests/regression/55-loop-unrolling/10-continue-right-place.t +++ b/tests/regression/55-loop-unrolling/10-continue-right-place.t @@ -1,6 +1,6 @@ $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 11 --enable justcil --set dbg.justcil-printer clean 10-continue-right-place.c [Info] unrolling loop at 10-continue-right-place.c:7:3-15:3 with factor 11 - extern void __goblint_check(int exp ) __attribute__((__goblint_array_domain__("unroll"))) ; + extern void __goblint_check(int exp ) ; extern void __goblint_assume(int exp ) ; extern void __goblint_assert(int exp ) ; extern void __goblint_assume_join() ; @@ -10,8 +10,8 @@ extern void __goblint_bounded(unsigned long long exp ) ; int main(void) { - int i __attribute__((__goblint_array_domain__("unroll"))) ; - int j __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; + int j ; { i = 0;