search

izlatkin / HornLauncher

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

float case: ___VERIFIER_nondet_float #25

Closed izlatkin closed 2 years ago

izlatkin commented 3 years ago

Are we going to support _VERIFIER_nondetfloat() Now VERIFIER_nondet_float does not replace in the source code and, as a result, doesn't compile

https://github.com/sosy-lab/sv-benchmarks/blob/master/c/loop-floats-scientific-comp/loop3.c from https://github.com/sosy-lab/sv-benchmarks/blob/master/c/loop-floats-scientific-comp/

izlatkin commented 3 years ago

testgen.h should be generated taking into account 'float' `extern int nondet(void); float nondet_4926(){ return 4926 + nondet(); } int nondet_3443(){ return 3443 + nondet(); }

`

izlatkin commented 2 years ago

not supported