Changeset 124 for Csemantics/Values.ma
 Timestamp:
 Sep 24, 2010, 10:31:32 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Values.ma
r14 r124 36 36 *) 37 37 38 ninductive ptr_class : Type ≝ 39  Universal : ptr_class 40  Data : ptr_class 41  IData : ptr_class 42  XData : ptr_class 43 (* pdata? I'd rather not... *) 44  Code : ptr_class. 45 46 ninductive ptr_class_compat : ptr_class → ptr_class → Prop ≝ 47  ptr_class_same : ∀pcl. ptr_class_compat pcl pcl 48  ptr_univ_l : ∀pcl. ptr_class_compat Universal pcl 49  ptr_univ_r : ∀pcl. ptr_class_compat pcl Universal. 50 51 nlemma ptr_class_compat_sym : ∀p,p'. ptr_class_compat p p' → ptr_class_compat p' p. 52 #p p' H; ninversion H; //; nqed. 53 54 (* TODO: should comparison and subtraction of pointers of different sorts 55 be supported? *) 56 38 57 ninductive val: Type[0] ≝ 39 58  Vundef: val 40 59  Vint: int > val 41 60  Vfloat: float > val 42  Vptr: block > int > val.61  Vptr: ptr_class → block > int > val. 43 62 44 63 ndefinition Vzero: val ≝ Vint zero. … … 63 82  Vint _ ⇒ match t with [ Tint ⇒ True  _ ⇒ False ] 64 83  Vfloat _ ⇒ match t with [ Tfloat ⇒ True  _ ⇒ False ] 65  Vptr _ _ ⇒ match t with [ Tint ⇒ True  _ ⇒ False ]84  Vptr _ _ _ ⇒ match t with [ Tint ⇒ True  _ ⇒ False ] 66 85  _ ⇒ False 67 86 ]. … … 81 100 match v with 82 101 [ Vint n ⇒ n ≠ zero 83  Vptr b ofs ⇒ True102  Vptr _ b ofs ⇒ True 84 103  _ ⇒ False 85 104 ]. … … 97 116 bool_of_val (Vint zero) false 98 117  bool_of_val_ptr: 99 ∀ b,ofs. bool_of_val (Vptrb ofs) true.118 ∀pty,b,ofs. bool_of_val (Vptr pty b ofs) true. 100 119 101 120 ndefinition neg : val → val ≝ λv. … … 152 171 match v with 153 172 [ Vint n ⇒ of_bool (int_eq n zero) 154  Vptr b ofs ⇒ Vfalse173  Vptr _ b ofs ⇒ Vfalse 155 174  _ ⇒ Vundef 156 175 ]. … … 178 197 [ Vint n1 ⇒ match v2 with 179 198 [ Vint n2 ⇒ Vint (add n1 n2) 180  Vptr b2 ofs2 ⇒ Vptrb2 (add ofs2 n1)181  _ ⇒ Vundef ] 182  Vptr b1 ofs1 ⇒ match v2 with183 [ Vint n2 ⇒ Vptr b1 (add ofs1 n2)199  Vptr pty b2 ofs2 ⇒ Vptr pty b2 (add ofs2 n1) 200  _ ⇒ Vundef ] 201  Vptr pty b1 ofs1 ⇒ match v2 with 202 [ Vint n2 ⇒ Vptr pty b1 (add ofs1 n2) 184 203  _ ⇒ Vundef ] 185 204  _ ⇒ Vundef ]. … … 190 209 [ Vint n2 ⇒ Vint (sub n1 n2) 191 210  _ ⇒ Vundef ] 192  Vptr b1 ofs1 ⇒ match v2 with193 [ Vint n2 ⇒ Vptr b1 (sub ofs1 n2)194  Vptr b2 ofs2 ⇒211  Vptr pty1 b1 ofs1 ⇒ match v2 with 212 [ Vint n2 ⇒ Vptr pty1 b1 (sub ofs1 n2) 213  Vptr pty2 b2 ofs2 ⇒ 195 214 if eqZb b1 b2 then Vint (sub ofs1 ofs2) else Vundef 196 215  _ ⇒ Vundef ] … … 352 371 [ Vint n1 ⇒ match v2 with 353 372 [ Vint n2 ⇒ of_bool (cmp c n1 n2) 354  Vptr b2 ofs2 ⇒373  Vptr pty2 b2 ofs2 ⇒ 355 374 if eq n1 zero then cmp_mismatch c else Vundef 356 375  _ ⇒ Vundef ] 357  Vptr b1 ofs1 ⇒ match v2 with358 [ Vptr b2 ofs2 ⇒376  Vptr pty1 b1 ofs1 ⇒ match v2 with 377 [ Vptr pty2 b2 ofs2 ⇒ 359 378 if eqZb b1 b2 360 379 then of_bool (cmp c ofs1 ofs2) … … 369 388 [ Vint n1 ⇒ match v2 with 370 389 [ Vint n2 ⇒ of_bool (cmpu c n1 n2) 371  Vptr b2 ofs2 ⇒390  Vptr pty2 b2 ofs2 ⇒ 372 391 if eq n1 zero then cmp_mismatch c else Vundef 373 392  _ ⇒ Vundef ] 374  Vptr b1 ofs1 ⇒ match v2 with375 [ Vptr b2 ofs2 ⇒393  Vptr pty1 b1 ofs1 ⇒ match v2 with 394 [ Vptr pty2 b2 ofs2 ⇒ 376 395 if eqZb b1 b2 377 396 then of_bool (cmpu c ofs1 ofs2) … … 409 428  _ ⇒ Vundef 410 429 ] 411  Vptr b ofs ⇒430  Vptr pty b ofs ⇒ 412 431 match chunk with 413 [ Mint32 ⇒ Vptr b ofs432 [ Mint32 ⇒ Vptr pty b ofs 414 433  _ ⇒ Vundef 415 434 ]
Note: See TracChangeset
for help on using the changeset viewer.