summaryrefslogtreecommitdiff
path: root/abstract/value_domain.ml
diff options
context:
space:
mode:
authorAlex AUVOLAT <alex.auvolat@ens.fr>2014-05-07 19:04:38 +0200
committerAlex AUVOLAT <alex.auvolat@ens.fr>2014-05-07 19:04:38 +0200
commitd4ab85a1a6503cdbcb98c183c3357926d78da8a7 (patch)
treeb28ac764dd21ca7225ee46c6f4a4686648511fa3 /abstract/value_domain.ml
parent9ccef2c0850b73bf3d92f26bfa0aeacf933e1d17 (diff)
downloadSemVerif-Projet-d4ab85a1a6503cdbcb98c183c3357926d78da8a7.tar.gz
SemVerif-Projet-d4ab85a1a6503cdbcb98c183c3357926d78da8a7.zip
implement assert, print
Diffstat (limited to 'abstract/value_domain.ml')
-rw-r--r--abstract/value_domain.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml
index a0f082f..9cf6d76 100644
--- a/abstract/value_domain.ml
+++ b/abstract/value_domain.ml
@@ -25,4 +25,7 @@ module type VALUE_DOMAIN = sig
(* boolean test *)
val leq : t -> t -> t * t (* For intervals : [a, b] -> [c, d] -> ([a, min b d], [max a c, d]) *)
+
+ (* pretty-printing *)
+ val to_string : t -> string
end