From 5f858a94e1085ffc097d960fb4ea74e211f8bd78 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 22 Jun 2021 17:25:59 +0200
Subject: [PATCH] explain our choice of integer division operator
---
iris_heap_lang/lang.v | 3 +++
1 file changed, 3 insertions(+)
diff --git a/iris_heap_lang/lang.v b/iris_heap_lang/lang.v
index f435cb81c..6a126402e 100644
--- a/iris_heap_lang/lang.v
+++ b/iris_heap_lang/lang.v
@@ -79,6 +79,9 @@ Inductive base_lit : Set :=
Inductive un_op : Set :=
| NegOp | MinusUnOp.
Inductive bin_op : Set :=
+ (** We use "quot" and "rem" instead of "div" and "mod" to
+ better match the behavior of 'real' languages:
+ -30/-4 == 7. ("div" would return 8.) *)
| PlusOp | MinusOp | MultOp | QuotOp | RemOp (* Arithmetic *)
| AndOp | OrOp | XorOp (* Bitwise *)
| ShiftLOp | ShiftROp (* Shifts *)
--
GitLab