[isabelle] Norrish's C-parser and structs



Hi everyone,

I am using Michael Norrish's C-parser (in the version shipped with autocorres-0.1) to import a C-program to Isabelle, but I have some problems dealing with structs: I start with the following C-file

struct foo_t {
  unsigned cnt;
};

unsigned foo_cnt(struct foo_t *x) {
  return x->cnt;
}

and want to prove that the value returned by foo_cnt is the value of the field cnt_C of the abstracted version of the struct:

abbreviation "c_lift s ≡ lift_t⇡c (hst_mem s, hst_htd s)"

fun foo where
  "foo h n p = (case c_lift h p of Some g ⇒ cnt_C g = n | None ⇒ False)"

lemma "Γ ⊢ ⦃ σ. foo σ n ´x ⦄ ´ret__unsigned :== CALL foo_cnt (´x) ⦃ ´ret__unsigned = n ⦄"
  apply vcg
  apply (clarsimp simp: lift_t_g split: option.split_asm)
  apply (intro conjI)
   apply (rule c_guard_field_lvalue)
     apply (simp add: lift_t_g split: option.split_asm)
    apply fastforce
   apply (simp add: typ_uinfo_t_def)

This leaves me with the following subgoal, which I am not able to prove:

 1. ⋀globals x a.
lift_t⇡c (hrs_mem (t_hrs_' globals), hrs_htd (t_hrs_' globals)) x = Some a ⟹
       h_val (hrs_mem (t_hrs_' globals)) (Ptr &(x→[''cnt_C''])) = cnt_C a

So, how do I relate the projections of an abstracted struct to a field with the pointer access to said field of the concrete struct?

  -- Lars





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.