search

izlatkin / HornLauncher

scripts and reports for executions seahorn and test generation
0 stars 0 forks source link

instrumentation error for n.c24 #24

Closed izlatkin closed 2 years ago

izlatkin commented 3 years ago

Following methods ignores during the replacement/instrumentation process.

int bar(char *x)
{
  return __VERIFIER_nondet_int();
}

int foo(int * x){
   *x = __VERIFIER_nondet_int();
   return *x;
}

https://github.com/sosy-lab/sv-benchmarks/blob/master/c/loops/n.c24.c

image

izlatkin commented 2 years ago

fixed.