summaryrefslogtreecommitdiff
path: root/src/ExpressionsUtils.ml
diff options
context:
space:
mode:
authorSidney Congard2022-06-30 14:54:15 +0200
committerSidney Congard2022-06-30 14:54:15 +0200
commitfdbbb82ff89b1d5141ec63bc2385936da3de3616 (patch)
treed48e3fa933280e8a275d2cfdab8f126e920e5f13 /src/ExpressionsUtils.ml
parent47691de8fe3dc32a29663d4d8343eb415ce1d81e (diff)
parent4f33892c81cdaf6aefaad9b7cef1456dcfead67c (diff)
Merge branch 'main' of github.com:Kachoc/aeneas into constants-v2
Complete the constants extraction by making all functions fail
Diffstat (limited to '')
-rw-r--r--src/ExpressionsUtils.ml10
1 files changed, 10 insertions, 0 deletions
diff --git a/src/ExpressionsUtils.ml b/src/ExpressionsUtils.ml
new file mode 100644
index 00000000..c3ccfb15
--- /dev/null
+++ b/src/ExpressionsUtils.ml
@@ -0,0 +1,10 @@
+module E = Expressions
+
+let unop_can_fail (unop : E.unop) : bool =
+ match unop with Neg | Cast _ -> true | Not -> false
+
+let binop_can_fail (binop : E.binop) : bool =
+ match binop with
+ | BitXor | BitAnd | BitOr | Eq | Lt | Le | Ne | Ge | Gt -> false
+ | Div | Rem | Add | Sub | Mul -> true
+ | Shl | Shr -> raise Errors.Unimplemented