Ignore:
Timestamp:
Feb 23, 2013, 5:05:03 PM (7 years ago)
Author:
campbell
Message:

It's easier to keep the real function identifier in front-end Callstates
than mucking around with the function pointer.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r2706 r2722  
    19231923  rg_find_symbol: ∀s.
    19241924    find_symbol ? ge s = find_symbol ? ge' s;
    1925   rg_find_funct: ∀v,f.
    1926     find_funct ? ge v = Some ? f
    1927     find_funct ? ge' v = Some ? (t f);
     1925  rg_find_funct_id: ∀v,f,id.
     1926    find_funct_id ? ge v = Some ? 〈f,id〉
     1927    find_funct_id ? ge' v = Some ? 〈t f,id〉;
    19281928  rg_find_funct_ptr: ∀b,f.
    19291929    find_funct_ptr ? ge b = Some ? f →
     
    29132913       cases (bindIO_inversion ??????? Hexec) #xfunc * #Heq_func #Hexec_func
    29142914       cases (bindIO_inversion ??????? Hexec_func) #xargs * #Heq_args #Hexec_args
    2915        cases (bindIO_inversion ??????? Hexec_args) #called_fundef * #Heq_fundef #Hexec_typeeq
     2915       cases (bindIO_inversion ??????? Hexec_args) * #called_fundef #fid * #Heq_fundef #Hexec_typeeq
    29162916       cases (bindIO_inversion ??????? Hexec_typeeq) #Htype_eq * #Heq_assert #Hexec_ret
    29172917       >(Hsim_expr … Heq_func) whd in match (m_bind ?????);
    29182918       >(exec_expr_sim_to_exec_exprlist … Hsim_expr … Heq_args)
    29192919       whd in ⊢ (??%?);
    2920        >(rg_find_funct … Hrelated … (opt_to_io_Value … Heq_fundef))
     2920       >(rg_find_funct_id … Hrelated … (opt_to_io_Value … Heq_fundef))
    29212921       whd in ⊢ (??%?); <fundef_type_simplify >Heq_assert
    29222922       whd in ⊢ (??%?); -Hexec -Hexec_func -Hexec_args -Hexec_typeeq lapply Hexec_ret -Hexec_ret
Note: See TracChangeset for help on using the changeset viewer.