bench/check-ce/oracles/threshold_Alt-Ergo,2.5.2_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) (6 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) (23 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 (terminated because 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 (terminated because 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 (18 steps).
  80 The following counterexample model could not be verified
  81   (both RAC terminated because 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 : t = {bv.BV128.t'int => 1}
  86   Line 633:
  87     t'int :
  88       t
  89       ->
  90       int = [|{bv.BV128.t'int => 2} => 2;
  91             {bv.BV128.t'int => 4294967295} => 4294967295;
  92             {bv.BV128.t'int => 128} => 128;
  93             _ =>
  94             if arg_04 = {bv.BV128.t'int => 0} \/
  95                arg_04 = {bv.BV128.t'int => 0}
  96             then 0 else 1|]
  97   Line 639:
  98     add : t -> t -> t = fun arg_07 arg_1 -> {bv.BV128.t'int => 2}
  99   Line 689:
 100     t'int :
 101       t1
 102       ->
 103       int = [|{bv.BV32.t'int => 4294967297} => 4294967297;
 104             {bv.BV32.t'int => 4294967295} => 4294967295;
 105             _ =>
 106             if arg_05 = {bv.BV32.t'int => 0} \/ arg_05 = {bv.BV32.t'int => 0}
 107             then 0 else if arg_05 = {bv.BV32.t'int => 1} then 1 else 32|]
 108   Line 837:
 109     toBig :
 110       t1
 111       ->
 112       t = [|{bv.BV32.t'int => 32} => {bv.BV128.t'int => 0};
 113           {bv.BV32.t'int => 32} => {bv.BV128.t'int => 1};
 114           _ => {bv.BV128.t'int => 1}|]
 115 File threshold.mlw:
 116   Line 26:
 117     max : t1 = {bv.BV32.t'int => 32}
 118     min : t1 = {bv.BV32.t'int => 32}
 119   Line 30:
 120     max : t1 = {bv.BV32.t'int => 32}
 121     min : t1 = {bv.BV32.t'int => 32}
 122
 123 <check_ce:categorization>Categorizations of models:
 124 - Checked model 0: BAD_CE
 125   - Concrete RAC: NORMAL
 126   - Abstract RAC: NORMAL
 127 - Selected model 1: INCOMPLETE
 128   - Concrete RAC: INCOMPLETE (terminated because missing value for return value of call to u_add at "bench/check-ce/threshold.mlw", line 30, characters 11-24)
 129   - Abstract RAC: INCOMPLETE (terminated because missing value for return value of call to u_add at "bench/check-ce/threshold.mlw", line 30, characters 11-24)
 130 File "bench/check-ce/threshold.mlw", line 27, characters 13-45:
 131 Sub-goal Postcondition of goal f'vc.
 132 Prover result is: Step limit exceeded (38 steps).
 133 The following counterexample model could not be verified
 134   (both RAC terminated because missing value for return value of call to u_add at "bench/check-ce/threshold.mlw", line 30, characters 11-24):
 135 File bv.mlw:
 136   Line 362:
 137     size_bv : t1 = {bv.BV32.t'int => 32}
 138     size_bv : t = {bv.BV128.t'int => 1}
 139   Line 633:
 140     t'int :
 141       t
 142       ->
 143       int = [|{bv.BV128.t'int => 4294967295} => 4294967295;
 144             {bv.BV128.t'int => 128} => 128; {bv.BV128.t'int => 0} => 0;
 145             _ => 1|]
 146   Line 689:
 147     t'int :
 148       t1
 149       ->
 150       int = [|{bv.BV32.t'int => 4} => 4; {bv.BV32.t'int => 3} => 3;
 151             _ =>
 152             if arg_09 = {bv.BV32.t'int => 0} \/ arg_09 = {bv.BV32.t'int => 0}
 153             then 0
 154             else if arg_09 = {bv.BV32.t'int => 1} \/
 155                     arg_09 = {bv.BV32.t'int => 1}
 156                  then 1 else 32|]
 157   Line 695:
 158     add : t1 -> t1 -> t1 = fun arg_010 arg_11 -> {bv.BV32.t'int => 4}
 159 File threshold.mlw:
 160   Line 26:
 161     max : t1 = {bv.BV32.t'int => 32}
 162     min : t1 = {bv.BV32.t'int => 32}
 163     n : t1 = {bv.BV32.t'int => 32}
 164   Line 27:
 165     max : t1 = {bv.BV32.t'int => 32}
 166     min : t1 = {bv.BV32.t'int => 32}
 167     result : t1 = {bv.BV32.t'int => 32}
 168     result : t1 = {bv.BV32.t'int => 32}
 169   Line 30:
 170     _x : t1 = {bv.BV32.t'int => 4}
 171     result : t1 = {bv.BV32.t'int => 32}
 172