Merge pull request #6253 from TGWDB/Output_c_rol_ror

Add conversion for rol and ror operators to c output

Author: TGWDB

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)

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 \

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>"
+)

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

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

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.