search

rems-project / cerberus

Cerberus C semantics
https://www.cl.cam.ac.uk/~pes20/cerberus/
Other
51 stars 28 forks source link

[CN] Terms should be printed with location information #550

Open dc-mak opened 1 month ago

dc-mak commented 1 month ago

Both in debug output, and in reports

dc-mak commented 1 month ago

This helps for debugging:

diff --git a/backend/cn/lib/logicalConstraints.ml b/backend/cn/lib/logicalConstraints.ml
index 59809311c..404901d0a 100644
--- a/backend/cn/lib/logicalConstraints.ml
+++ b/backend/cn/lib/logicalConstraints.ml
@@ -16,7 +16,7 @@ let equal = equal_logical_constraint
 let compare = compare_logical_constraint

 let pp = function
-  | T it -> IT.pp it
+  | T it -> IT.pp it ^^^ parens (Locations.pp (IT.loc it))
   | Forall ((s, bt), it) -> Pp.c_app !^"forall" [ Sym.pp s; BT.pp bt ] ^^ dot ^^^ IT.pp it