Skip to content

Commit

Permalink
Rebase on latest master
Browse files Browse the repository at this point in the history
The new array test needed fixing.
  • Loading branch information
sebastianpoeplau committed Aug 31, 2020
1 parent 0232b5d commit b92ccb4
Showing 1 changed file with 5 additions and 5 deletions.
10 changes: 5 additions & 5 deletions test/arrays.c
Original file line number Diff line number Diff line change
Expand Up @@ -21,36 +21,36 @@
int main(int argc, char* argv[]) {
uint8_t input[4];
if (read(STDIN_FILENO, input, sizeof(input)) != sizeof(input)) {
printf("Failed to read the input\n");
fprintf(stderr, "Failed to read the input\n");
return -1;
}

uint8_t offset;
if (read(STDIN_FILENO, &offset, sizeof(offset)) != sizeof(offset)) {
printf("Failed to read the offset\n");
fprintf(stderr, "Failed to read the offset\n");
return -1;
}

// This is just to make the base pointer symbolic.
uint8_t *p = input + offset;

printf("%s\n", (p[0] == 1) ? "yes" : "no");
fprintf(stderr, "%s\n", (p[0] == 1) ? "yes" : "no");
// SIMPLE: Trying to solve
// QSYM-COUNT-2: SMT
// ANY: yes

// If our GetElementPointer computations are incorrect, this will create
// path constraints that conflict with those generated by the previous array
// access.
printf("%s\n", (p[2] == 3) ? "yes" : "no");
fprintf(stderr, "%s\n", (p[2] == 3) ? "yes" : "no");
// SIMPLE: Trying to solve
// QSYM-COUNT-2: SMT
// ANY: yes

// Use the pointer in a condition to see if contradicting constraints have
// been created. The QSYM backend will log an error in this case (see
// below), the simple backend just aborts.
printf("%s\n", (p == input) ? "yes" : "no");
fprintf(stderr, "%s\n", (p == input) ? "yes" : "no");
// SIMPLE: Trying to solve
// QSYM-NOT: Incorrect constraints are inserted
// QSYM-COUNT-2: SMT
Expand Down

0 comments on commit b92ccb4

Please sign in to comment.