bench/check-ce/oracles/array_mono_Alt-Ergo,2.5.4_SP.oracle

   1 File bench/check-ce/array_mono.mlw:
   2 Goal array'vc.
   3 Prover result is: Valid (1 steps).
   4
   5 <check_ce:categorization>Categorizations of models:
   6 - Checked model 0: INCOMPLETE
   7   - Concrete RAC: INCOMPLETE (terminated because Precondition of `([])` cannot be evaluated)
   8   - Abstract RAC: INCOMPLETE (terminated because Precondition of `([])` cannot be evaluated)
   9 - Checked model 1: BAD_CE
  10   - Concrete RAC: STUCK (failure in type invariant of type array at "bench/check-ce/array_mono.mlw", line 11, characters 16-27)
  11   - Abstract RAC: STUCK (failure in type invariant of type array at "bench/check-ce/array_mono.mlw", line 11, characters 16-27)
  12 - Selected model 2: NC
  13   - Concrete RAC: FAILURE (precondition at "bench/check-ce/array_mono.mlw", line 36, characters 4-8)
  14   - Abstract RAC: FAILURE (precondition at "bench/check-ce/array_mono.mlw", line 36, characters 4-8)
  15 File "bench/check-ce/array_mono.mlw", line 36, characters 4-8:
  16 Sub-goal Index in array bounds of goal f1'vc.
  17 Prover result is: Unknown (unknown) (2 steps).
  18 The program does not comply to the verification goal, for example during the
  19   following execution:
  20 File int.mlw:
  21   Line 13:
  22     Constant zero initialization
  23     zero = 0
  24   Line 14:
  25     Constant one initialization
  26     one = 1
  27 File array_mono.mlw:
  28   Line 35:
  29     a = {elts= UNDEFINED; length= 0}
  30     a = {elts= UNDEFINED; length= 0}
  31     Execution of main function `f1` with env:
  32       a = {elts= UNDEFINED; length= 0}
  33       zero = 0
  34       one = 1
  35   Line 36:
  36     (giant-step) execution of unimplemented function `([])`
  37       a = {elts= UNDEFINED; length= 0}
  38       i = 0
  39     Property failure at precondition of `([])` with:
  40       a = {elts= UNDEFINED; length= 0}
  41       i = 0
  42
  43 File "bench/check-ce/array_mono.mlw", line 41, characters 4-14:
  44 Sub-goal Index in array bounds of goal f2'vc.
  45 Prover result is: Valid (1 steps).
  46
  47 <check_ce:categorization>Categorizations of models:
  48 - Checked model 0: INCOMPLETE
  49   - Concrete RAC: INCOMPLETE (terminated because Precondition of `f2` cannot be evaluated)
  50   - Abstract RAC: INCOMPLETE (terminated because Precondition of `f2` cannot be evaluated)
  51 - Checked model 1: INCOMPLETE
  52   - Concrete RAC: INCOMPLETE (terminated because Postcondition of `([]<-)` cannot be evaluated)
  53   - Abstract RAC: INCOMPLETE (terminated because Postcondition of `([]<-)` cannot be evaluated)
  54 - Selected model 2: INCOMPLETE
  55   - Concrete RAC: INCOMPLETE (terminated because Postcondition of `([]<-)` cannot be evaluated)
  56   - Abstract RAC: INCOMPLETE (terminated because Postcondition of `([]<-)` cannot be evaluated)
  57 File "bench/check-ce/array_mono.mlw", line 40, characters 14-26:
  58 Sub-goal Postcondition of goal f2'vc.
  59 Prover result is: Unknown (unknown) (19 steps).
  60 The following counterexample model could not be verified
  61   (both RAC terminated because Postcondition of `([]<-)` cannot be evaluated):
  62 File array_mono.mlw:
  63   Line 38:
  64     a :  = {elts = [|0 => 0; 1 => 42; _ => 0|]; length = 3}
  65     a : array = {elts = [|0 => 0; 1 => 42; _ => 0|]; length = 3}
  66   Line 41:
  67     a : array = {elts = [|0 => 42; 1 => 42; _ => 0|]; length = 3}
  68     result :  = Tuple0
  69