diff options
| author | Alasdair Armstrong | 2019-03-25 14:43:40 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-03-25 14:44:33 +0000 |
| commit | a0aae7194dddab24d0c198d46b0e22fef04c2026 (patch) | |
| tree | 1e5adcf754c895efd4c063ccf05c05b1bfc52397 /src | |
| parent | aed0ec76a7497365ea436c4764f764e58ccc6685 (diff) | |
Typecheck: Use emod_int/ediv_int in sizeof rewriting
These are the correct versions for div/mod in the SMT solver
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index 92425daa..7af0ecff 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2210,15 +2210,17 @@ let rec rewrite_sizeof' env (Nexp_aux (aux, l) as nexp) = let exp = rewrite_sizeof' env nexp in mk_exp (E_app (mk_id "pow2", [exp])) + (* SMT solver div/mod is euclidian, so we must use those versions of + div and mod in lib/smt.sail *) | Nexp_app (id, [nexp1; nexp2]) when string_of_id id = "div" -> let exp1 = rewrite_sizeof' env nexp1 in let exp2 = rewrite_sizeof' env nexp2 in - mk_exp (E_app (mk_id "div", [exp1; exp2])) + mk_exp (E_app (mk_id "ediv_int", [exp1; exp2])) | Nexp_app (id, [nexp1; nexp2]) when string_of_id id = "mod" -> let exp1 = rewrite_sizeof' env nexp1 in let exp2 = rewrite_sizeof' env nexp2 in - mk_exp (E_app (mk_id "mod", [exp1; exp2])) + mk_exp (E_app (mk_id "emod_int", [exp1; exp2])) | Nexp_app _ | Nexp_id _ -> typ_error env l ("Cannot re-write sizeof(" ^ string_of_nexp nexp ^ ")") |