From 88075d446d51253c680131339f8b487c381affd2 Mon Sep 17 00:00:00 2001
From: pgupta751 <gupta751@purdue.edu>
Date: Mon, 3 Jun 2024 10:02:23 -0400
Subject: [PATCH] added new c0 program addTwo

---
 src/test/resources/verifier/addtwo.c0        | 15 +++++++++++++
 src/test/resources/verifier/addtwo.output.c0 | 23 ++++++++++++++++++++
 2 files changed, 38 insertions(+)
 create mode 100644 src/test/resources/verifier/addtwo.c0
 create mode 100644 src/test/resources/verifier/addtwo.output.c0

diff --git a/src/test/resources/verifier/addtwo.c0 b/src/test/resources/verifier/addtwo.c0
new file mode 100644
index 0000000..f73c727
--- /dev/null
+++ b/src/test/resources/verifier/addtwo.c0
@@ -0,0 +1,15 @@
+int add(int a, int b)
+    //@requires a > 0 && b > 0;
+    //@ensures ?;
+{
+    return a+b;
+}
+
+int main()
+    //@requires true;
+    //@ensures true;
+{
+    int sum = add(1, 3);
+    //@assert sum == 4;
+    return 0;
+}
\ No newline at end of file
diff --git a/src/test/resources/verifier/addtwo.output.c0 b/src/test/resources/verifier/addtwo.output.c0
new file mode 100644
index 0000000..158a872
--- /dev/null
+++ b/src/test/resources/verifier/addtwo.output.c0
@@ -0,0 +1,23 @@
+#use <runtime>
+int add(int a, int b, struct OwnedFields* _ownedFields);
+int main();
+
+int add(int a, int b, struct OwnedFields* _ownedFields)
+{
+  return a + b;
+}
+
+int main()
+{
+  int sum = 0;
+  int* _instanceCounter = NULL;
+  struct OwnedFields* _tempFields = NULL;
+  struct OwnedFields* _ownedFields = NULL;
+  _instanceCounter = alloc(int);
+  _ownedFields = initOwnedFields(_instanceCounter);
+  _tempFields = initOwnedFields(_instanceCounter);
+  sum = add(1, 3, _tempFields);
+  join(_ownedFields, _tempFields);
+  assert(sum == 4);
+  return 0;
+}