Skip to content

Commit

Permalink
added new c0 program addTwo
Browse files Browse the repository at this point in the history
  • Loading branch information
pgupta751 committed Jun 3, 2024
1 parent a50147b commit 88075d4
Show file tree
Hide file tree
Showing 2 changed files with 38 additions and 0 deletions.
15 changes: 15 additions & 0 deletions src/test/resources/verifier/addtwo.c0
Original file line number Diff line number Diff line change
@@ -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;
}
23 changes: 23 additions & 0 deletions src/test/resources/verifier/addtwo.output.c0
Original file line number Diff line number Diff line change
@@ -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;
}

0 comments on commit 88075d4

Please sign in to comment.