about summary refs log tree commit diff homepage
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/CMakeLists.txt4
-rw-r--r--test/Concrete/ConstantExpr.ll13
-rw-r--r--test/Feature/Alias.c9
-rw-r--r--test/Feature/LargeReturnTypes.cpp3
-rw-r--r--test/Feature/LinkLLVMLib.c2
-rw-r--r--test/Feature/LongDouble.c (renamed from test/Feature/LongDouble.cpp)29
-rw-r--r--test/Feature/MemoryLimit.c6
-rw-r--r--test/Feature/Realloc.c4
-rw-r--r--test/Feature/Vararg.c1
-rw-r--r--test/Runtime/POSIX/DirSeek.c4
-rw-r--r--test/Runtime/POSIX/FD_Fail.c2
-rw-r--r--test/lit.cfg116
-rw-r--r--test/regression/2016-11-24-bitcast-weak-alias.c1
-rw-r--r--test/regression/2017-02-21-pathOS-id.c19
-rw-r--r--test/regression/2017-03-23-early-exit-log-stats.c22
15 files changed, 156 insertions, 79 deletions
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index a2a46e2a..2e97f38a 100644
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -68,7 +68,7 @@ endif()
 if (DOWNLOAD_FILECHECK_SOURCE)
   set(FILECHECK_SRC_URL "https://raw.githubusercontent.com/llvm-mirror/llvm/release_${LLVM_VERSION_MAJOR}${LLVM_VERSION_MINOR}/utils/FileCheck/FileCheck.cpp")
   set(FILECHECK_SRC_FILE "${CMAKE_CURRENT_BINARY_DIR}/FileCheck.cpp")
-  if (NOT EXISTS "${FILECHECK_SRC_URL}")
+  if (NOT EXISTS "${FILECHECK_SRC_FILE}")
     message(STATUS "Downloading LLVM FileCheck source")
     file(DOWNLOAD "${FILECHECK_SRC_URL}" "${FILECHECK_SRC_FILE}" SHOW_PROGRESS)
   endif()
@@ -96,7 +96,7 @@ if (DOWNLOAD_NOT_SOURCE)
   target_include_directories("not" PRIVATE ${KLEE_COMPONENT_EXTRA_INCLUDE_DIRS})
   target_compile_options("not" PRIVATE ${KLEE_COMPONENT_CXX_FLAGS})
   target_compile_definitions("not" PRIVATE ${KLEE_COMPONENT_CXX_DEFINES})
-  target_link_libraries("not" PRIVATE ${FILECHECK_NEEDED_LIBS})
+  target_link_libraries("not" PRIVATE ${NOT_NEEDED_LIBS})
 endif()
 
 ###############################################################################
