diff options
| author | Martin Nowack <m.nowack@imperial.ac.uk> | 2020-04-28 18:23:50 +0100 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-06-06 19:03:03 +0100 |
| commit | daa2d4d202929f9f7ba38dd76feabf2fa34816ab (patch) | |
| tree | 77d43893132707ab6f06a9d551e0c52352f363d1 /runtime/FreeStanding/memcpy.c | |
| parent | 597df194218f2de174ead6b8a1abb2555f8bef4b (diff) | |
| download | klee-daa2d4d202929f9f7ba38dd76feabf2fa34816ab.tar.gz | |
[Module] Disable lifting for inline asm resembling memory fences with return values
Inline asm used for memory barriers might use their operands and propagate them as return value. This is currently not supported. Tighten check for this condition and do not to lift those inline asm instructions. Fixes #1252
Diffstat (limited to 'runtime/FreeStanding/memcpy.c')
0 files changed, 0 insertions, 0 deletions