continue the example

C11-BackEnds/AutoCorres_wrapper/examples/Parse_for_loop.thy

@@ -61,8 +61,8 @@ text \<open>The invocation of AutoCorres:\<close>
 declare [[AutoCorres]]
 
 text \<open>Setup of AutoCorres for semantically representing this C element:\<close>
-declare_autocorres parse_for_loop [ ts_rules = nondet, unsigned_word_abs = f g h f2 ]
-
+declare_autocorres parse_for_loop [ ts_rules = nondet, unsigned_word_abs = g ]
+(*
 C\<open>
 /*
  * Copyright 2014, NICTA
@@ -86,18 +86,25 @@ int *f(int *i, int c)
   i[0]++;
   return i;
 }
+\<close>
+*)
+
+setup \<open>C_Module.C_Term.map_expression (fn _ => fn _ => fn _ => @{term "1 :: nat"})\<close>
+
+C \<open>
+  int g(int c)
+  { for (unsigned int j = 10; 0 < j; j--)
+      //* +@ INVARIANT \<open>0 < \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>j\<close> \<and> \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>j\<close> \<le> 10\<close>
+      //* +@ highlight
+      {
+        c = c + j;
+      }
+    return c;
+  }
+\<close>
 
-int g(int c)
-{ /** +@ INVARIANT: "\<lbrace> 0 <= \<acute>j \<and> \<acute>j <= 10 \<rbrace>"
-      +@ highlight */
-  for (unsigned int j = 10; 0 < j; j--)
-    // This is where the above invariant gets ultimately attached:
-    /** INVARIANT: "\<lbrace> 0 <= \<acute>j \<and> \<acute>j <= 10 \<rbrace>" */
-    {
-      c = c + j;
-    }
-  return c;
-}
+(*
+C \<open>
 
 int h(int c)
 {
@@ -115,6 +122,7 @@ int f2(int *a)
 }
 
 \<close>
+*)
 
 find_theorems name:"parse_for_loop"
 
@@ -135,7 +143,7 @@ lemma
           Guard DontReach {} SKIP
         CATCH SKIP
         END"
-  by (simp add: assms parse_for_loop_global_addresses.g_body_def)
+  oops
 
 text \<open> During the initialization phases of \<^theory_text>\<open>autocorres\<close>, the
 invariant information of \<^term>\<open>parse_for_loop_global_addresses.g_body\<close> gets lost