Changeset 2877


Ignore:
Timestamp:
Mar 15, 2013, 11:29:50 AM (4 years ago)
Author:
garnier
Message:

Correction of a bug in my former bug correction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2822 r2877  
    12111211            let 〈tmp2, uv2〉 as Etmp' ≝ alloc_tmp ? (Tpointer (typeof e1)) uv1 in
    12121212            OK ? «〈uv2, ul,
    1213                     (St_seq (St_store ? (Id ? tmp2) e1')
     1213                    (St_seq (St_assign ? tmp2 e1')
    12141214                    (St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args')
    1215                             (St_store (typ_of_type (typeof e1)) e1' (Id ? tmp))))〉, ?»
     1215                            (St_store (typ_of_type (typeof e1)) (Id ? tmp2) (Id ? tmp))))〉, ?»
    12161216        ]
    12171217    ]
     
    13621362             | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp)
    13631363             | 3: elim args' // ] ]
    1364 [ 5: whd @conj
     1364(*[ 5: whd @conj
    13651365     [ 1: cases e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
    13661366     | 2: @(alloc_tmp_preserves … Etmp') @(local_id_fresh_tmp … Etmp) ] ]     
     1367     *)
    13671368[ 1,3: elim e2' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
    13681369| 2: elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)
    1369 | 4,7: elim ef' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ]
    1370 [ 3: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
     1370| 4,8: elim ef' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ]
     1371[ 4: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
    13711372             | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp)
    13721373             | 3: elim args' // ]
    1373 | 2: #H @(alloc_tmp_preserves … Etmp' l ASTptr) @(alloc_tmp_preserves … Etmp l ASTptr) @H
    1374 | 1: #sz #sg #H @(alloc_tmp_preserves … Etmp' l) @(alloc_tmp_preserves … Etmp l) @H ]
     1374| 3: #H @(alloc_tmp_preserves … Etmp' l ASTptr) @(alloc_tmp_preserves … Etmp l ASTptr) @H
     1375| 2: #sz #sg #H @(alloc_tmp_preserves … Etmp' l) @(alloc_tmp_preserves … Etmp l) @H
     1376| 1: whd @conj
     1377     [ 1: @(local_id_fresh_tmp vars tmp2 uv2 (Tpointer (typeof e1)) uv1 Etmp')
     1378     | 2: @(alloc_tmp_preserves … Etmp') @(local_id_fresh_tmp vars tmp uv1 ((typeof e1)) uv Etmp) ] ]
    13751379try @refl (* Does (at least) the return_ok cases *)
    13761380try @(match fgens1 return λx.x=fgens1 → ? with
Note: See TracChangeset for help on using the changeset viewer.