Rename student examples
This commit is contained in:
320
drawSquare.c
320
drawSquare.c
@@ -12,7 +12,7 @@
|
||||
#endif
|
||||
|
||||
typedef struct line {
|
||||
int x0, y0, x1, y1;
|
||||
int x0, y0, x1, y1;
|
||||
} line_t;
|
||||
|
||||
static line_t referenceLines[4];
|
||||
@@ -23,195 +23,227 @@ static int actualIdx = 0;
|
||||
|
||||
/* drawReferenceLine implementation. */
|
||||
void drawReferenceLine(int x0, int y0, int x1, int y1) {
|
||||
if (referenceIdx < sizeof(referenceLines) / sizeof(line_t)) {
|
||||
referenceLines[referenceIdx++] = (line_t) {x0, y0, x1, y1};
|
||||
} else {
|
||||
exit(1);
|
||||
}
|
||||
if (referenceIdx < sizeof(referenceLines) / sizeof(line_t)) {
|
||||
referenceLines[referenceIdx++] = (line_t) {.x0 = x0, .y0 = y0, .x1 = x1, .y1 = y1};
|
||||
} else {
|
||||
exit(1);
|
||||
}
|
||||
}
|
||||
|
||||
/* drawLine implementation. */
|
||||
void drawLine(int x0, int y0, int x1, int y1) {
|
||||
if (actualIdx < sizeof(actualLines) / sizeof(line_t)) {
|
||||
actualLines[actualIdx++] = (line_t) {x0, y0, x1, y1};
|
||||
} else {
|
||||
exit(1);
|
||||
}
|
||||
if (actualIdx < sizeof(actualLines) / sizeof(line_t)) {
|
||||
actualLines[actualIdx++] = (line_t) {.x0 = x0, .y0 = y0, .x1 = x1, .y1 = y1};
|
||||
} else {
|
||||
exit(1);
|
||||
}
|
||||
}
|
||||
|
||||
/* drawSquare implementations follow. */
|
||||
|
||||
void drawSquareWeird(int x, int y, int len)
|
||||
static void drawSquareStudent1(int x, int y, int len) {
|
||||
if (x+len > 10){
|
||||
len = 10-x;
|
||||
}
|
||||
|
||||
{
|
||||
if (y+len > 10){
|
||||
len = 10-y;
|
||||
}
|
||||
|
||||
if(((x+len<10) && (x-len>= 0)) && ((y-len>0) && (y+len<=10)) && len>0)
|
||||
drawLine(x, y, x+len, y);
|
||||
|
||||
{
|
||||
drawLine(x, y, x, y+len);
|
||||
|
||||
drawLine(x, y, x+len, y);
|
||||
drawLine(x+len, y, x+len, y+len);
|
||||
|
||||
drawLine(x+len, y, x+len, y-len);
|
||||
|
||||
drawLine(x+len, y-len, x, y-len);
|
||||
|
||||
drawLine(x, y-len, x, y);
|
||||
|
||||
}
|
||||
|
||||
else
|
||||
|
||||
{
|
||||
|
||||
while(len<=0)
|
||||
|
||||
{
|
||||
|
||||
len++;
|
||||
|
||||
}
|
||||
|
||||
while(((x+len<10) && (x-len>= 0)) && ((y-len>0) && (y+len<=10)) == false)
|
||||
{
|
||||
|
||||
len--;
|
||||
|
||||
}
|
||||
|
||||
drawLine(x, y, x+len, y);
|
||||
|
||||
drawLine(x+len, y, x+len, y-len);
|
||||
|
||||
drawLine(x+len, y-len, x, y-len);
|
||||
|
||||
drawLine(x, y-len, x, y);
|
||||
}
|
||||
drawLine(x, y+len, x+len, y+len);
|
||||
}
|
||||
|
||||
static void drawSquareAlmostCorrect(int x, int y, int len) {
|
||||
if (x+len > 10){
|
||||
len = 10-x;
|
||||
}
|
||||
void drawSquareStudent2(int x, int y, int len)
|
||||
{
|
||||
|
||||
if (y+len > 10){
|
||||
len = 10-y;
|
||||
}
|
||||
if(((x+len<10) && (x-len>= 0)) && ((y-len>0) && (y+len<=10)) && len>0)
|
||||
|
||||
drawLine(x, y, x+len, y);
|
||||
{
|
||||
|
||||
drawLine(x, y, x, y+len);
|
||||
drawLine(x, y, x+len, y);
|
||||
|
||||
drawLine(x+len, y, x+len, y+len);
|
||||
drawLine(x+len, y, x+len, y-len);
|
||||
|
||||
drawLine(x, y+len, x+len, y+len);
|
||||
drawLine(x+len, y-len, x, y-len);
|
||||
|
||||
drawLine(x, y-len, x, y);
|
||||
|
||||
}
|
||||
|
||||
else
|
||||
|
||||
{
|
||||
|
||||
while(len<=0)
|
||||
|
||||
{
|
||||
|
||||
len++;
|
||||
|
||||
}
|
||||
|
||||
while(((x+len<10) && (x-len>= 0)) && ((y-len>0) && (y+len<=10)) == false)
|
||||
{
|
||||
|
||||
len--;
|
||||
|
||||
}
|
||||
|
||||
drawLine(x, y, x+len, y);
|
||||
|
||||
drawLine(x+len, y, x+len, y-len);
|
||||
|
||||
drawLine(x+len, y-len, x, y-len);
|
||||
|
||||
drawLine(x, y-len, x, y);
|
||||
}
|
||||
}
|
||||
|
||||
void drawSquareStudent3(int x, int y, int len)
|
||||
{
|
||||
if (0 <= x && x > 10 && 0 < y && y <= 10 && len > 0){
|
||||
|
||||
drawLine(x, y, x + len, y);
|
||||
|
||||
drawLine(x + len, y, x + len, y - len);
|
||||
drawLine(x + len, y - len, x, y - len);
|
||||
drawLine(x, y - len, x, y);
|
||||
}
|
||||
|
||||
else if (x + len < 0|| y - len >= 10){
|
||||
|
||||
len++;
|
||||
drawLine(x, y, x + len, y);
|
||||
|
||||
drawLine(x + len, y, x + len, y - len);
|
||||
drawLine(x + len, y - len, x, y - len);
|
||||
drawLine(x, y - len, x, y);
|
||||
}
|
||||
|
||||
else {
|
||||
|
||||
len--;
|
||||
|
||||
drawLine(x, y, x + len, y);
|
||||
|
||||
drawLine(x + len, y, x + len, y - len);
|
||||
drawLine(x + len, y - len, x, y - len);
|
||||
drawLine(x, y - len, x, y);
|
||||
}
|
||||
}
|
||||
|
||||
/* Example drawSquare that's just drawReferenceSquare reordered. */
|
||||
static void drawSquareReordered(int x, int y, int len) {
|
||||
if (x+len > 10){
|
||||
len = 10-x;
|
||||
}
|
||||
if (x+len > 10){
|
||||
len = 10-x;
|
||||
}
|
||||
|
||||
if (y-len < 0){
|
||||
len = y;
|
||||
}
|
||||
if (y-len < 0){
|
||||
len = y;
|
||||
}
|
||||
|
||||
drawLine(x, y-len, x, y);
|
||||
drawLine(x+len, y-len, x, y-len);
|
||||
drawLine(x, y, x+len, y);
|
||||
drawLine(x+len, y-len, x+len, y);
|
||||
drawLine(x, y-len, x, y);
|
||||
drawLine(x+len, y-len, x, y-len);
|
||||
drawLine(x, y, x+len, y);
|
||||
drawLine(x+len, y-len, x+len, y);
|
||||
}
|
||||
|
||||
/** Draws the "reference" square. */
|
||||
static void drawReferenceSquare(int x, int y, int len) {
|
||||
if (x+len > 10){
|
||||
len = 10-x;
|
||||
}
|
||||
if (x+len > 10){
|
||||
len = 10-x;
|
||||
}
|
||||
|
||||
if (y-len < 0){
|
||||
len = y;
|
||||
}
|
||||
if (y-len < 0){
|
||||
len = y;
|
||||
}
|
||||
|
||||
drawReferenceLine(x, y, x+len, y);
|
||||
drawReferenceLine(x+len, y, x+len, y-len);
|
||||
drawReferenceLine(x+len, y-len, x, y-len);
|
||||
drawReferenceLine(x, y-len, x, y);
|
||||
drawReferenceLine(x, y, x+len, y);
|
||||
drawReferenceLine(x+len, y, x+len, y-len);
|
||||
drawReferenceLine(x+len, y-len, x, y-len);
|
||||
drawReferenceLine(x, y-len, x, y);
|
||||
}
|
||||
|
||||
/** Compares that the drawn square is equal to the reference square. */
|
||||
static int compareSquares(void) {
|
||||
int ret = 0;
|
||||
int ret = 0;
|
||||
|
||||
const int numLines = sizeof(actualLines) / sizeof(line_t);
|
||||
int confirmed[numLines] = {0};
|
||||
int numConfirmed = 0;
|
||||
for (int actualIdx = 0; actualIdx < numLines; actualIdx++) {
|
||||
line_t *actualLine = &actualLines[actualIdx];
|
||||
bool found = false;
|
||||
for (int referenceIdx = 0; referenceIdx < numLines; referenceIdx++) {
|
||||
line_t *referenceLine = &referenceLines[referenceIdx];
|
||||
bool skipThis = false;
|
||||
for (int idx = 0; idx < numConfirmed; idx++) {
|
||||
if (confirmed[idx] == referenceIdx) {
|
||||
skipThis = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
const int numLines = sizeof(actualLines) / sizeof(line_t);
|
||||
int confirmed[numLines] = {0};
|
||||
int numConfirmed = 0;
|
||||
for (int actualIdx = 0; actualIdx < numLines; actualIdx++) {
|
||||
line_t *actualLine = &actualLines[actualIdx];
|
||||
bool found = false;
|
||||
for (int referenceIdx = 0; referenceIdx < numLines; referenceIdx++) {
|
||||
line_t *referenceLine = &referenceLines[referenceIdx];
|
||||
bool skipThis = false;
|
||||
for (int idx = 0; idx < numConfirmed; idx++) {
|
||||
if (confirmed[idx] == referenceIdx) {
|
||||
skipThis = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
if (!skipThis && (
|
||||
(actualLine->x0 == referenceLine->x0
|
||||
&& actualLine->y0 == referenceLine->y0
|
||||
&& actualLine->x1 == referenceLine->x1
|
||||
&& actualLine->y1 == referenceLine->y1) ||
|
||||
(actualLine->x1 == referenceLine->x0
|
||||
&& actualLine->y1 == referenceLine->y0
|
||||
&& actualLine->x0 == referenceLine->x1
|
||||
&& actualLine->y0 == referenceLine->y1))) {
|
||||
found = true;
|
||||
confirmed[numConfirmed++] = referenceIdx;
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (!found) {
|
||||
ret = 1;
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (!skipThis && (
|
||||
(actualLine->x0 == referenceLine->x0
|
||||
&& actualLine->y0 == referenceLine->y0
|
||||
&& actualLine->x1 == referenceLine->x1
|
||||
&& actualLine->y1 == referenceLine->y1) ||
|
||||
(actualLine->x1 == referenceLine->x0
|
||||
&& actualLine->y1 == referenceLine->y0
|
||||
&& actualLine->x0 == referenceLine->x1
|
||||
&& actualLine->y0 == referenceLine->y1))) {
|
||||
found = true;
|
||||
confirmed[numConfirmed++] = referenceIdx;
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (!found) {
|
||||
ret = 1;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
return ret;
|
||||
return ret;
|
||||
}
|
||||
|
||||
int main() {
|
||||
int x, y, len;
|
||||
klee_make_symbolic(&x, sizeof(x), "x");
|
||||
klee_make_symbolic(&y, sizeof(y), "y");
|
||||
klee_make_symbolic(&len, sizeof(len), "len");
|
||||
klee_assume(x >= 0 && x < 10 && y >= 0 && y < 10 && len > 0 && len <= 10);
|
||||
int x, y, len;
|
||||
klee_make_symbolic(&x, sizeof(x), "x");
|
||||
klee_make_symbolic(&y, sizeof(y), "y");
|
||||
klee_make_symbolic(&len, sizeof(len), "len");
|
||||
klee_assume(x >= 0 && x < 10 && y >= 0 && y < 10 && len > 0 && len <= 10);
|
||||
|
||||
drawReferenceSquare(x, y, len);
|
||||
drawSquare(x, y, len);
|
||||
drawReferenceSquare(x, y, len);
|
||||
drawSquare(x, y, len);
|
||||
|
||||
int ret = compareSquares();
|
||||
int ret = compareSquares();
|
||||
|
||||
if (klee_is_replay()) {
|
||||
printf("Inputs: x=%d, y=%d, len=%d\n", x, y, len);
|
||||
if (klee_is_replay()) {
|
||||
printf("Inputs: x=%d, y=%d, len=%d\n", x, y, len);
|
||||
|
||||
const int numLines = sizeof(referenceLines) / sizeof(line_t);
|
||||
for (int referenceIdx = 0; referenceIdx < numLines; referenceIdx++) {
|
||||
line_t *referenceLine = &referenceLines[referenceIdx];
|
||||
printf("Reference: (%d, %d) -> (%d, %d)\n", referenceLine->x0, referenceLine->y0, referenceLine->x1, referenceLine->y1);
|
||||
}
|
||||
for (int actualIdx = 0; actualIdx < numLines; actualIdx++) {
|
||||
line_t *actualLine = &actualLines[actualIdx];
|
||||
printf("Actual: (%d, %d) -> (%d, %d)\n", actualLine->x0, actualLine->y0, actualLine->x1, actualLine->y1);
|
||||
}
|
||||
const int numLines = sizeof(referenceLines) / sizeof(line_t);
|
||||
for (int referenceIdx = 0; referenceIdx < numLines; referenceIdx++) {
|
||||
line_t *referenceLine = &referenceLines[referenceIdx];
|
||||
printf("Reference: (%d, %d) -> (%d, %d)\n", referenceLine->x0, referenceLine->y0, referenceLine->x1, referenceLine->y1);
|
||||
}
|
||||
for (int actualIdx = 0; actualIdx < numLines; actualIdx++) {
|
||||
line_t *actualLine = &actualLines[actualIdx];
|
||||
printf("Actual: (%d, %d) -> (%d, %d)\n", actualLine->x0, actualLine->y0, actualLine->x1, actualLine->y1);
|
||||
}
|
||||
|
||||
if (ret == 0) {
|
||||
printf("All outputs matched\n");
|
||||
} else {
|
||||
printf("Outputs mismatched\n");
|
||||
}
|
||||
}
|
||||
if (ret == 0) {
|
||||
printf("All outputs matched\n");
|
||||
} else {
|
||||
printf("Outputs mismatched\n");
|
||||
}
|
||||
}
|
||||
|
||||
return 0;
|
||||
return 0;
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user