Michael Tautschnig

I don't think we should actually run anything (this is a security risk), but we can certainly compile while linking in some dummy implementation of SVCOMP-specific functions. This is one...

> Which version of the C standard you are referring to? That's what C11, page 363 says. > It has nothing to do with reachability of __VERIFIER_error() Yes, and "true-unreach-call"...

Brilliant, the correctness of that benchmark depends on a pointer-manipulating undefined function apparently not covered by any standard or rules.

> For several years I'm trying to attract attention to this problem, but the community likes to discuss examples one-by-one without building a common solution. Apart from removing all the...

@dbeyer According to `git log --follow` those have been submitted by Sagar Chaki. Would you be able to chase this up?

@Guoanshisb With @AndrianovPavel's further comment, are all issues covered by either a pull request or that final comment? If so, this issue should be closed.

@PhilippWendler What is the procedure here? I would be happy to contribute the information for the missing float-* (BSD license), but I don't know how to take action.

ce25410 of #239 adds license files for floats-cbmc-regression, floats-cdfpl, pthread-wmm (and busybox, but that wasn't essential).

Those license fixes have now been moved into #243.

@mikhailramalho That benchmark appears to have been submitted by Omar; is there any original source to it? Indeed the code: ``` if (q->head == 20) { __CS_cs(); if (__CS_ret !=...