Depending in the optimization level, assertion violations in inline functions may not be detected

[lzaoral]

Code:

• main.c

#include "inline.h"

int main(void)
{
    foo();
}

• inline.h

inline void foo(void) {}

• inline.c

#include <assert.h>

void foo(void)
{
    assert(0);
}

For clang the following holds: -O0 or -O1 are used, the definition in inline.c will be used, when -O2 or higher are used, the definition in inline.h MAY be used instead only of the compiler is able to inline the given call.

Either way, Symbiotic should always explore both definitions in the example above as C99 §6.7.4.5 says that

...
Making a function an inline function suggests that calls to the function be as fast as possible. The extent to which such suggestions are effective is implementation-defined. For example, an implementation might never perform inline substitution, or might only perform inline substitutions to calls in the scope of an inline declaration.

[mchalupa]

Hmm, isn't it different in C89? (I do not know). What I am saying is that to adhere to such a behavior, we should also have a switch that says what standard of C we are assuming (if any).

And to the technical side: any idea how to handle this? We want to plug both definitions into the program and non-deterministically call one of them, but we do not want to do this transformation on C level.
Another (a bit 'workaround') option would be to also specify which definition should be used. That is, have a way of exploring both possibilities but let the user choose.

EDIT: added the third option.

[lzaoral]

Yeah, it's different in C89/90 as the inline keyword was introduced in C99 (mentioned in Foreword.5). Before that, it was available only as a GNU extension with somewhat swapped semantics. See wiki for more details.

EDIT: typo

[mchalupa]

By the way, related to this is also the indeterminism in evaluating operands with side effects, e.g., if the C code calls foo() + bar() than it is unspecified which of the functions is called first. If the functions have side-effects then we can get different program states based on which of the functions would be called first and therefore we would like Symbiotic to explore both options. This possibility is also lost during the compilation to LLVM.