diff --git a/test/Concrete/ConstantExpr.ll b/test/Concrete/ConstantExpr.ll
index 351223e7..d00c59a6 100644
--- a/test/Concrete/ConstantExpr.ll
+++ b/test/Concrete/ConstantExpr.ll
@@ -45,13 +45,14 @@ define void @"test_logical_ops"() {
   call void @print_i32(i32 %t1)
   call void @print_i32(i32 %t2)
   call void @print_i32(i32 %t3)
+
+  ; or the address with 1 to ensure the addresses will differ in 'ne' below
+  %t4 = shl i64 lshr(i64 or(i64 ptrtoint(i32* @gInt to i64), i64 1), i64 8), 8
+  %t5 = shl i64 ashr(i64 or(i64 ptrtoint(i32* @gInt to i64), i64 1), i64 8), 8
+  %t6 = lshr i64 shl(i64 or(i64 ptrtoint(i32* @gInt to i64), i64 1), i64 8), 8
   
-  %t4 = shl i32 lshr(i32 ptrtoint(i32* @gInt to i32), i32 8), 8
-  %t5 = shl i32 ashr(i32 ptrtoint(i32* @gInt to i32), i32 8), 8
-  %t6 = lshr i32 shl(i32 ptrtoint(i32* @gInt to i32), i32 8), 8
-  
-  %t7 = icmp eq i32 %t4, %t5     
-  %t8 = icmp ne i32 %t4, %t6     
+  %t7 = icmp eq i64 %t4, %t5
+  %t8 = icmp ne i64 %t4, %t6
   
   %t9 = zext i1 %t7 to i8
   %t10 = zext i1 %t8 to i8
diff --git a/test/Feature/Alias.c b/test/Feature/Alias.c
index 381bcc2a..09abb3e0 100644
--- a/test/Feature/Alias.c
+++ b/test/Feature/Alias.c
@@ -1,10 +1,9 @@
+// Darwin does not have strong aliases.
+// REQUIRES: not-darwin
 // RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc
 
-// Darwin does not have strong aliases.
-// XFAIL: darwin
-
 #include <assert.h>
 
 // alias for global
@@ -17,10 +16,10 @@ extern int foo() __attribute__((alias("__foo")));
 
 int *c = &a;
 
-int main() { 
+int main() {
   assert(a == 52);
   assert(foo() == 52);
   assert(*c == 52);
-  
+
   return 0;
 }
diff --git a/test/Feature/LargeReturnTypes.cpp b/test/Feature/LargeReturnTypes.cpp
index 937b0758..84119624 100644
--- a/test/Feature/LargeReturnTypes.cpp
+++ b/test/Feature/LargeReturnTypes.cpp
@@ -1,3 +1,4 @@
+// REQUIRES: not-darwin
 // RUN: %llvmgxx -g -fno-exceptions -emit-llvm -O0 -c -o %t.bc %s
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --libc=klee --no-output --exit-on-error %t.bc > %t.log
@@ -9,8 +10,6 @@
 // This test currently doesn't work on darwin because this isn't how things work
 // in libc++. This test should be rewritten to not depend on an external
 // dependency.
-//
-// XFAIL: darwin
 
 #include <fstream>
 
diff --git a/test/Feature/LinkLLVMLib.c b/test/Feature/LinkLLVMLib.c
index 95437094..34931409 100644
--- a/test/Feature/LinkLLVMLib.c
+++ b/test/Feature/LinkLLVMLib.c
@@ -3,7 +3,7 @@
 //
 // RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t2.bc -DLINK_LLVM_LIB_TEST_EXEC
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --link-llvm-lib %t1.a --output-dir=%t.klee-out --emit-all-errors %t2.bc 2>&1 | FileCheck %s
+// RUN: %klee --link-llvm-lib %t1.a --output-dir=%t.klee-out --emit-all-errors --warnings-only-to-file=false %t2.bc 2>&1 | FileCheck %s
 
 #ifdef LINK_LLVM_LIB_TEST_EXEC
 extern void printint(int d);
diff --git a/test/Feature/LongDouble.cpp b/test/Feature/LongDouble.c
index 08924293..ad4c1a79 100644
--- a/test/Feature/LongDouble.cpp
+++ b/test/Feature/LongDouble.c
@@ -1,6 +1,7 @@
-// RUN: %llvmgxx -I../../../include -g -fno-exceptions -emit-llvm -O0 -c -o %t.bc %s
+// RUN: %llvmgcc  -g -emit-llvm -O0 -c -o %t.bc %s
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --libc=klee --no-output --exit-on-error %t.bc > %t.log
+// FIXME: When we remove LLVM 2.9 support just use FileCheck and remove these `grep`s.
 // RUN: grep -q powl\(-11\\.0,0\)=1\\.0\\+ %t.log
 // RUN: grep -q powl\(-11\\.0,1\)=-11\\.0\\+ %t.log
 // RUN: grep -q powl\(-11\\.0,2\)=121\\.0\\+ %t.log
@@ -8,28 +9,26 @@
 // RUN: grep -q 1/-1=-1\\.0\\+ %t.log
 // RUN: grep -q 1/-2=-0\\.50\\+ %t.log
 
-#include <cstdio>
-#include <cstdlib>
-#include <cmath>
-#include <cassert>
-
 #include "klee/klee.h"
+#include <assert.h>
+#include <math.h>
+#include <stdio.h>
+#include <stdlib.h>
 
 unsigned klee_urange(unsigned start, unsigned end) {
   unsigned x;
   klee_make_symbolic(&x, sizeof x, "x");
-  if (x-start>=end-start) klee_silent_exit(0);
+  if (x - start >= end - start)
+    klee_silent_exit(0);
   return x;
 }
 
-int main(int argc, char ** argv)
-{
-
-  int a = klee_urange(0,3);
+int main(int argc, char **argv) {
+  int a = klee_urange(0, 3);
   int b;
 
   // fork states
-  switch(a) {
+  switch (a) {
   case 0:
     b = -0;
     break;
@@ -40,7 +39,7 @@ int main(int argc, char ** argv)
     b = -2;
     break;
   default:
-    assert(false && "Impossible switch target");
+    assert(0 && "Impossible switch target");
   }
 
   // test 80-bit external dispatch
@@ -52,7 +51,7 @@ int main(int argc, char ** argv)
   printf("powl(-11.0,%d)=%Lf\n", a, d);
 
   // test 80-bit fdiv
-  long double e = (long double) 1 / (long double) b;
+  long double e = (long double)1 / (long double)b;
   // CHECK-DAG: 1/0=inf
   // CHECK-DAG: 1/1-1=-1.0
   // CHECK-DAG: 1/-2=-0.50
@@ -60,5 +59,3 @@ int main(int argc, char ** argv)
 
   return 0;
 }
-
-
diff --git a/test/Feature/MemoryLimit.c b/test/Feature/MemoryLimit.c
index fb9f2c86..ce4bc00f 100644
--- a/test/Feature/MemoryLimit.c
+++ b/test/Feature/MemoryLimit.c
@@ -4,17 +4,17 @@
 
 // RUN: %llvmgcc -emit-llvm -DLITTLE_ALLOC -g -c %s -o %t.little.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --max-memory=20 %t.little.bc > %t.little.log 2> %t.little.err
+// RUN: %klee --output-dir=%t.klee-out --max-memory=20 %t.little.bc > %t.little.log
 // RUN: not grep -q "MALLOC FAILED" %t.little.log
 // RUN: not grep -q "DONE" %t.little.log
-// RUN: grep "WARNING: killing 1 states (over memory cap)" %t.little.err
+// RUN: grep "WARNING: killing 1 states (over memory cap)" %t.klee-out/warnings.txt
 
 // RUN: %llvmgcc -emit-llvm -g -c %s -o %t.big.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --max-memory=20 %t.big.bc > %t.big.log 2> %t.big.err
 // RUN: not grep -q "MALLOC FAILED" %t.big.log
 // RUN: not grep -q "DONE" %t.big.log
-// RUN: grep "WARNING: killing 1 states (over memory cap)" %t.big.err
+// RUN: grep "WARNING: killing 1 states (over memory cap)" %t.klee-out/warnings.txt
 
 #include <stdlib.h>
 #include <stdio.h>
diff --git a/test/Feature/Realloc.c b/test/Feature/Realloc.c
index 76016fb7..d0c85b21 100644
--- a/test/Feature/Realloc.c
+++ b/test/Feature/Realloc.c
@@ -1,6 +1,6 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc 2>&1 | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --exit-on-error --warnings-only-to-file=false %t1.bc 2>&1 | FileCheck %s
 
 #include <assert.h>
 #include <stdlib.h>
@@ -13,7 +13,7 @@ int main() {
 
   // CHECK: KLEE: WARNING ONCE: Large alloc
   int *p2 = realloc(p, 1<<30);
-  assert(p2[1] == 52);
+  assert(!p2 || p2[1] == 52);
 
   return 0;
 }
diff --git a/test/Feature/Vararg.c b/test/Feature/Vararg.c
index 82fbe4f1..a78b784e 100644
--- a/test/Feature/Vararg.c
+++ b/test/Feature/Vararg.c
@@ -1,3 +1,4 @@
+// REQUIRES: not-darwin
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out %t1.bc > %t2.out
diff --git a/test/Runtime/POSIX/DirSeek.c b/test/Runtime/POSIX/DirSeek.c
index e017b98d..3908b4e2 100644
--- a/test/Runtime/POSIX/DirSeek.c
+++ b/test/Runtime/POSIX/DirSeek.c
@@ -23,15 +23,13 @@
 #include <string.h>
 
 int main(int argc, char **argv) {
-  struct stat s;
-
   char first[256], second[256];
   DIR *d = opendir(".");
   struct dirent *de = readdir(d);
   assert(de);
   strcpy(first, de->d_name);
   off_t pos = telldir(d);
-  printf("pos: %d\n", telldir(d));
+  printf("pos: %ld\n", telldir(d));
   de = readdir(d);
   assert(de);
   strcpy(second, de->d_name);
diff --git a/test/Runtime/POSIX/FD_Fail.c b/test/Runtime/POSIX/FD_Fail.c
index 186ada51..2ee1a1a2 100644
--- a/test/Runtime/POSIX/FD_Fail.c
+++ b/test/Runtime/POSIX/FD_Fail.c
@@ -11,7 +11,7 @@
 
 int main(int argc, char** argv) {
   char buf[1024];  
-  FILE* f = fopen("/etc/fstab", "r");
+  FILE* f = fopen("/etc/mtab", "r");
   assert(f);
     
   int r = fread(buf, 1, 100, f);
diff --git a/test/lit.cfg b/test/lit.cfg
index 31552882..9c557a78 100644
--- a/test/lit.cfg
+++ b/test/lit.cfg
@@ -1,4 +1,6 @@
 # -*- Python -*-
+# vim: set filetype=python:
+# vim: ts=2:sts=2:sw=2:et:tw=80:
 
 # Configuration file for the 'lit' test runner.
 
@@ -8,10 +10,10 @@ import re
 import platform
 
 try:
-   import lit.util
-   import lit.formats
+  import lit.util
+  import lit.formats
 except ImportError:
-   pass
+  pass
 
 # name: The name of this test suite.
 config.name = 'KLEE'
@@ -31,27 +33,33 @@ klee_obj_root = getattr(config, 'klee_obj_root', None)
 klee_src_root = getattr(config, 'klee_src_root', None)
 
 if klee_obj_root is not None:
-    config.test_exec_root = os.path.join(klee_obj_root, 'test')
+  config.test_exec_root = os.path.join(klee_obj_root, 'test')
 
 # Tweak the PATH to include the tool dir.
 if klee_obj_root is not None:
-    klee_tools_dir = getattr(config, 'klee_tools_dir', None)
-    if not klee_tools_dir:
-        lit.fatal('No KLEE tools dir set!')
+  klee_tools_dir = getattr(config, 'klee_tools_dir', None)
+  if not klee_tools_dir:
+    lit.fatal('No KLEE tools dir set!')
 
-    # Check LLVM tool directory
-    llvm_tools_dir = getattr(config, 'llvm_tools_dir', None)
-    if not llvm_tools_dir:
-        lit.fatal('No LLVM tool directory set!')
+  # Check LLVM tool directory
+  llvm_tools_dir = getattr(config, 'llvm_tools_dir', None)
+  if not llvm_tools_dir:
+    lit.fatal('No LLVM tool directory set!')
 
-    path = os.path.pathsep.join((llvm_tools_dir, klee_tools_dir, config.environment['PATH'] ))
-    config.environment['PATH'] = path
+  path = os.path.pathsep.join(
+    (
+      llvm_tools_dir,
+      klee_tools_dir,
+      config.environment['PATH']
+    )
+  )
+  config.environment['PATH'] = path
 
 
 # Propogate some environment variable to test environment.
 def addEnv(name):
-    if name in os.environ:
-        config.environment[name] = os.environ[name]
+  if name in os.environ:
+    config.environment[name] = os.environ[name]
 
 addEnv('HOME')
 addEnv('PWD')
@@ -72,27 +80,37 @@ addEnv('CPLUS_INCLUDE_PATH')
 
 # Check that the object root is known.
 if config.test_exec_root is None:
-    lit.fatal('test execution root not set!')
+  lit.fatal('test execution root not set!')
 
 
 # Add substitutions from lit.site.cfg
 subs = [ 'llvmgcc', 'llvmgxx', 'cc', 'cxx']
 for name in subs:
-    value = getattr(config, name, None)
-    if value == None:
-        lit.fatal('{0} is not set'.format(name))
-    config.substitutions.append( ('%' + name, value))
+  value = getattr(config, name, None)
+  if value == None:
+    lit.fatal('{0} is not set'.format(name))
+  config.substitutions.append( ('%' + name, value))
 
 # Add a substitution for lli.
-config.substitutions.append( ('%lli', os.path.join(llvm_tools_dir, 'lli')) )
+config.substitutions.append(
+  ('%lli', os.path.join(llvm_tools_dir, 'lli'))
+)
 # Add a substitution for llvm-as
-config.substitutions.append( ('%llvmas', os.path.join(llvm_tools_dir, 'llvm-as')) )
+config.substitutions.append(
+  ('%llvmas', os.path.join(llvm_tools_dir, 'llvm-as'))
+)
 # Add a substitution for llvm-ar
-config.substitutions.append( ('%llvmar', os.path.join(llvm_tools_dir, 'llvm-ar')) )
+config.substitutions.append(
+  ('%llvmar', os.path.join(llvm_tools_dir, 'llvm-ar'))
+)
 
 # Add a substition for libkleeruntest
-config.substitutions.append( ('%libkleeruntestdir', os.path.dirname(config.libkleeruntest)) )
-config.substitutions.append( ('%libkleeruntest', config.libkleeruntest) )
+config.substitutions.append(
+  ('%libkleeruntestdir', os.path.dirname(config.libkleeruntest))
+)
+config.substitutions.append(
+  ('%libkleeruntest', config.libkleeruntest)
+)
 
 # Get KLEE and Kleaver specific parameters passed on llvm-lit cmd line
 # e.g. llvm-lit --param klee_opts=--help
@@ -106,9 +124,13 @@ else:
   kleaver_extra_params = lit.params.get('kleaver_opts',"")
 
 if len(klee_extra_params) != 0:
-    print("Passing extra KLEE command line args: {0}".format(klee_extra_params))
+  print("Passing extra KLEE command line args: {0}".format(
+    klee_extra_params)
+  )
 if len(kleaver_extra_params) != 0:
-    print("Passing extra Kleaver command line args: {0}".format(kleaver_extra_params))
+  print("Passing extra Kleaver command line args: {0}".format(
+    kleaver_extra_params)
+  )
 
 # Set absolute paths and extra cmdline args for KLEE's tools
 subs = [ ('%kleaver', 'kleaver', kleaver_extra_params),
@@ -116,27 +138,37 @@ subs = [ ('%kleaver', 'kleaver', kleaver_extra_params),
   ('%ktest-tool', 'ktest-tool', '')
 ]
 for s,basename,extra_args in subs:
-    config.substitutions.append( ( s,
-                                   "{0} {1}".format( os.path.join(klee_tools_dir, basename), extra_args ).strip()
-                                 )
-                               )
-
-config.substitutions.append( ('%gentmp', os.path.join(klee_src_root, 'scripts/genTempFiles.sh')) )
+  config.substitutions.append(
+    ( s,
+      "{0} {1}".format(
+        os.path.join(klee_tools_dir, basename),
+        extra_args
+      ).strip()
+    )
+  )
+
+config.substitutions.append(
+  ('%gentmp', os.path.join(klee_src_root, 'scripts/genTempFiles.sh'))
+)
 
 # LLVM < 3.0 doesn't Support %T directive
 if int(config.llvm_version_major) == 2:
-    # This is a hack
-    config.substitutions.append(('%T','Output'))
+  # This is a hack
+  config.substitutions.append(('%T','Output'))
 
 # Add feature for the LLVM version in use, so it can be tested in REQUIRES and
 # XFAIL checks. We also add "not-XXX" variants, for the same reason.
-known_llvm_versions = set(["2.9", "3.4", "3.5"])
+known_llvm_versions = set(["2.9", "3.4", "3.5", "3.6"])
 current_llvm_version = "%s.%s" % (config.llvm_version_major,
                                   config.llvm_version_minor)
 config.available_features.add("llvm-" + current_llvm_version)
 for version in known_llvm_versions:
-   if version != current_llvm_version:
-      config.available_features.add("not-llvm-" + version)
+  if version != current_llvm_version:
+    config.available_features.add("not-llvm-" + version)
+  if current_llvm_version >= version:
+    config.available_features.add("geq-llvm-" + version)
+  else:
+    config.available_features.add("lt-llvm-" + version)
 
 # Solver features
 if config.enable_stp:
@@ -151,3 +183,11 @@ else:
 # POSIX runtime feature
 if config.enable_posix_runtime:
   config.available_features.add('posix-runtime')
+
+# Target operating system features
+supported_targets = ['linux', 'darwin']
+for target in supported_targets:
+  if config.target_triple.find(target) != -1:
+    config.available_features.add(target)
+  else:
+    config.available_features.add('not-{}'.format(target))
diff --git a/test/regression/2016-11-24-bitcast-weak-alias.c b/test/regression/2016-11-24-bitcast-weak-alias.c
index f115731b..3e4ebe64 100644
--- a/test/regression/2016-11-24-bitcast-weak-alias.c
+++ b/test/regression/2016-11-24-bitcast-weak-alias.c
@@ -1,3 +1,4 @@
+// REQUIRES: not-darwin
 // RUN: %llvmgcc %s -Wall -emit-llvm -g -O0 -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: klee --output-dir=%t.klee-out -exit-on-error -search=nurs:covnew %t.bc DUMMY_ARG >%t1.log 2>&1
diff --git a/test/regression/2017-02-21-pathOS-id.c b/test/regression/2017-02-21-pathOS-id.c
new file mode 100644
index 00000000..d3bffbe0
--- /dev/null
+++ b/test/regression/2017-02-21-pathOS-id.c
@@ -0,0 +1,19 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out -write-paths %t.bc 2> %t.log
+// RUN: cat %t.klee-out/test000001.path | wc -l | grep -q 1
+// RUN: cat %t.klee-out/test000002.path | wc -l | grep -q 1
+// RUN: cat %t.klee-out/test000003.path | wc -l | grep -q 1
+// RUN: cat %t.klee-out/test000004.path | wc -l | grep -q 1
+int main(){
+	int a, b;
+	klee_make_symbolic (&a, sizeof(int), "a");
+	klee_make_symbolic (&b, sizeof(int), "b");
+	klee_assume(a<2);
+	klee_assume(a>=0);
+	malloc(a);
+	if(b){
+		b++;//do something
+	}
+	return b;
+}
diff --git a/test/regression/2017-03-23-early-exit-log-stats.c b/test/regression/2017-03-23-early-exit-log-stats.c
new file mode 100644
index 00000000..96d3c30f
--- /dev/null
+++ b/test/regression/2017-03-23-early-exit-log-stats.c
@@ -0,0 +1,22 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// Delay writing instructions so that we ensure on exit that flush happens
+// RUN: not %klee --output-dir=%t.klee-out -exit-on-error -stats-write-interval=0 -stats-write-after-instructions=999999 %t.bc 2> %t.log
+// RUN: FileCheck -check-prefix=CHECK-KLEE -input-file=%t.log %s
+// RUN: FileCheck -check-prefix=CHECK-STATS -input-file=%t.klee-out/run.stats %s
+#include "klee/klee.h"
+#include <stdlib.h>
+int main(){
+  int a;
+  klee_make_symbolic (&a, sizeof(int), "a");
+  if (a) {
+    // CHECK-KLEE: EXITING ON ERROR
+    // CHECK-KLEE-NEXT: Error: abort failure
+    abort();
+  }
+  return 0;
+}
+// First check we find a line with the expected format
+// CHECK-STATS:{{^\('Instructions'}}
+// Now check that we eventually get a line where a non zero amount of instructions were executed
+// CHECK-STATS:{{^\([ ]*([1-9]|([1-9]+)[0-9])}}
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-05-04 00:06:05 +0000