Skip to content

memory-alloca: remove termination benchmarks

Ondra Lengál requested to merge github/fork/ondrik/master into master

This removes termination benchmarks from the memory-alloca directory. The removed programs were obtained by changing a code of the form

int main()
{
  int x;
  // manipulate x
}

to the form

int main()
{
  int* x = alloca(sizeof(int));
  // manipulate *x
}

where the main body of the program tests termination of a loop and is memory-safety uninteresting. All of the removed files are also present in the directory termination-memory-alloca, which is a part of the benchmark set for the Termination category, and are therefore duplicit.

I kept only the two files:

c.03-alloca_true-valid-memsafety.c
c.03-alloca_true-valid-memsafety.i

as a challenging example that contains some very easy memory manipulation and a non-trivial integer loop, such that memory safety of the program does not depend on the termination of the program. This is a challenge for memory-safety analyzers; they can deduce such a fact and skip the termination analysis.

ref: https://groups.google.com/forum/#!topic/sv-comp/tjV3nkCq9sI

Merge request reports