search

goblint / bench

The benchmark suite
4 stars 5 forks source link

Initial setup for cve-bench #20

Closed vesalvojdani closed 2 years ago

vesalvojdani commented 2 years ago

I'm creating this pull request to get some input on how we should set up these GobPie demonstrators (#22).

  1. How to set up the harnessing. I was thinking that maybe we should go the ldv approach, but that's a fairly ugly demo to open the preprocessed file in the GUI. The alternative is to rely on Goblint's own amazingly sound auto-harness features (i.e., beauties like otherfuns), which we might survive for now...
  2. The problem if we do not merge the files is that we need different versions of include files. I guess one could have the needed include files for each project here and set the kernel directory flag.

The current CVE included here should work with our current include files. My question is what we should do to make these work more-or-less out of the box with GobPie.

vesalvojdani commented 2 years ago

Also, narrowing these down to CVE may be a bad idea. If there is a good example from ldv-commit-races, we could use that here too, but I don't think we want them preprocessed for a demonstrator.

sim642 commented 2 years ago

Already preprocessed files with all the #line macros won't work with GobPie anyway, because through CIL our locations for warnings will refer to those (absolute) pre-merging paths. But because they don't exist, the warnings don't show up anywhere. So we'd have to strip the #lines anyway.