Propagate guards from compound literals

This fixes JIRA VER-456

tools/c-parser/expression_translation.ML

@@ -788,7 +788,8 @@ fun mk_complit_upd thy cty rootty ((pth,value), ei) = let
         end
   fun rval s = mk_upds rootty pth (rval_of value s) $ (rval_of ei s)
 in
-  mk_rval(rval, cty, false, eileft ei, eiright ei) |> add_ei_guards ei
+  mk_rval(rval, cty, false, eileft ei, eiright ei)
+         |> add_ei_guards ei |> add_ei_guards value
 end
 
 

tools/c-parser/testfiles/jiraver456.c

@@ -0,0 +1,19 @@
+struct div_t {
+  unsigned q;
+};
+
+unsigned f0(unsigned n, unsigned d)
+{
+  return n/d;
+}
+
+struct div_t f1(unsigned n, unsigned d)
+{
+  struct div_t r = { n / d };
+  return r;
+}
+
+struct div_t f2(unsigned n, unsigned d)
+{
+  return (struct div_t){n/d};
+}

tools/c-parser/testfiles/jiraver456.thy

@@ -0,0 +1,34 @@
+theory jiraver456
+  imports "../CTranslation"
+  
+begin
+
+install_C_file "jiraver456.c"
+
+context jiraver456
+begin
+
+thm f0_body_def
+thm f1_body_def
+thm f2_body_def
+
+ML {*
+
+fun count c th = 
+let
+  val t = Thm.concl_of th
+  fun incifGuard t i = if t = c then i + 1 else i 
+in
+  fold_aterms incifGuard t 0
+end
+val f = count @{const Div_0};
+
+   (f @{thm f1_body_def} = 1 andalso f @{thm f2_body_def} = 1 andalso f @{thm f0_body_def} = 1) 
+   orelse
+   OS.Process.exit OS.Process.failure
+*}
+
+
+end
+
+end