From 1d90fa730df7d1cb2ee726d3b41b9915ae4e4e2e Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 3 Sep 2019 23:02:06 +0200
Subject: moved trapping_mode to a more appropriate place

---
 common/AST.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'common')

diff --git a/common/AST.v b/common/AST.v
index a91138c9..d98f954a 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -193,6 +193,15 @@ Definition chunk_of_type (ty: typ) :=
 Lemma chunk_of_Tptr: chunk_of_type Tptr = Mptr.
 Proof. unfold Mptr, Tptr; destruct Archi.ptr64; auto. Qed.
 
+(** Trapping mode: does undefined behavior result in a trap or an undefined value (e.g. for loads) *)
+Inductive trapping_mode : Type := TRAP | NOTRAP.
+
+Definition trapping_mode_eq : forall x y : trapping_mode,
+    { x=y } + { x <> y}.
+Proof.
+  decide equality.
+Defined.
+
 (** Initialization data for global variables. *)
 
 Inductive init_data: Type :=
-- 
cgit