Skip to content

sprintf wrapper #137

Open
Open
@ercoppa

Description

@ercoppa

Consider the following example (inspired by a real-world program):

int main(int argc, char *argv[]) {
  char c[8];

  ssize_t nbytes = read(STDIN_FILENO, c, 1);
  if (nbytes != 1)
    return 1;

  sprintf(c, "0%d", 1);

  if (c[0])
    fprintf(stderr, "Concrete: %s\n", c);
  else
    fprintf(stderr, "Symbolic: %s\n", c);
  return 0;
}

c[0] is not symbolic due to the effects of sprintf. Writing an exhaustive wrapper for sprintf is hard, however, we can at least clear the symbolic memory written by sprintf to avoid (a) solving invalid queries and (b) polluting the path constraints.

One possible fix could be this one. Let me know if this ok or how to improve it.

P.s. I had to make this declaration to make the compiler happy (see the attribute), however, maybe we want to move it somewhere else.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions