bench/check-ce/oracles/threshold_Alt-Ergo,2.5.4_WP.oracle

   1 <check_ce:categorization>Categorizations of models:
   2 - Checked model 0: BAD_CE
   3   - Concrete RAC: NORMAL
   4   - Abstract RAC: NORMAL
   5 - Checked model 1: BAD_CE
   6   - Concrete RAC: NORMAL
   7   - Abstract RAC: NORMAL
   8 - Selected model 2: NC
   9   - Concrete RAC: FAILURE (precondition at "bench/check-ce/threshold.mlw", line 11, characters 11-20)
  10   - Abstract RAC: FAILURE (precondition at "bench/check-ce/threshold.mlw", line 11, characters 11-20)
  11 File "bench/check-ce/threshold.mlw", line 11, characters 11-20:
  12 Sub-goal Integer overflow of goal f'vc.
  13 Prover result is: Unknown (unknown) (5 steps).
  14 The program does not comply to the verification goal, for example during the
  15   following execution:
  16 File int.mlw:
  17   Line 13:
  18     Constant zero initialization
  19     zero = 0
  20   Line 14:
  21     Constant one initialization
  22     one = 1
  23 File int.mlw:
  24   Line 281:
  25     Constant min_int32 initialization
  26     min_int32 = (-2147483648)
  27   Line 282:
  28     Constant max_int32 initialization
  29     max_int32 = 2147483647
  30 File threshold.mlw:
  31   Line 8:
  32     n = 0
  33     min = epsilon x:int32. int32'int x = 2147483647
  34     max = epsilon x:int32. int32'int x = 2147483647
  35     n = 0
  36     min = epsilon x:int32. int32'int x = 2147483647
  37     max = epsilon x:int32. int32'int x = 2147483647
  38     Execution of main function `f` with env:
  39       n = 0
  40       min = epsilon x:int32. int32'int x = 2147483647
  41       max = epsilon x:int32. int32'int x = 2147483647
  42       zero = 0
  43       one = 1
  44       min_int32 = (-2147483648)
  45       max_int32 = 2147483647
  46   Line 11:
  47     (giant-step) execution of unimplemented function `(+)`
  48       a = epsilon x:int32. int32'int x = 2147483647
  49       b = epsilon x:int32. int32'int x = 2147483647
  50     Property failure at precondition of `(+)` with:
  51       a = epsilon x:int32. int32'int x = 2147483647
  52       b = epsilon x:int32. int32'int x = 2147483647
  53
  54 <check_ce:categorization>Categorizations of models:
  55 - Checked model 0: BAD_CE
  56   - Concrete RAC: NORMAL
  57   - Abstract RAC: NORMAL
  58 - Checked model 1: BAD_CE
  59   - Concrete RAC: NORMAL
  60   - Abstract RAC: NORMAL
  61 - Selected model 2: BAD_CE
  62   - Concrete RAC: FAILURE (precondition at "bench/check-ce/threshold.mlw", line 11, characters 11-20)
  63   - Abstract RAC: FAILURE (precondition at "bench/check-ce/threshold.mlw", line 11, characters 11-20)
  64 File "bench/check-ce/threshold.mlw", line 9, characters 13-33:
  65 Sub-goal Postcondition of goal f'vc.
  66 Prover result is: Unknown (unknown) (19 steps).
  67 Sorry, we don't have a good counterexample for you :(
  68
  69
  70 <check_ce:categorization>Categorizations of models:
  71 - Checked model 0: BAD_CE
  72   - Concrete RAC: NORMAL
  73   - Abstract RAC: NORMAL
  74 - Selected model 1: INCOMPLETE
  75   - Concrete RAC: INCOMPLETE (fatal rac error: missing value for return value of call to u_add at "bench/check-ce/threshold.mlw", line 30, characters 11-24)
  76   - Abstract RAC: INCOMPLETE (fatal rac error: missing value for return value of call to u_add at "bench/check-ce/threshold.mlw", line 30, characters 11-24)
  77 File "bench/check-ce/threshold.mlw", line 30, characters 11-24:
  78 Sub-goal Arithmetic overflow of goal f'vc.
  79 Prover result is: Step limit exceeded (17 steps).
  80 The following counterexample model could not be verified
  81   (both RAC fatal rac error: missing value for return value of call to u_add at "bench/check-ce/threshold.mlw", line 30, characters 11-24):
  82 File bv.mlw:
  83   Line 362:
  84     size_bv : t1 = {bv.BV32.t'int => 32}
  85     size_bv : t1 = {bv.BV32.t'int => 32}
  86     size_bv : t = {bv.BV128.t'int => 1}
  87     size_bv : t = {bv.BV128.t'int => 1}
  88   Line 633:
  89     t'int :
  90       t
  91       ->
  92       int = [|{bv.BV128.t'int => 2} => 2;
  93             {bv.BV128.t'int => 4294967295} => 4294967295;
  94             {bv.BV128.t'int => 128} => 128;
  95             _ =>
  96             if arg_04 = {bv.BV128.t'int => 0} \/
  97                arg_04 = {bv.BV128.t'int => 0}
  98             then 0 else 1|]
  99     t'int :
 100       t
 101       ->
 102       int = [|{bv.BV128.t'int => 2} => 2;
 103             {bv.BV128.t'int => 4294967295} => 4294967295;
 104             {bv.BV128.t'int => 128} => 128;
 105             _ =>
 106             if arg_04 = {bv.BV128.t'int => 0} \/
 107                arg_04 = {bv.BV128.t'int => 0}
 108             then 0 else 1|]
 109   Line 639:
 110     add : t -> t -> t = fun arg_07 arg_1 -> {bv.BV128.t'int => 2}
 111     add : t -> t -> t = fun arg_07 arg_1 -> {bv.BV128.t'int => 2}
 112   Line 689:
 113     t'int :
 114       t1
 115       ->
 116       int = [|{bv.BV32.t'int => 4294967297} => 4294967297;
 117             {bv.BV32.t'int => 4294967295} => 4294967295;
 118             _ =>
 119             if arg_05 = {bv.BV32.t'int => 0} \/ arg_05 = {bv.BV32.t'int => 0}
 120             then 0 else if arg_05 = {bv.BV32.t'int => 1} then 1 else 32|]
 121     t'int :
 122       t1
 123       ->
 124       int = [|{bv.BV32.t'int => 4294967297} => 4294967297;
 125             {bv.BV32.t'int => 4294967295} => 4294967295;
 126             _ =>
 127             if arg_05 = {bv.BV32.t'int => 0} \/ arg_05 = {bv.BV32.t'int => 0}
 128             then 0 else if arg_05 = {bv.BV32.t'int => 1} then 1 else 32|]
 129   Line 899:
 130     toBig :
 131       t1
 132       ->
 133       t = [|{bv.BV32.t'int => 32} => {bv.BV128.t'int => 0};
 134           {bv.BV32.t'int => 32} => {bv.BV128.t'int => 1};
 135           _ => {bv.BV128.t'int => 1}|]
 136     toBig :
 137       t1
 138       ->
 139       t = [|{bv.BV32.t'int => 32} => {bv.BV128.t'int => 0};
 140           {bv.BV32.t'int => 32} => {bv.BV128.t'int => 1};
 141           _ => {bv.BV128.t'int => 1}|]
 142 File threshold.mlw:
 143   Line 26:
 144     max : t1 = {bv.BV32.t'int => 32}
 145     max : t1 = {bv.BV32.t'int => 32}
 146     min : t1 = {bv.BV32.t'int => 32}
 147     min : t1 = {bv.BV32.t'int => 32}
 148
 149 <check_ce:categorization>Categorizations of models:
 150 - Checked model 0: BAD_CE
 151   - Concrete RAC: NORMAL
 152   - Abstract RAC: NORMAL
 153 - Selected model 1: INCOMPLETE
 154   - Concrete RAC: INCOMPLETE (fatal rac error: missing value for return value of call to u_add at "bench/check-ce/threshold.mlw", line 30, characters 11-24)
 155   - Abstract RAC: INCOMPLETE (fatal rac error: missing value for return value of call to u_add at "bench/check-ce/threshold.mlw", line 30, characters 11-24)
 156 File "bench/check-ce/threshold.mlw", line 27, characters 13-45:
 157 Sub-goal Postcondition of goal f'vc.
 158 Prover result is: Step limit exceeded (34 steps).
 159 The following counterexample model could not be verified
 160   (both RAC fatal rac error: missing value for return value of call to u_add at "bench/check-ce/threshold.mlw", line 30, characters 11-24):
 161 File bv.mlw:
 162   Line 362:
 163     size_bv : t1 = {bv.BV32.t'int => 32}
 164     size_bv : t1 = {bv.BV32.t'int => 32}
 165     size_bv : t = {bv.BV128.t'int => 1}
 166     size_bv : t = {bv.BV128.t'int => 1}
 167   Line 633:
 168     t'int :
 169       t
 170       ->
 171       int = [|{bv.BV128.t'int => 4294967295} => 4294967295;
 172             {bv.BV128.t'int => 128} => 128; {bv.BV128.t'int => 0} => 0;
 173             _ => 1|]
 174     t'int :
 175       t
 176       ->
 177       int = [|{bv.BV128.t'int => 4294967295} => 4294967295;
 178             {bv.BV128.t'int => 128} => 128; {bv.BV128.t'int => 0} => 0;
 179             _ => 1|]
 180   Line 689:
 181     t'int :
 182       t1
 183       ->
 184       int = [|{bv.BV32.t'int => 4} => 4; {bv.BV32.t'int => 3} => 3;
 185             _ =>
 186             if arg_09 = {bv.BV32.t'int => 0} \/ arg_09 = {bv.BV32.t'int => 0}
 187             then 0
 188             else if arg_09 = {bv.BV32.t'int => 1} \/
 189                     arg_09 = {bv.BV32.t'int => 1}
 190                  then 1 else 32|]
 191     t'int :
 192       t1
 193       ->
 194       int = [|{bv.BV32.t'int => 4} => 4; {bv.BV32.t'int => 3} => 3;
 195             _ =>
 196             if arg_09 = {bv.BV32.t'int => 0} \/ arg_09 = {bv.BV32.t'int => 0}
 197             then 0
 198             else if arg_09 = {bv.BV32.t'int => 1} \/
 199                     arg_09 = {bv.BV32.t'int => 1}
 200                  then 1 else 32|]
 201   Line 695:
 202     add : t1 -> t1 -> t1 = fun arg_010 arg_11 -> {bv.BV32.t'int => 4}
 203     add : t1 -> t1 -> t1 = fun arg_010 arg_11 -> {bv.BV32.t'int => 4}
 204 File threshold.mlw:
 205   Line 26:
 206     max : t1 = {bv.BV32.t'int => 32}
 207     max : t1 = {bv.BV32.t'int => 32}
 208     min : t1 = {bv.BV32.t'int => 32}
 209     min : t1 = {bv.BV32.t'int => 32}
 210     n : t1 = {bv.BV32.t'int => 32}
 211     n : t1 = {bv.BV32.t'int => 32}
 212   Line 27:
 213     result : t1 = {bv.BV32.t'int => 32}
 214   Line 30:
 215     _x : t1 = {bv.BV32.t'int => 4}
 216     _x : t1 = {bv.BV32.t'int => 4}
 217     result : t1 = {bv.BV32.t'int => 32}
 218