search

izlatkin / HornLauncher

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

Fixing LARGE_INT: #23

Closed izlatkin closed 3 years ago

izlatkin commented 3 years ago

Fixing LARGE_INT:

int main() { int scheme; int urilen,tokenlen; int cp,c; urilen = nondet_6530(); tokenlen = nondet_9760(); scheme = nondet_6957(); int LARGE_INT = nondet_35636(); if (!(urilen <= LARGE_INT && urilen >= -LARGE_INT)) return 0; if (!(tokenlen <= LARGE_INT && tokenlen >= -LARGE_INT)) return 0; if (!(scheme <= LARGE_INT && scheme >= -LARGE_INT)) return 0;

izlatkin commented 3 years ago

looks like https://github.com/izlatkin/sv-benchmarks/blob/master/c/loop-invgen/assert.h contains all necessary dependencies https://github.com/izlatkin/sv-benchmarks/commit/888342d3238e8af0937304de423be9369a5c9d6e