From ee88b2faa616ab6911ad94126a788eb663577d86 Mon Sep 17 00:00:00 2001 From: Morgan Jones Date: Sun, 17 Oct 2021 23:29:44 -0700 Subject: [PATCH] Rename student examples --- drawSquare.c | 320 ++++++++++++++++++++++++++++----------------------- 1 file changed, 176 insertions(+), 144 deletions(-) diff --git a/drawSquare.c b/drawSquare.c index a78f0a9..f9c1fed 100644 --- a/drawSquare.c +++ b/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; }