tests/while_break2.scop

   1 start: 45
   2 end: 157
   3 indent: "\t"
   4 context: '[N] -> {  : N <= 2147483647 and N >= -2147483648 }'
   5 arrays:
   6 - context: '{  :  }'
   7   extent: '[N] -> { __pet_test_0[i, t] : N = 0 and i <= 9 and i >= 0 and t >= 0; __pet_test_0[0,
   8     t] : (N <= -1 and t >= 0) or (N >= 1 and t >= 0) }'
   9   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
  10   element_type: int
  11   element_size: 4
  12   uniquely_defined: 1
  13 - context: '{  :  }'
  14   extent: '[N] -> { a[] }'
  15   element_type: int
  16   element_size: 4
  17 statements:
  18 - line: 10
  19   domain: '[N] -> { [S_0[i, t] -> [1]] : N = 0 and i <= 9 and i >= 0 and t >= 0; [S_0[0,
  20     t] -> [1]] : (N <= -1 and t >= 0) or (N >= 1 and t >= 0) }'
  21   schedule: '[N] -> { S_0[i, t] -> [0, i, 0, t, 0] }'
  22   body:
  23     type: expression
  24     expr:
  25       type: op
  26       operation: =
  27       arguments:
  28       - type: access
  29         index: '[N] -> { S_0[i, t] -> __pet_test_0[(i), (t)] }'
  30         reference: __pet_ref_1
  31         read: 0
  32         write: 1
  33       - type: call
  34         name: f
  35   arguments:
  36   - type: access
  37     index: '[N] -> { S_0[i, t] -> __pet_test_0[(i), ((-1 + t) : t >= 1)] }'
  38     reference: __pet_ref_0
  39     read: 1
  40     write: 0
  41 - line: 11
  42   domain: '[N] -> { [S_1[i, t] -> [1]] : N = 0 and i <= 9 and i >= 0 and t >= 0; [S_1[0,
  43     t] -> [1]] : (N <= -1 and t >= 0) or (N >= 1 and t >= 0) }'
  44   schedule: '[N] -> { S_1[i, t] -> [0, i, 0, t, 1] }'
  45   body:
  46     type: expression
  47     expr:
  48       type: op
  49       operation: =
  50       arguments:
  51       - type: access
  52         index: '[N] -> { S_1[i, t] -> a[] }'
  53         reference: __pet_ref_3
  54         read: 0
  55         write: 1
  56       - type: int
  57         value: 5
  58   arguments:
  59   - type: access
  60     index: '[N] -> { S_1[i, t] -> __pet_test_0[(i), (t)] }'
  61     reference: __pet_ref_2
  62     read: 1
  63     write: 0
  64 - line: 14
  65   domain: '[N] -> { S_2[i] : N = 0 and i <= 9 and i >= 0 }'
  66   schedule: '[N] -> { S_2[i] -> [0, i, 2] }'
  67   body:
  68     type: expression
  69     expr:
  70       type: op
  71       operation: =
  72       arguments:
  73       - type: access
  74         index: '[N] -> { S_2[i] -> a[] }'
  75         reference: __pet_ref_4
  76         read: 0
  77         write: 1
  78       - type: int
  79         value: 6
  80 implications:
  81 - satisfied: 1
  82   extension: '[N] -> { __pet_test_0[i, t] -> __pet_test_0[i, t''] : N = 0 and t''
  83     <= t and i >= 0 and i <= 9 and t'' >= 0; __pet_test_0[0, t] -> __pet_test_0[0,
  84     t''] : (N >= 1 and t'' >= 0 and t'' <= t) or (N <= -1 and t'' >= 0 and t'' <=
  85     t) }'