From f9cb81fa27ca6ae4fef1c22081040071d20e4413 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Mon, 30 Oct 2023 11:59:29 +0000 Subject: Assume C compiler's default standard is `-std=gnu17` 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. --- test/VectorInstructions/insert_element.c | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'test/VectorInstructions/insert_element.c') diff --git a/test/VectorInstructions/insert_element.c b/test/VectorInstructions/insert_element.c index df09819d..35054fd9 100644 --- a/test/VectorInstructions/insert_element.c +++ b/test/VectorInstructions/insert_element.c @@ -5,9 +5,10 @@ // RUN: %klee --output-dir=%t.klee-out --optimize=false %t1.bc > %t.stdout.log 2> %t.stderr.log // RUN: FileCheck -check-prefix=CHECK-STDOUT -input-file=%t.stdout.log %s // RUN: FileCheck -check-prefix=CHECK-STDERR -input-file=%t.stderr.log %s +#include "klee/klee.h" #include -#include #include +#include typedef uint32_t v4ui __attribute__ ((vector_size (16))); int main() { -- cgit 1.4.1