Changeset 457


Ignore:
Timestamp:
Jan 19, 2011, 3:06:10 PM (7 years ago)
Author:
campbell
Message:

Correct checking of function pointers.

Location:
Deliverables/D3.1/C-semantics
Files:
1 added
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Cexec.ma

    r400 r457  
    555555    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al;
    556556    ! fd ← find_funct ? ? ge vf;
    557     ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (typeof a));
     557    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (fun_typeof a));
    558558(* requires associativity of IOMonad, so rearrange it below
    559559    ! k' ← match lhs with
  • Deliverables/D3.1/C-semantics/Csem.ma

    r226 r457  
    982982(* * Transition relation *)
    983983
     984(* Strip off outer pointer for use when comparing function types. *)
     985ndefinition fun_typeof ≝
     986λe. match typeof e with
     987[ Tvoid ⇒ Tvoid
     988| Tint a b ⇒ Tint a b
     989| Tfloat a ⇒ Tfloat a
     990| Tpointer _ ty ⇒ ty
     991| Tarray a b c ⇒ Tarray a b c
     992| Tfunction a b ⇒ Tfunction a b
     993| Tstruct a b ⇒ Tstruct a b
     994| Tunion a b ⇒ Tunion a b
     995| Tcomp_ptr a ⇒ Tcomp_ptr a
     996].
     997
    984998(* XXX: note that cost labels in exprs expose a particular eval order. *)
    985999
     
    9971011      eval_exprlist ge e m al vargs tr2 →
    9981012      find_funct ?? ge vf = Some ? fd →
    999       type_of_fundef fd = typeof a →
     1013      type_of_fundef fd = fun_typeof a →
    10001014      step ge (State f (Scall (None ?) a al) k e m)
    10011015           (tr1⧺tr2) (Callstate fd vargs (Kcall (None ?) f e k) m)
     
    10061020      eval_exprlist ge e m al vargs tr3 →
    10071021      find_funct ?? ge vf = Some ? fd →
    1008       type_of_fundef fd = typeof a →
     1022      type_of_fundef fd = fun_typeof a →
    10091023      step ge (State f (Scall (Some ? lhs) a al) k e m)
    10101024           (tr1⧺tr2⧺tr3) (Callstate fd vargs (Kcall (Some ? 〈〈〈psp, loc〉, ofs〉, typeof lhs〉) f e k) m)
Note: See TracChangeset for help on using the changeset viewer.