diff options
| author | Alasdair Armstrong | 2019-05-01 16:27:45 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-05-01 16:32:28 +0100 |
| commit | 89f6064f6b0a1b5a6ba5e515ce38d7cf4ff37d22 (patch) | |
| tree | c5dacad57a9e44f53c876eac84bffcdd55d91894 /src/property.ml | |
| parent | 58d46e240315abb684823812ff1b2a9684653e5d (diff) | |
Jib: Refactor V_call
Get rid of separate V_op and V_unary constructors. jib.ott now defines
the valid operations for V_call including zero/sign extension, in such
a way that the operation ctyp can be inferred. Overall this makes the
IR less ad-hoc, and means we can share more code between SMT and C.
string_of_cval no longer used by c_backend, which now uses sgen_cval
following other sgen_ functions in the code generator, meaning
string_of_cval doesn't have to produce valid C code anymore and so can
be used for backend-agnostic debug and error messages.
Diffstat (limited to 'src/property.ml')
| -rw-r--r-- | src/property.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/property.ml b/src/property.ml index 84e9d734..9ef546a2 100644 --- a/src/property.ml +++ b/src/property.ml @@ -80,7 +80,7 @@ let add_property_guards props (Defs defs) = let add_constraints_to_funcl (FCL_aux (FCL_Funcl (id, Pat_aux (pexp, pexp_aux)), fcl_aux)) = let add_guard exp = (* FIXME: Use an assert *) - let exp' = mk_exp (E_block [mk_exp (E_app (mk_id "__assume", [mk_exp (E_constraint (List.fold_left nc_and nc_true constraints))])); + let exp' = mk_exp (E_block [mk_exp (E_app (mk_id "sail_assume", [mk_exp (E_constraint (List.fold_left nc_and nc_true constraints))])); strip_exp exp]) in try Type_check.check_exp (env_of exp) exp' (typ_of exp) with |