diff options
| author | Alasdair Armstrong | 2019-05-14 15:46:10 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-05-14 15:46:10 +0100 |
| commit | 9d6734f717639f9babdec4441f8362bfeca10d66 (patch) | |
| tree | 91080afb376c38328de7262352f7c3217bc22719 /src/jib/jib_util.ml | |
| parent | 63d7f669f3d292315e4a353115284358ba7d5627 (diff) | |
| parent | f6cc45f2788dc777d1fa35aa9a216de994992288 (diff) | |
Merge branch 'smt_experiments' into sail2
Diffstat (limited to 'src/jib/jib_util.ml')
| -rw-r--r-- | src/jib/jib_util.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml index 378f5fae..3326d4ad 100644 --- a/src/jib/jib_util.ml +++ b/src/jib/jib_util.ml @@ -278,6 +278,8 @@ let string_of_name ?deref_current_exception:(dce=true) ?zencode:(zencode=true) = let string_of_op = function | Bnot -> "@not" + | Band -> "@and" + | Bor -> "@or" | List_hd -> "@hd" | List_tl -> "@tl" | Bit_to_bool -> "@bit_to_bool" @@ -896,6 +898,8 @@ let rec infer_call op vs = match op, vs with | Bit_to_bool, _ -> CT_bool | Bnot, _ -> CT_bool + | Band, _ -> CT_bool + | Bor, _ -> CT_bool | List_hd, [v] -> begin match cval_ctyp v with | CT_list ctyp -> ctyp |