[HornLaucher] instrumentation doesn't work for ldv-linux-3.4-simple

izlatkin / HornLauncher

scripts and reports for executions seahorn and test generation

0 stars 0 forks source link

[HornLaucher] instrumentation doesn't work for ldv-linux-3.4-simple #29

Open izlatkin opened 3 years ago

izlatkin commented 3 years ago

https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ldv-linux-3.4-simple/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--acpi--apei--einj.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c

izlatkin commented 3 years ago

https://github.com/izlatkin/HornLauncher/commit/ae1da5782aa8cb585bbd15d43cd3ec58e5f0207c

izlatkin commented 3 years ago

currently majority (all) linux cfiles do NOT compile because of error: typedef redefinition with different types ('__kernel_dev_t' (aka 'unsigned int') vs '__dev_t' (aka 'unsigned long long')) and similar error.

https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ldv-linux-3.4-simple/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--acpi--apei--einj.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c#L37

full log: log.txt