Initial commit

This commit is contained in:
Bassem Girgis
2018-12-20 17:34:07 -06:00
parent 7a2d899662
commit 81b4b9e273
34743 changed files with 5940233 additions and 0 deletions

View File

@@ -0,0 +1,11 @@
#include <stdio.h>
int Circle (int x, int y, int radius) {
/* Draw Circle */
printf("Drawing the circle...\n");
/* Return -1 to test contract post assertion */
if (radius == 2)
return -1;
else
return 1;
}

View File

@@ -0,0 +1,19 @@
/* File : example.i */
/* Basic C example for swig contract */
/* Tiger, University of Chicago, 2003 */
%module example
%contract Circle (int x, int y, int radius) {
require:
x >= 0;
y >= 0;
radius > x;
ensure:
Circle >= 0;
}
%inline %{
extern int Circle (int x, int y, int radius);
%}

View File

@@ -0,0 +1,17 @@
import example
# Call the Circle() function correctly
x = 1;
y = 1;
r = 3;
c = example.Circle(x, y, r)
# test post-assertion
x = 1;
y = 1;
r = 2;
c = example.Circle(x, y, r)
print "The return value of Circle(%d, %d, %d) is %d" % (x,y,r,c)

View File

@@ -0,0 +1,20 @@
import example
# Call the Circle() function correctly
x = 1;
y = 1;
r = 3;
c = example.Circle(x, y, r)
print "The return value of Circle(%d, %d, %d) is %d" % (x,y,r,c)
# test pre-assertion
x = 1;
y = -1;
r = 3;
c = example.Circle(x, y, r)
print "The return value of Circle(%d, %d, %d) is %d" % (x,y,r,c)