value2.ml1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84(*Generated by Lem from value2.lem.*) (*==========================================================================*) (* Sail *) (* *) (* Sail and the Sail architecture models here, comprising all files and *) (* directories except the ASL-derived Sail code in the aarch64 directory, *) (* are subject to the BSD two-clause licence below. *) (* *) (* The ASL derived parts of the ARMv8.3 specification in *) (* aarch64/no_vector and aarch64/full are copyright ARM Ltd. *) (* *) (* Copyright (c) 2013-2021 *) (* Kathyrn Gray *) (* Shaked Flur *) (* Stephen Kell *) (* Gabriel Kerneis *) (* Robert Norton-Wright *) (* Christopher Pulte *) (* Peter Sewell *) (* Alasdair Armstrong *) (* Brian Campbell *) (* Thomas Bauereiss *) (* Anthony Fox *) (* Jon French *) (* Dominic Mulligan *) (* Stephen Kell *) (* Mark Wassell *) (* Alastair Reid (Arm Ltd) *) (* *) (* All rights reserved. *) (* *) (* This work was partially supported by EPSRC grant EP/K008528/1 <a *) (* href="http://www.cl.cam.ac.uk/users/pes20/rems">REMS: Rigorous *) (* Engineering for Mainstream Systems</a>, an ARM iCASE award, EPSRC IAA *) (* KTF funding, and donations from Arm. This project has received *) (* funding from the European Research Council (ERC) under the European *) (* Unionâs Horizon 2020 research and innovation programme (grant *) (* agreement No 789108, ELVER). *) (* *) (* This software was developed by SRI International and the University of *) (* Cambridge Computer Laboratory (Department of Computer Science and *) (* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") *) (* and FA8750-10-C-0237 ("CTSRD"). *) (* *) (* Redistribution and use in source and binary forms, with or without *) (* modification, are permitted provided that the following conditions *) (* are met: *) (* 1. Redistributions of source code must retain the above copyright *) (* notice, this list of conditions and the following disclaimer. *) (* 2. Redistributions in binary form must reproduce the above copyright *) (* notice, this list of conditions and the following disclaimer in *) (* the documentation and/or other materials provided with the *) (* distribution. *) (* *) (* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) (* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) (* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) (* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) (* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) (* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) (* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) (* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) (* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) (* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) (* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) (* SUCH DAMAGE. *) (*==========================================================================*) open Lem_pervasives open Sail2_values type vl = | VL_bits of bitU list * bool | VL_bit of bitU | VL_bool of bool | VL_unit | VL_int of Nat_big_num.num | VL_string of string | VL_real of string | VL_empty_list | VL_enum of string | VL_ref of string | VL_undefined