From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 test-suite/bugs/opened/2652b.v-disabled | 88 +++++++++++++++++++++++++++++++++
 1 file changed, 88 insertions(+)
 create mode 100644 test-suite/bugs/opened/2652b.v-disabled

(limited to 'test-suite/bugs/opened/2652b.v-disabled')

diff --git a/test-suite/bugs/opened/2652b.v-disabled b/test-suite/bugs/opened/2652b.v-disabled
new file mode 100644
index 00000000..b340436d
--- /dev/null
+++ b/test-suite/bugs/opened/2652b.v-disabled
@@ -0,0 +1,88 @@
+(* This used to show a bug in evarutil. which is fixed in 8.4 *)
+Require Import Strings.String.
+Require Import Classes.EquivDec.
+Require Import Lists.List.
+
+Inductive Owner : Type :=
+ | server : Owner
+ | client : Owner.
+
+Inductive ClassName : Type :=
+ | className : string -> ClassName.
+
+Inductive Label : Type :=
+ | label : nat -> Owner -> Label.
+
+Inductive Var : Type :=
+ | var : string -> Var.
+
+Inductive FieldName : Type :=
+ | fieldName : string -> Owner -> FieldName.
+
+Inductive MethodCall : Type :=
+ | methodCall : string -> MethodCall.
+
+Inductive Exp : Type :=
+ | varExp : Var -> Exp
+ | fieldReference : Var -> FieldName -> Exp
+ | methodCallExp : Var -> MethodCall -> list Var -> Exp
+ | allocation : ClassName -> list Var -> Exp
+ | cast : ClassName -> Var -> Exp.
+
+Inductive Stmt : Type :=
+ | assignment : Var -> Exp -> Label -> Stmt
+ | returnStmt : Var -> Label -> Stmt
+ | fieldUpdate : Var -> FieldName -> Exp -> Label -> Stmt.
+
+Inductive Konst : Type :=
+ | konst : ClassName -> (list (ClassName * FieldName)) -> list FieldName -> (list FieldName * FieldName) -> Konst.
+
+Inductive Method : Type :=
+ | method : ClassName -> MethodCall -> list (ClassName * Var) -> list (ClassName * Var) -> (list Stmt) -> Method.
+
+Inductive Class : Type :=
+ | class : ClassName -> ClassName -> (list (ClassName * FieldName)) -> (Konst * (list Method)) -> Class.
+
+Inductive Context : Type :=
+ | context : nat -> Context.
+
+Inductive HContext : Type :=
+ | heapContext : nat -> HContext.
+
+Inductive Location := loc : nat -> Location.
+
+Definition AbsLocation := ((Var * Context) +  (FieldName * HContext)) % type.
+
+Definition CallStack := list (Stmt * Context * Var) % type.
+
+Inductive TypeState : Type :=
+ | fresh : TypeState
+ | stale : TypeState.
+
+Definition Obj := (HContext * (FieldName -> option AbsLocation) * TypeState) % type.
+
+Definition Store := Location -> option Obj.
+
+Definition OwnerStore := Owner -> Store.
+
+Definition AbsStore := AbsLocation -> option (list Obj).
+
+Definition Stack := list (Var -> option Location).
+
+Definition Batch := list Location.
+
+Definition Sigma := (Stmt * Stack * OwnerStore * AbsStore * CallStack * Context * Batch) % type.
+
+Definition update {A : Type} {B : Type} `{EqDec A} `{EqDec B} (f : A -> B) (k : A) (v : B) : (A -> B) :=
+    fun k' => if equiv_decb k' k then v else f k'.
+
+Parameter succ : Label -> Stmt.
+
+Inductive concreteSingleStep : Sigma -> Sigma -> Prop :=
+ | fieldAssignmentLocal : forall v f_do  f o  so sigma_so hc m sigma'_so v' l st sigma absSigma cst c b sigma' sigma'' b',
+   Some (hc, m, fresh) = sigma_so(st(v)) -> sigma'_so = update sigma_so st(v) (Some (hc, update m f_do st(v'), fresh))
+   -> 
+   concreteSingleStep ((fieldUpdate v f_do (varExp v') l), st, sigma, absSigma, cst, c, b)
+                      (succ(l), st, sigma'', absSigma, cst, c, b').
+
+.
-- 
cgit v1.2.3