Skip to content

Commit

Permalink
Don't add goblint_array_domain attribute to non-array variables
Browse files Browse the repository at this point in the history
  • Loading branch information
@sim642
sim642 committed Feb 21, 2024
1 parent 7c80a6e commit 93bfa3b
Show file tree
Hide file tree
Showing 10 changed files with 48 additions and 50 deletions.
2 changes: 1 addition & 1 deletion src/util/loopUnrolling.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
31 changes: 15 additions & 16 deletions tests/regression/55-loop-unrolling/01-simple-cases.t
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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() ;
Expand Down Expand Up @@ -50,7 +50,7 @@
void example1(void)
{
int a[5] ;
int i __attribute__((__goblint_array_domain__("unroll"))) ;
int i ;

{
i = 0;
Expand Down Expand Up @@ -106,7 +106,7 @@
void example2(void)
{
int a[5] ;
int i __attribute__((__goblint_array_domain__("unroll"))) ;
int i ;

{
i = 0;
Expand Down Expand Up @@ -162,7 +162,7 @@
void example3(void)
{
int a[10] ;
int i __attribute__((__goblint_array_domain__("unroll"))) ;
int i ;

{
i = 0;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -414,7 +414,7 @@
void example6(void)
{
int a[5] ;
int i __attribute__((__goblint_array_domain__("unroll"))) ;
int i ;
int top ;

{
Expand Down Expand Up @@ -476,7 +476,6 @@
return;
}
}
int update(int i ) __attribute__((__goblint_array_domain__("unroll"))) ;
int update(int i )
{

Expand All @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -886,7 +885,7 @@
void example9(void)
{
int a[5] ;
int i __attribute__((__goblint_array_domain__("unroll"))) ;
int i ;

{
i = 0;
Expand Down Expand Up @@ -958,7 +957,7 @@
void example10(void)
{
int a[5] ;
int i __attribute__((__goblint_array_domain__("unroll"))) ;
int i ;

{
i = 0;
Expand Down
4 changes: 2 additions & 2 deletions tests/regression/55-loop-unrolling/02-break.t
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
4 changes: 2 additions & 2 deletions tests/regression/55-loop-unrolling/03-break-right-place.t
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
2 changes: 1 addition & 1 deletion tests/regression/55-loop-unrolling/04-simple.t
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
4 changes: 2 additions & 2 deletions tests/regression/55-loop-unrolling/05-continue.t
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
31 changes: 15 additions & 16 deletions tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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() ;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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 ;

{
Expand Down Expand Up @@ -476,7 +476,6 @@
return;
}
}
int update(int i ) __attribute__((__goblint_array_domain__("unroll"))) ;
int update(int i )
{

Expand All @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down
10 changes: 5 additions & 5 deletions tests/regression/55-loop-unrolling/07-nested-unroll.t
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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() ;
Expand All @@ -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;
Expand Down
4 changes: 2 additions & 2 deletions tests/regression/55-loop-unrolling/09-weird.t
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
6 changes: 3 additions & 3 deletions tests/regression/55-loop-unrolling/10-continue-right-place.t
View file
Original file line number Diff line number Diff line change
@@ -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() ;
Expand All @@ -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;
Expand Down

0 comments on commit 93bfa3b

Please sign in to comment.