Changeset 2895 for src/RTLabs/RTLabs_partial_traces.ma
- Timestamp:
- Mar 16, 2013, 9:08:19 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLabs_partial_traces.ma
r2894 r2895 1488 1488 lemma init_state_is : ∀p,s. 1489 1489 make_initial_state p = OK ? s → 1490 𝚺b. match s with [ Callstate _ fd _ _ fs _ ⇒ fs = [ ] ∧ find_funct_ptr ? (make_global p) b = Some ? fd 1490 𝚺b. match s with [ Callstate fid fd _ _ fs _ ⇒ 1491 fs = [ ] ∧ 1492 fid = prog_main … p ∧ 1493 find_symbol ? (make_global p) (prog_main … p) = Some ? b ∧ 1494 find_funct_ptr ? (make_global p) b = Some ? fd 1491 1495 | _ ⇒ False ]. 1492 1496 #p #s … … 1496 1500 #E whd in E:(??%%); destruct 1497 1501 %{b} whd 1498 % // @Ef1502 % [% [%] ] // [ @Eb | @Ef ] 1499 1503 qed. 1500 1504 … … 1504 1508 cases s 1505 1509 [ #f #fs #m * 1506 | # vf #fd #args #dst #fs #m * #E1 #E2 destruct whd % //1510 | #fid #fd #args #dst #fs #m * * * #E1 #E2 #E3 #E4 destruct whd % /2/ 1507 1511 | #rv #rr #fs #m * 1508 1512 | #r *
Note: See TracChangeset
for help on using the changeset viewer.