x86: Add an integration test

Author: chameco

intTests/test_llvm_x86_07/test

@@ -0,0 +1,10 @@
+section .bss
+section .text
+global precondtest
+precondtest:
+	mov rax, rdi
+        ret
+global _start
+_start:
+        mov rax, 60
+        syscall

intTests/test_llvm_x86_07/test.S

@@ -0,0 +1,8 @@
+#include <stdint.h>
+#include <stdio.h>
+
+extern uint64_t precondtest(uint64_t x);
+
+void test() {
+	precondtest(1);
+};

intTests/test_llvm_x86_07/test.c

@@ -0,0 +1,14 @@
+enable_experimental;
+
+m <- llvm_load_module "test.bc";
+
+let precondtest_setup = do {
+  x <- crucible_fresh_var "x" (llvm_int 64);
+  crucible_precond {{ x < 10 }};
+  llvm_execute_func [crucible_term x];
+  x' <- crucible_fresh_var "x'" (llvm_int 64);
+  crucible_return (crucible_term x');
+  crucible_postcond {{ x' < 10 }};
+};
+
+llvm_verify_x86 m "./test" "precondtest" [] false precondtest_setup w4;

intTests/test_llvm_x86_07/test.saw

@@ -0,0 +1,7 @@
+#!/bin/sh
+set -e
+
+# yasm -felf64 test.S
+# ld test.o -o test
+clang -c -emit-llvm test.c
+$SAW test.saw