From 91af7cdc0521a155a050976eaa8856f04a576826 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Tue, 22 Mar 2016 16:39:49 +0100 Subject: Generate forked states for switch instructions deterministically This patch generates the states based on the order of switch-cases. Before, switch-constraints were randomly assigned to forked states. As generated code might be different between LLVM versions, we use the case values, order them, and iterate in that order over the cases. This way we can also support deterministic execution of older LLVM versions. --- test/Feature/DeterministicSwitch.c | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) (limited to 'test') diff --git a/test/Feature/DeterministicSwitch.c b/test/Feature/DeterministicSwitch.c index 0768576c..b6c186ff 100644 --- a/test/Feature/DeterministicSwitch.c +++ b/test/Feature/DeterministicSwitch.c @@ -1,6 +1,3 @@ -// The order cases are generated in LLVM 2.9 is different: tab first then space -// as one can see in assembly.ll, skip this test for older versions -// REQUIRES: not-llvm-2.9 // RUN: %llvmgcc %s -emit-llvm -g -c -o %t.bc // RUN: rm -rf %t.klee-out // RUN: %klee -debug-print-instructions=all:stderr --output-dir=%t.klee-out --allow-external-sym-calls --switch-type=internal --search=dfs %t.bc >%t.switch.log 2>&1 @@ -18,23 +15,23 @@ int main(int argc, char **argv) { klee_make_symbolic(&c, sizeof(c), "index"); switch (c) { - case ' ': - printf("space\n"); - break; case '\t': printf("tab\n"); break; + case ' ': + printf("space\n"); + break; default: printf("default\n"); break; } // CHECK-DFS: default - // CHECK-DFS: tab // CHECK-DFS: space + // CHECK-DFS: tab - // CHECK-BFS: space // CHECK-BFS: tab + // CHECK-BFS: space // CHECK-BFS: default return 0; -- cgit 1.4.1