bench/check-ce/oracles/tuple1_Alt-Ergo,2.5.2_WP.oracle

   1 <check_ce:categorization>Categorizations of models:
   2 - Checked model 0: INCOMPLETE
   3   - Concrete RAC: INCOMPLETE (terminated because missing value for return value of call at "WHY3DATA/stdlib/mach/int.mlw", line 475, character 22 to line 476, character 45)
   4   - Abstract RAC: INCOMPLETE (terminated because missing value for return value of call at "WHY3DATA/stdlib/mach/int.mlw", line 475, character 22 to line 476, character 45)
   5 - Checked model 1: INCOMPLETE
   6   - Concrete RAC: INCOMPLETE (terminated because missing value for return value of call at "WHY3DATA/stdlib/mach/int.mlw", line 475, character 22 to line 476, character 45)
   7   - Abstract RAC: INCOMPLETE (terminated because missing value for return value of call at "WHY3DATA/stdlib/mach/int.mlw", line 475, character 22 to line 476, character 45)
   8 - Selected model 2: INCOMPLETE
   9   - Concrete RAC: INCOMPLETE (terminated because missing value for return value of call at "WHY3DATA/stdlib/mach/int.mlw", line 475, character 22 to line 476, character 45)
  10   - Abstract RAC: INCOMPLETE (terminated because missing value for return value of call at "WHY3DATA/stdlib/mach/int.mlw", line 475, character 22 to line 476, character 45)
  11 File "bench/check-ce/tuple1.mlw", line 7, characters 14-19:
  12 Sub-goal Integer overflow of goal swap'vc.
  13 Prover result is: Unknown (unknown) (9 steps).
  14 The following counterexample model could not be verified
  15   (both RAC terminated because missing value for return value of call at "WHY3DATA/stdlib/mach/int.mlw", line 475, character 22 to line 476, character 45):
  16 File int.mlw:
  17   Line 459:
  18     int63'int :
  19       int63
  20       ->
  21       int = [|{mach.int.Int63.int63'int => 4611686018427387902} =>
  22               4611686018427387902;
  23             {mach.int.Int63.int63'int => 2} => 2;
  24             {mach.int.Int63.int63'int => -4611686018427387904} =>
  25             -4611686018427387904; _ => 4611686018427387903|]
  26   Line 475:
  27     max_int : int63 = {mach.int.Int63.int63'int => 4611686018427387903}
  28   Line 477:
  29     min_int : int63 = {mach.int.Int63.int63'int => 4611686018427387903}
  30 File tuple1.mlw:
  31   Line 6:
  32     a : int63 = {mach.int.Int63.int63'int => 4611686018427387903}
  33     b : int63 = {mach.int.Int63.int63'int => 4611686018427387903}
  34   Line 7:
  35     a : int63 = {mach.int.Int63.int63'int => 4611686018427387903}
  36     b : int63 = {mach.int.Int63.int63'int => 4611686018427387903}
  37
  38 File "bench/check-ce/tuple1.mlw", line 7, characters 14-23:
  39 Sub-goal Integer overflow of goal swap'vc.
  40 Prover result is: Valid (10 steps).
  41
  42 File "bench/check-ce/tuple1.mlw", line 7, characters 3-8:
  43 Sub-goal Integer overflow of goal swap'vc.
  44 Prover result is: Valid (12 steps).
  45
  46 File "bench/check-ce/tuple1.mlw", line 7, characters 3-12:
  47 Sub-goal Integer overflow of goal swap'vc.
  48 Prover result is: Valid (13 steps).
  49
  50 File "bench/check-ce/tuple1.mlw", line 5, characters 38-43:
  51 Sub-goal Postcondition of goal swap'vc.
  52 Prover result is: Valid (16 steps).
  53