Age | Commit message (Collapse) | Author | |
---|---|---|---|
2021-05-04 | tests: adjust to new summary output | Frank Busse | |
2019-03-18 | Disable optimisation for functions that contain KLEE calls | Martin Nowack | |
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`. | |||
2019-03-18 | make test/Feature/srem.c more explicit | Julian Büning | |
2019-03-07 | Renamed %llvmgcc and %llvmgxx to %clang and %clangxx respectively. | Cristian Cadar | |
2018-10-26 | llvm5: test, add -disable-O0-optnone to -O0 | Jiri Slaby | |
Otherwise optimizations done in klee won't have any effect. Signed-off-by: Jiri Slaby <jirislaby@gmail.com> | |||
2015-09-22 | [STPBuilder] Generate SRrem expressions correctly | Martin Nowack | |
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. |