aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/opened/2652b.v-disabled
blob: b340436d8742d96fedd9da4697cdc9c580c0adc1 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
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').

.