bench/check-ce/array_records_poly.mlw

   1
   2
   3 module Array_records
   4
   5    use int.Int
   6    use array.Array
   7
   8    type value = int
   9    type index = int
  10
  11    function to_rep value: int
  12    meta "model_projection" function to_rep
  13
  14    type basic_record =
  15    {
  16       flag : bool;
  17       first_value : value;
  18       second_value : value;
  19    }
  20
  21    type array_of_records = array basic_record
  22
  23    let var_overwrite (a: array_of_records) (i: int) : unit
  24      requires { a[i] = {flag = true; first_value = 3; second_value = 5}}
  25      ensures { a[i].first_value = 42 }
  26    =
  27      a[i] <- {flag = a[i].flag; first_value= a[i].first_value; second_value = 69};
  28      a[i] <- {flag = a[i].flag; first_value= 42; second_value = a[i].second_value};
  29      a[i] <- {flag = a[i].flag; first_value= 23; second_value = a[i].second_value};
  30      a[i] <- {flag = false; first_value= a[i].first_value; second_value = a[i].second_value};
  31      assert {a[i].second_value = 69};
  32
  33 end