Fix for struct-literal-initialisation with pointer-type fields.

JIRA VER-310

tools/c-parser/expression_translation.ML

@@ -730,7 +730,7 @@ in
       Signed _ => mk_zero (ctype_to_typ(thy, cty))
     | Unsigned _ => mk_zero (ctype_to_typ(thy, cty))
     | PlainChar => mk_zero IntInfo.char
-    | Ptr _ => mk_zero (ctype_to_typ(thy, cty))
+    | Ptr cty0 => mk_ptr (mk_zero addr_ty, ctype_to_typ(thy,cty0))
     | StructTy s => let
         val flds = case assoc(senv, s) of
                      NONE => raise Fail ("zero_term: no s. info for "^s)

tools/c-parser/testfiles/jiraver310.c

@@ -0,0 +1,24 @@
+struct s {
+  struct s *next;
+  int data;
+};
+
+int * globalptr;
+
+struct s f(int i)
+{
+  struct s node = {.data = i};
+  return node;
+}
+
+struct s g(int i)
+{
+  globalptr = 0;
+  return (struct s){.data = i, .next = 0};
+}
+
+struct s h(void)
+{
+  struct s node = {0};
+  return node;
+}

tools/c-parser/testfiles/jiraver310.thy

@@ -0,0 +1,21 @@
+theory jiraver310
+  imports "../CTranslation"
+begin
+
+  install_C_file "jiraver310.c"
+
+  context jiraver310
+  begin
+
+    thm f_body_def
+    thm g_body_def
+    
+    lemma "g_body = X"
+    apply (simp add: g_body_def)
+    oops
+    
+    thm h_body_def
+    
+  end (* context *)
+
+end (* theory *)