| Age | Commit message (Collapse) | Author |
|---|
|
Newer compilers use `-std=gnu17` as the default when compiling C code.
Fix all the test cases that violate this behaviour or explicitly request
older standards `-std=c89` where necessary.
|
|
|
|
Compilers are allowed to hoist function calls and do GVE.
This is currently done even without `--optimization` enabled.
This is unfortunate in the context of KLEE function calls that might
depend on specific code position without direct control flow
dependencies. In such cases, function calls can be hoisted.
To circumvent this, disallow to optimise functions that contain such
calls by default. This might reduce optimisation for some functions
containing such function calls but still allows it for all others.
This patch adds an additional pass, that detects all functions starting with a
prefix `klee_` and disable optimisations for functions containing such
calls.
This is enabled by default but can be disabled by
`--klee-call-optimisation=false`.
|
|
|
|
|
|
Otherwise optimizations done in klee won't have any effect.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
The '%' operater in C is not Gauss Modulo
but remainder operations.
Using a negative number as right operand
can result in a negative number.
Fix appropriate SRem building
Note: MetaSMTlib implementation doesn't have that bug.
|
