---

yaml
---
r: 83310
b: refs/heads/variant-submodule
c: 9a26a63
h: refs/heads/develop

Author: TGWDB

[refs]

@@ -131,7 +131,7 @@ refs/heads/unwind-counters4: 57aedaa3fe3995b30ba69c96c9f04df79f8e8ff8
 refs/heads/value-set-make-member: 0f8404cb460f55d43bc253e12f1bde7fd7ed4d37
 refs/heads/value-set-member-fix: 2c87bd4c0d9e1954e2de6af0118fa1ef296ae548
 "refs/heads/value_set_fi_hacks": 3d243543adb4ff450596e7994e2fa1d590ec1e1b
-refs/heads/variant-submodule: c750f5e9eec033096f42e04518a9f6591a9cc105
+refs/heads/variant-submodule: 9a26a63c03d4adcd7dff59e8435f116b10285fa4
 refs/heads/windows-console-streambuf: b984ac7bd772da956bb5656f0072d85b3fdbbf34
 refs/tags/cbmc-5.10: 097cf712f57d59cff9c53a9fb7b9b81be1245f93
 refs/tags/cbmc-5.11: 90d0de91b0918c9e5d5ed250cae62241ae38392a

branches/variant-submodule/regression/CMakeLists.txt

@@ -36,6 +36,7 @@ add_subdirectory(cbmc-incr-smt2)
 add_subdirectory(cbmc-incr)
 add_subdirectory(cbmc-with-incr)
 add_subdirectory(array-refinement-with-incr)
+add_subdirectory(goto-instrument-json)
 add_subdirectory(goto-instrument-wmm-core)
 add_subdirectory(goto-instrument-typedef)
 add_subdirectory(smt2_solver)

branches/variant-submodule/regression/Makefile

@@ -14,6 +14,7 @@ DIRS = cbmc \
        cbmc-incr \
        cbmc-with-incr \
        array-refinement-with-incr \
+       goto-instrument-json \
        goto-instrument-wmm-core \
        goto-instrument-typedef \
        smt2_solver \

branches/variant-submodule/regression/goto-instrument-json/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+  "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:symtab2gb> $<TARGET_FILE:goto-instrument>"
+)

branches/variant-submodule/regression/goto-instrument-json/Makefile

@@ -0,0 +1,20 @@
+default: tests.log
+
+include ../../src/config.inc
+include ../../src/common
+
+test:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/symtab2gb/symtab2gb ../../../src/goto-instrument/goto-instrument'
+
+tests.log:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/symtab2gb/symtab2gb ../../../src/goto-instrument/goto-instrument'
+
+clean:
+	@for dir in *; do \
+		$(RM) tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			$(RM) *.out *.gb; \
+			cd ..; \
+		fi \
+	done

branches/variant-submodule/regression/goto-instrument-json/chain.sh

@@ -0,0 +1,13 @@
+#!/bin/bash
+
+set -e
+
+symtab2gb_exe=$1
+goto_instrument_exe=$2
+
+name=${*:$#}
+
+args=${*:3:$#-3}
+
+$symtab2gb_exe "${name}"
+$goto_instrument_exe "${args}" a.out

branches/variant-submodule/regression/goto-instrument-json/rol_signed/test-signed.desc

@@ -0,0 +1,14 @@
+CORE
+test-signed.json
+--dump-c
+^EXIT=0$
+^SIGNAL=0$
+signed char rol8=\(unsigned char\)'8' << 3 % 8 \| \(unsigned char\)'8' >> 8 - 3 % 8;
+--
+irep
+--
+This tests that the rol goto operation is converted into suitable bit
+twiddling operations in C representation. This is also checks that
+signed rotations cast to unsigned to perform the shifts to avoid
+sign bit problems. Also the negative check for "irep" checks that no
+irep is failing conversion.