c-parser: automated testing for JIRA VER-881

tools/c-parser/testfiles/jiraver881.c

@@ -8,26 +8,40 @@
  * @TAG(DATA61_BSD)
  */
 
-int f (void);
-
+int f(void);
 
 struct two_int {
-  int first; int second;
+    int first, second;
 };
 
-void
-g (void) {
-
-  int x;
-  unsigned int y;
-  struct two_int t;
-  int z[2];
-
-  x = f ();
-
-  y = f ();
-
-  t.first = f ();
-
-  z[0] = f ();
+void baseline1(void) {
+    int x;
+    x = f();
+}
+
+int baseline2(void) {
+    return f();
+}
+
+void test1(void) {
+    unsigned y;
+    y = f();
+}
+
+void test2(void) {
+    struct two_int t;
+    t.first = f();
+}
+
+void test3(void) {
+    int z[2];
+    z[0] = f();
+}
+
+unsigned test4(void) {
+    return f();
+}
+
+struct two_int test5(void) {
+    return (struct two_int) { .first = f() };
 }

tools/c-parser/testfiles/jiraver881.thy

@@ -21,7 +21,43 @@ context jiraver881 begin
 (* note that x is assigned directly from f(),
    but that compound lvars and y (different notional type) are
    assigned via explicit statements. *)
-thm g_body_def
+
+thm baseline1_body_def
+thm baseline2_body_def
+
+thm test1_body_def
+thm test2_body_def
+thm test3_body_def
+thm test4_body_def
+thm test5_body_def
+
+(* We expect the call to store the int retvals into ret__int and similar.
+   To test this, we pass the updater of the expected variable as the "upd" argument. *)
+ML \<open>
+fun check_ret func upd =
+let val fn_def = Proof_Context.get_thm @{context} (func ^ "_body_def")
+in
+  assert
+    (exists_Const (fn (name, _) => name = upd)
+       (term_of_thm fn_def))
+    ("assert failed: jiraver881 test for " ^ func ^ " call")
+end
+\<close>
+
+(* Should always work, since these are trivial assignments *)
+ML \<open>
+check_ret "baseline1" @{const_name x_'_update};
+check_ret "baseline2" @{const_name ret__int_'_update};
+\<close>
+
+(* Actual tests *)
+ML \<open>
+check_ret "test1" @{const_name ret__int_'_update};
+check_ret "test2" @{const_name ret__int_'_update};
+check_ret "test3" @{const_name ret__int_'_update};
+check_ret "test4" @{const_name ret__int_'_update};
+check_ret "test5" @{const_name ret__int_'_update};
+\<close>
 
 end