Changeset 2895


Ignore:
Timestamp:
Mar 16, 2013, 9:08:19 PM (4 years ago)
Author:
campbell
Message:

Match up function id from RTLabs Callstate with shadow stack,
use in observables proof.

Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/MeasurableToStructured.ma

    r2894 r2895  
    5555  do m ← init_mem … (λx.[Init_space x]) p;
    5656  let main ≝ prog_main ?? p in
    57   do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
     57  do b as Eb ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
    5858  do f as Ef ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr … ge b);
    5959  let s ≝ Callstate main f (nil ?) (None ?) (nil ?) m in
    6060  return (mk_RTLabs_ext_state (make_global p) s [b] ?).
    61 % [ @Ef | % ]
     61% [ % assumption | % ]
    6262qed.
    6363
     
    6767#p #s #E
    6868cases (bind_inversion ????? E) -E #m * #E1 #E
    69 cases (bind_inversion ????? E) -E #b * #E2 #E
     69cases (bind_as_inversion ????? E) -E #b * #Eb #E
    7070cases (bind_as_inversion ????? E) -E #f * #Ef #E
    7171whd in ⊢ (??%?); >E1
    72 whd in ⊢ (??%?); >E2
     72whd in ⊢ (??%?); >Eb
    7373whd in ⊢ (??%?); >Ef
    7474whd in E:(??%%) ⊢ (??%?); destruct
     
    8181#p #s #E
    8282cases (bind_inversion ????? E) -E #m * #E1 #E
    83 cases (bind_inversion ????? E) -E #b * #E2 #E
     83cases (bind_inversion ????? E) -E #b * #Eb #E
    8484cases (bind_inversion ????? E) -E #f * #Ef #E
    8585whd in E:(??%%); destruct
    86 %{[b]} % [ % [ @Ef | % ] ]
     86%{[b]} % [ % [ % assumption | % ] ]
    8787whd in ⊢ (??%?); >E1
    88 whd in ⊢ (??%?); >E2
     88whd in ⊢ (??%?); generalize in match (refl ??);
     89>Eb in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); #Eb'
    8990whd in ⊢ (??%?); generalize in match (refl ??);
    9091>Ef in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); #Ef' %
     
    140141lemma will_return_equiv : ∀ge,trace,depth,n,s,s',EX.
    141142  will_return_aux (pcs_to_cs … RTLabs_pcsys ge) depth trace →
    142   will_return ge depth s (make_flat_trace ge n s trace s' EX).
     143  ΣWR:will_return ge depth s (make_flat_trace ge n s trace s' EX).
     144    will_return_end … WR = ?.
     145[2: %{s'} @ft_stop ] (* XXX replace ? above? *)
    143146#ge #trace0 elim trace0
    144147[ #depth #n #s #s' #EX *
     
    169172      [ #EX #_
    170173        lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
    171         @wr_base
    172         destruct @CL
     174        %{(wr_base …)}
     175        [ destruct @CL
     176        | cases CFT #ctr #cs #cEV #cEX #cmake whd in ⊢ (??%?);
     177          whd in cEX:(??%%); destruct %
     178        ]
    173179      | * #s3 #tr3 #tl3 #EX *
    174180      ]
    175181    | #depth' whd in ⊢ (?% → ?); #H
    176182      lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
    177       @wr_ret
    178       [ destruct @CL
    179       | @IH @H
     183      cases (IH ???? (cft_EX … CFT) H) #WR' #WRe
     184      %{(wr_ret …)}
     185      [ @WR'
     186      | destruct @CL
     187      | @WRe
    180188      ]
    181189    ]
    182190  | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
    183     @wr_step [ %2 destruct @CL | @IH @H ]
     191    cases (IH ???? (cft_EX … CFT) H) #WR' #WRe
     192    %{(wr_step …)} [ @WR' | %2 destruct @CL | @WRe ]
    184193  | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
    185     @wr_call [ destruct @CL | @IH @H ]
     194    cases (IH ???? (cft_EX … CFT) H) #WR' #WRe
     195    %{(wr_call …)} [ @WR' | destruct @CL | @WRe ]
    186196  | cases (RTLabs_notail … CL)
    187197  | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
    188     @wr_step [ %1 destruct @CL | @IH @H ]
    189   ]
    190 ] qed.
     198    cases (IH ???? (cft_EX … CFT) H) #WR' #WRe
     199    %{(wr_step …)} [ @WR' | %1 destruct @CL | @WRe ]
     200  ]
     201] qed.
     202
    191203
    192204lemma extend_RTLabs_eval_statement : ∀ge. ∀s:RTLabs_ext_state ge. ∀tr,s'.
     
    446458] qed.
    447459
     460lemma really_no_label : ∀ge,s,obs.
     461  ¬as_costed (RTLabs_status ge) s →
     462  maybe_label ge s obs = obs.
     463#ge #s #obs
     464whd in ⊢ (?% → ??%?);
     465cases (as_label ??)
     466[ //
     467| #l * #H @⊥ @H % #E destruct
     468] qed.
     469
     470
    448471lemma call_ret_event : ∀ge,s,tr,s',obs.
    449472  step … RTLabs_ext_fullexec ge s = Value ??? 〈tr,s'〉 →
     
    478501] qed.
    479502
     503lemma as_call_cs_callee : ∀ge,s,CL,CL'.
     504  as_call_ident (RTLabs_status ge) «s,CL» = cs_callee (pcs_to_cs RTLabs_ext_pcsys ge) s CL'.
     505#ge * #s #S #M #CL #CL' cases (rtlabs_call_inv … CL) #fn * #fd * #args * #dst * #stk * #m #E
     506destruct %
     507qed.
     508
    480509lemma itot_call : ∀C,cs,s,rem,cs',trace.
    481510  ∀CL:match cs_classify C s with [ cl_call ⇒ True | _ ⇒ False ].
     
    491520qed.
    492521
    493 (* WIP
    494 lemma as_call_cs_callee : ∀ge,s,CL,CL'.
    495   as_call_ident (RTLabs_status ge) «s,CL» = cs_callee (pcs_to_cs RTLabs_ext_pcsys ge) s CL'.
    496 #ge * #s #S #M #CL #CL' cases (rtlabs_call_inv … CL) #fn * #fd * #args * #dst * #stk * #m #E
    497 destruct cases S in M CL' ⊢ %; [ * ] #fn' #S' * #M1 #M' #CL'
    498 whd in ⊢ (??%%); cases (symbol_for_block ??)
    499 
     522lemma itot_step : ∀ge,cs,s,tr,s',rem,cs',obs.
     523  as_classifier (RTLabs_status ge) s cl_other →
     524  step … RTLabs_ext_pcsys ge s = Value ??? 〈tr,s'〉 →
     525  intensional_trace_of_trace (pcs_to_cs … RTLabs_ext_pcsys ge) cs (〈s,tr〉::rem) = 〈cs',obs〉 →
     526  ∃obs'.
     527    obs = (intensional_events_of_events tr) @ obs' ∧
     528    intensional_trace_of_trace (pcs_to_cs … RTLabs_ext_pcsys ge) cs rem = 〈cs',obs'〉.
     529#ge #cs #s #tr #s' #rem #cs #obs #CL #EX
     530whd in ⊢ (??%? → ?); generalize in match (cs_callee ??) in ⊢ (% → ?);
     531whd in CL; change with (cs_classify (pcs_to_cs … RTLabs_ext_pcsys ge) ?) in CL:(??%?);
     532>CL #name whd in ⊢ (??%? → ?);
     533cases (intensional_trace_of_trace ???) #cs'' #trace'' #E whd in E:(??%?); destruct
     534%{trace''} /2/
     535qed.
    500536
    501537(* observables_trace_label_label emits the cost label for the first step of the
     
    527563  @(eq_obs_tal … EX ITOT)
    528564| cases tal
    529   [ #s1 #s2 #ST * #CL #CS #EX
     565  [ #s1 #s2 #ST #CL0 #CS #EX cases CL0 #CL
    530566    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX
    531567    whd in EX:(??%?); destruct
     
    555591    cases (eq_obs_tlr … EX ITOT')
    556592    #OBS' #E4 <E4 %
    557     [ >E3 <OBS' whd in ⊢ (??%?);
    558 
    559    
    560    
    561 
    562 ] qed.
    563 *)
    564 
     593    [ >E3 <OBS' whd in ⊢ (??%?); <(as_call_cs_callee … CL) %
     594    | %
     595    ]
     596  | #s1 #s2 #s3 #ST #CL #tlr #EX #ITOT @⊥ @(RTLabs_notail … CL)
     597  | #ends #s1 #s2 #s3 #s4 #ST #CL #AF #tlr #CS #tal' #EX
     598    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace0 * * #E1 >E1 #ST' #EX
     599    cases (call_ret_event … ST')
     600    [ #E2 #E3 >E2 >E3 | skip | %1 @CL ] #ITOT
     601    cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_ext_pcsys ge) ? = ?) in CL; >CL % ]
     602    #obs' * #E4 #ITOT'
     603    <(as_exec_eq_step … ST ST') in EX; #EX
     604    cases (exec_steps_split … EX) #trace1 * #trace2 * #s2'' * * #EX1 #EX2 #E
     605    >E in ITOT'; #ITOT' cases (int_trace_split … ITOT') #cs1 * #t1' * #t2' * * #ITOT1 #ITOT2 #Eobs
     606    lapply (eq_end_tlr … EX1) #E5 <E5 in EX1; #EX1
     607    cases (eq_obs_tlr … EX1 ITOT1) #ITOT1' #CS_CH <CS_CH in ITOT2 EX2; <E5 #ITOT2 #EX2
     608    cases (eq_obs_tal … EX2 ITOT2) #ITOT2' #CS_CH' %
     609    [ >E4 whd in ⊢ (??%?);
     610      <(as_call_cs_callee … CL) in ITOT1' ⊢ %; #ITOT1' >ITOT1'
     611      >(really_no_label … CS) in ITOT2'; #ITOT2' >ITOT2'
     612      <Eobs %
     613    | @CS_CH'
     614    ]
     615  | #ends #s1 #s2 #s3 #ST #tal' #CL #CS #EX
     616    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace0 * * #E1 >E1 #ST' #EX
     617    #ITOT  cases (itot_step … CL ST' ITOT) #obs' * #E >E #ITOT'
     618    <(as_exec_eq_step … ST ST') in EX; #EX
     619    cases (eq_obs_tal … EX ITOT')
     620    >(really_no_label … CS) #OBS' #CS_CH
     621    >(step_cost_event … ST') <OBS'
     622    % [ % | @CS_CH ]
     623  ]
     624] qed.
     625
     626
     627(* TODO move *)
     628lemma make_flat_trace_length : ∀ge,n,s1,trace,s2,EX.
     629  length_flat_trace io_out io_in ge s1 (make_flat_trace ge n s1 trace s2 EX) = n.
     630#ge #n0 elim n0
     631[ #s1 #trace #s2 #EX %
     632| #n #IH #s1 #trace #s2 #EX
     633  cases (exec_steps_S … EX) #_ * #tr * #s' * #tl * * #E1 #E2 #E3 destruct
     634  cases (cons_flat_trace ?????? EX)
     635  #tr'' #s'' #ST'' #EX'' #E >E whd in ⊢ (??%?); @eq_f @IH
     636] qed.
     637
     638
     639lemma cost_state_is_in_function : ∀ge,s,S,M.
     640  RTLabs_cost (mk_RTLabs_ext_state ge s S M) →
     641  ∃fn,S',id. S = fn::S' ∧ symbol_for_block ? ge fn = Some ? id.
     642#ge *
     643[ #f #fs #m * [*] #fn #S' * #FFP #M #_
     644  %{fn} %{S'} %{(symbol_of_function_block' … FFP)}
     645  % [ % | @symbol_of_function_block_ok [ >FFP % #E destruct | % ] ]
     646| #fid #fn #args #ret #fs #m #S #M *
     647| #rv #rr #fs #m #S #M *
     648| #r #S #M *
     649] qed.
    565650
    566651
     
    594679cases (initial_states_OK' … INIT) #S * #M #INIT'
    595680cases (extend_RTLabs_exec_steps ?? (mk_RTLabs_ext_state (make_global p) s0 S M) … EXEC1)
    596 #prefix'' * #S1 * #M1 letin s1' ≝ (mk_RTLabs_ext_state ? s1 S1 M1) #EXEC1'
     681#prefix'' * #S1 * #M1
     682lapply (label_to_return_state_labelled … LABEL_TO_RETURN EXEC2) #CS1
     683lapply (cost_state_is_in_function ge s1 S1 M1 CS1) * #fnb * #S1' * #fn * #ES1 #FN destruct
     684letin s1' ≝ (mk_RTLabs_ext_state ? s1 (fnb::S1') M1) #EXEC1'
     685cases (will_return_equiv … EXEC2 RETURNS) #RETURNS' #RETURNS_END
    597686lapply (make_label_return' ge 0 s1' (make_flat_trace ????? EXEC2) ????)
    598 [ @will_return_equiv assumption
    599 | @(label_to_return_state_labelled … LABEL_TO_RETURN EXEC2)
     687[ @RETURNS'
     688| @CS1
    600689| @(well_cost_labelled_exec_steps … EXEC1)
    601690  [ assumption
     
    603692  ]
    604693| @WCLge
    605 | * #s2' #rem #_ #tlr #LEN #STACK #_
    606 %{s1'} %{s2'} % [2: %{tlr}
     694| * #s2' #rem #_ #tlr #LEN #STACK whd in ⊢ (% → ?); whd in ⊢ (??%? → ?);
     695>RETURNS_END #E destruct
     696%{s1'} %{s2'} %{fn} %{tlr}
    607697% [ % [ %
    608698  [ whd in ⊢ (??%?);
     
    618708    ]
    619709 ]|
    620  ]|
     710 ]| cut (length_tlr … tlr = n)
     711    [ lapply (make_flat_trace_length ????? EXEC2) <LEN
     712      <plus_n_O @(λx.x) ]
     713    #LEN' <LEN' in EXEC2; #EXEC2
     714    cases (extend_RTLabs_exec_steps ?? s1' … EXEC2) #interesting'''
     715    lapply (eq_obs_tlr ????????? EXEC2)
    621716  ]
    622717]]
    623718
    624 
  • src/RTLabs/RTLabs_abstract.ma

    r2757 r2895  
    3535  match state with
    3636  [ State f fs m ⇒ All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) (f::fs) fn_stack
    37   | Callstate _ fd _ _ fs _ ⇒
     37  | Callstate fid fd _ _ fs _ ⇒
    3838      match fn_stack with
    3939      [ nil ⇒ False
    40       | cons h t ⇒ find_funct_ptr ? ge h = Some ? fd ∧
    41         All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs t
     40      | cons h t ⇒
     41          find_symbol … ge fid = Some ? h ∧
     42          find_funct_ptr ? ge h = Some ? fd ∧
     43          All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs t
    4244      ]
    4345  | Returnstate _ _ fs _ ⇒
     
    6971  | #ge' #vf #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
    7072    whd cases stk in mtc ⊢ %; [ * ]
    71     #hd #tl #H @H
     73    #hd #tl * * /3/
    7274  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
    7375  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #N #F #E1 #E2 #E3 #E4 destruct
     
    7678  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
    7779  ]
    78 | -s' #vf #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP
     80| -s' #fid #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP
    7981  whd % // -func_block cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
    8082  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
     
    232234    match s return λs':RTLabs_ext_state ge. RTLabs_classify s' = cl_call → ident with
    233235    [ mk_RTLabs_ext_state s' stk mtc0 ⇒
    234       match s' return λs'. Ras_Fn_Match ? s' ? → RTLabs_classify s' = cl_call → ident with
    235       [ Callstate _ fd _ _ _ _ ⇒
    236         match stk return λstk. Ras_Fn_Match ?? stk → ? → ident with
    237         [ nil ⇒ λmtc. ⊥
    238         | cons b _ ⇒ λmtc. λX. symbol_of_function_block … ge b ?
    239         ]
    240       | State f _ _ ⇒ λ_. λH.⊥
    241       | _ ⇒ λ_. λH.⊥
    242       ] mtc0
     236      match s' return λs'. RTLabs_classify s' = cl_call → ident with
     237      [ Callstate fid _ _ _ _ _ ⇒ λ_. fid
     238      | State f _ _ ⇒ λH.⊥
     239      | _ ⇒ λH.⊥
     240      ]
    243241    ] p
    244242  ].
     
    246244  cases (next_instruction f) in H;
    247245  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
    248 | 4,5: normalize in H; destruct (H)
    249 | cases mtc
    250 | cases mtc #FFP #_ >FFP % #E destruct (E)
     246| *: normalize in H; destruct (H)
    251247] qed.
    252248
  • src/RTLabs/RTLabs_partial_traces.ma

    r2894 r2895  
    14881488lemma init_state_is : ∀p,s.
    14891489  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
    14911495   | _ ⇒ False ].
    14921496#p #s
     
    14961500#E whd in E:(??%%); destruct
    14971501%{b} whd
    1498 % // @Ef
     1502% [% [%] ] // [ @Eb | @Ef ]
    14991503qed.
    15001504
     
    15041508cases s
    15051509[ #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/
    15071511| #rv #rr #fs #m *
    15081512| #r *
  • src/RTLabs/RTLabs_semantics.ma

    r2722 r2895  
    304304qed.
    305305
    306 definition func_block_of_exec : ∀ge,s,t,vf,fd,args,dst,fs,m.
    307   eval_statement ge s = Value ??? 〈t,Callstate vf fd args dst fs m〉 →
    308   Σb:block. find_funct_ptr … ge b = Some ? fd.
     306definition func_block_of_exec : ∀ge,s,t,fid,fd,args,dst,fs,m.
     307  eval_statement ge s = Value ??? 〈t,Callstate fid fd args dst fs m〉 →
     308  Σb:block. find_symbol … ge fid = Some ? b ∧ find_funct_ptr … ge b = Some ? fd.
    309309#ge *
    310310[ * #func #locals #next #nok #sp #dst #fs #m #tr #fid #fd #args #dst' #fs' #m'
     
    313313  (* Function call cases. *)
    314314  [ 8,9: #x #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd' #Efd @bind_ok #vs #Evs @jmeq_hackT #E normalize in E; destruct
    315     [ %{v} @Efd
     315    [ %{v} % assumption
    316316    | cases v in Efd;
    317       [ 4: * #b #off cases fd' #fd'' #fid' #Efd %{b} lapply (find_funct_id_drop ????? Efd) #Efd' whd in Efd':(??%?); cases (eq_offset ??) in Efd';
    318            [ #E @E | #E normalize in E; destruct ]
     317      [ 4: * #b #off cases fd' #fd'' #fid' #Efd %{b} cases (find_funct_id_ptr ????? Efd) #b' * * #E destruct #FS #FFPI %{FS} @FFPI
    319318      | *: normalize #A try #B try #C destruct
    320319      ]
  • src/RTLabs/RTLabs_traces.ma

    r2839 r2895  
    17851785lemma init_state_is : ∀p,s.
    17861786  make_initial_state p = OK ? s →
    1787   𝚺b. match s with [ Callstate _ fd _ _ fs _ ⇒ fs = [ ] ∧ find_funct_ptr ? (make_global p) b = Some ? fd
     1787  𝚺b. match s with [ Callstate fid fd _ _ fs _ ⇒
     1788       fs = [ ] ∧
     1789       fid = prog_main … p ∧
     1790       find_symbol ? (make_global p) (prog_main … p) = Some ? b ∧
     1791       find_funct_ptr ? (make_global p) b = Some ? fd
    17881792   | _ ⇒ False ].
    17891793#p #s
     
    17931797#E whd in E:(??%%); destruct
    17941798%{b} whd
    1795 % // @Ef
     1799% [% [%] ] // [ @Eb | @Ef ]
    17961800qed.
    17971801
     
    18011805cases s
    18021806[ #f #fs #m *
    1803 | #vf #fd #args #dst #fs #m * #E1 #E2 destruct whd % //
     1807| #fid #fd #args #dst #fs #m * * * #E1 #E2 #E3 #E4 destruct whd % /2/
    18041808| #rv #rr #fs #m *
    18051809| #r *
  • src/common/Globalenvs.ma

    r2722 r2895  
    594594  find_funct_id F ge v = Some ? 〈f,id〉 →
    595595  ∃b. v = Vptr (mk_pointer b zero_offset) ∧
     596  find_symbol F ge id = Some ? b ∧
    596597  find_funct_ptr_id F ge b = Some ? 〈f,id〉.
    597598#F #ge #v #f #id whd in ⊢ (??%? → ?);
     
    600601[ #X #E normalize in E; destruct
    601602| #f' #FF #E whd in E:(??%?);
    602   cases (find_funct_find_funct_ptr ???? FF) #b * #E1 #FFP %{b} %{E1}
     603  cases (find_funct_find_funct_ptr ???? FF) #b * #E1 #FFP %{b} % [ %
     604  [ @E1
     605  | @symbol_of_block_rev
     606    @symbol_of_function_block_ok [ >FFP % #E2 destruct ]
     607    destruct %
     608  ] ]
    603609  whd in ⊢ (??%?);
    604610  generalize in match (refl ??);
     
    12971303#A #B #t #ge #ge' #RG #v #f #id #FFI
    12981304cases (find_funct_id_ptr ????? FFI)
    1299 #b * #E1 #FFPI
     1305#b * * #E1 #FS #FFPI
    13001306cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SYM
    13011307lapply (rg_find_funct_ptr … RG … FFP) #FFP'
     
    13451351#tag #A #B #t #ge #ge' #RG #v #f #id #FFI
    13461352cases (find_funct_id_ptr ????? FFI)
    1347 #b * #E1 #FFPI
     1353#b * * #E1 #FS #FFPI
    13481354cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SYM
    13491355cases (rgg_find_funct_ptr … RG … FFP) #g #FFP' %{g}
Note: See TracChangeset for help on using the changeset viewer.