[ { "test_recipe": { "test_instance_name": "provenance_basic_global_xy.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_global_xy.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_global_xy.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_basic_global_xy.c.kcc-1.0.out tests/de_facto_memory_model/provenance_basic_global_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:55:50.970104", "duration": "4.882232" }, "binary_filename": "tests.bin/provenance_basic_global_xy.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_global_xy.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(nil) q=(nil)\nx=1 y=2 *p=0 *q=2\n", "stderr": "Comparison of unspecified value:\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:180:13\n in main at tests/de_facto_memory_model/provenance_basic_global_xy.c:8:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_basic_global_xy.c:9:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nTrying to write outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_basic_global_xy.c:9:5\n\n Undefined behavior (UB-EIO2):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section MEM35-C http://rvdoc.org/CERT-C/MEM35-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_basic_global_xy.c:10:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nReading outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_basic_global_xy.c:10:5\n\n Undefined behavior (UB-EIO7):\n see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1\n see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see CERT-C section STR32-C http://rvdoc.org/CERT-C/STR32-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:55:55.852509", "duration": "0.464252" }, "source_hashes": "b9933350a5c42d516774d11331341832 tests/de_facto_memory_model/provenance_basic_global_xy.c\n", "sources": "#include \n#include \nint x=1, y=2;\nint main() {\n int *p = &x + 1;\n int *q = &y;\n printf(\"Addresses: p=%p q=%p\\n\",(void*)p,(void*)q);\n if (memcmp(&p, &q, sizeof(p)) == 0) {\n *p = 11; // does this have undefined behaviour?\n printf(\"x=%d y=%d *p=%d *q=%d\\n\",x,y,*p,*q);\n }\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_basic_global_yx.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_global_yx.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_global_yx.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_basic_global_yx.c.kcc-1.0.out tests/de_facto_memory_model/provenance_basic_global_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:55:56.868514", "duration": "4.815242" }, "binary_filename": "tests.bin/provenance_basic_global_yx.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_global_yx.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(nil) q=(nil)\nx=1 y=2 *p=0 *q=2\n", "stderr": "Comparison of unspecified value:\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:180:13\n in main at tests/de_facto_memory_model/provenance_basic_global_yx.c:8:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_basic_global_yx.c:9:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nTrying to write outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_basic_global_yx.c:9:5\n\n Undefined behavior (UB-EIO2):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section MEM35-C http://rvdoc.org/CERT-C/MEM35-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_basic_global_yx.c:10:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nReading outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_basic_global_yx.c:10:5\n\n Undefined behavior (UB-EIO7):\n see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1\n see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see CERT-C section STR32-C http://rvdoc.org/CERT-C/STR32-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:56:01.683852", "duration": "0.507365" }, "source_hashes": "bbcbb8cf25a9be7bd1fc6251e0c4c588 tests/de_facto_memory_model/provenance_basic_global_yx.c\n", "sources": "#include \n#include \nint y=2, x=1;\nint main() {\n int *p = &x + 1;\n int *q = &y;\n printf(\"Addresses: p=%p q=%p\\n\",(void*)p,(void*)q);\n if (memcmp(&p, &q, sizeof(p)) == 0) {\n *p = 11; // does this have undefined behaviour?\n printf(\"x=%d y=%d *p=%d *q=%d\\n\",x,y,*p,*q);\n }\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_basic_auto_xy.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_auto_xy.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_auto_xy.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_basic_auto_xy.c.kcc-1.0.out tests/de_facto_memory_model/provenance_basic_auto_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:56:02.739906", "duration": "4.803724" }, "binary_filename": "tests.bin/provenance_basic_auto_xy.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_auto_xy.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(nil) q=(nil)\nx=1 y=2 *p=0 *q=2\n", "stderr": "Comparison of unspecified value:\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:180:13\n in main at tests/de_facto_memory_model/provenance_basic_auto_xy.c:8:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_basic_auto_xy.c:9:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nTrying to write outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_basic_auto_xy.c:9:5\n\n Undefined behavior (UB-EIO2):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section MEM35-C http://rvdoc.org/CERT-C/MEM35-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_basic_auto_xy.c:10:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nReading outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_basic_auto_xy.c:10:5\n\n Undefined behavior (UB-EIO7):\n see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1\n see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see CERT-C section STR32-C http://rvdoc.org/CERT-C/STR32-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nIndeterminate value used in an expression:\n > in main at tests/de_facto_memory_model/provenance_basic_auto_xy.c:10:5\n\n Undefined behavior (UB-CEE2):\n see C11 section 6.2.4 http://rvdoc.org/C11/6.2.4\n see C11 section 6.7.9 http://rvdoc.org/C11/6.7.9\n see C11 section 6.8 http://rvdoc.org/C11/6.8\n see C11 section J.2:1 item 11 http://rvdoc.org/C11/J.2\n see CERT-C section EXP33-C http://rvdoc.org/CERT-C/EXP33-C\n see MISRA-C section 8.9:1 http://rvdoc.org/MISRA-C/8.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:56:07.543724", "duration": "0.508856" }, "source_hashes": "c06e7c5859f8ce7047707a4f6e18a80e tests/de_facto_memory_model/provenance_basic_auto_xy.c\n", "sources": "#include \n#include \nint main() {\n int x=1, y=2;\n int *p = &x + 1;\n int *q = &y;\n printf(\"Addresses: p=%p q=%p\\n\",(void*)p,(void*)q);\n if (memcmp(&p, &q, sizeof(p)) == 0) {\n *p = 11; // does this have undefined behaviour?\n printf(\"x=%d y=%d *p=%d *q=%d\\n\",x,y,*p,*q);\n }\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_basic_auto_yx.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_auto_yx.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_auto_yx.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_basic_auto_yx.c.kcc-1.0.out tests/de_facto_memory_model/provenance_basic_auto_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:56:08.597511", "duration": "4.840232" }, "binary_filename": "tests.bin/provenance_basic_auto_yx.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_auto_yx.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(nil) q=(nil)\nx=1 y=2 *p=0 *q=2\n", "stderr": "Comparison of unspecified value:\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:180:13\n in main at tests/de_facto_memory_model/provenance_basic_auto_yx.c:8:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_basic_auto_yx.c:9:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nTrying to write outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_basic_auto_yx.c:9:5\n\n Undefined behavior (UB-EIO2):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section MEM35-C http://rvdoc.org/CERT-C/MEM35-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_basic_auto_yx.c:10:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nReading outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_basic_auto_yx.c:10:5\n\n Undefined behavior (UB-EIO7):\n see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1\n see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see CERT-C section STR32-C http://rvdoc.org/CERT-C/STR32-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nIndeterminate value used in an expression:\n > in main at tests/de_facto_memory_model/provenance_basic_auto_yx.c:10:5\n\n Undefined behavior (UB-CEE2):\n see C11 section 6.2.4 http://rvdoc.org/C11/6.2.4\n see C11 section 6.7.9 http://rvdoc.org/C11/6.7.9\n see C11 section 6.8 http://rvdoc.org/C11/6.8\n see C11 section J.2:1 item 11 http://rvdoc.org/C11/J.2\n see CERT-C section EXP33-C http://rvdoc.org/CERT-C/EXP33-C\n see MISRA-C section 8.9:1 http://rvdoc.org/MISRA-C/8.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:56:13.437922", "duration": "0.588295" }, "source_hashes": "df6aa1f607a0437fbc2f5c0113043012 tests/de_facto_memory_model/provenance_basic_auto_yx.c\n", "sources": "#include \n#include \nint main() {\n int y=2, x=1;\n int *p = &x + 1;\n int *q = &y;\n printf(\"Addresses: p=%p q=%p\\n\",(void*)p,(void*)q);\n if (memcmp(&p, &q, sizeof(p)) == 0) {\n *p = 11; // does this have undefined behaviour?\n printf(\"x=%d y=%d *p=%d *q=%d\\n\",x,y,*p,*q);\n }\n}\n" }, { "test_recipe": { "test_instance_name": "cheri_03_ii.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "cheri_03_ii.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "cheri_03_ii.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/cheri_03_ii.c.kcc-1.0.out tests/de_facto_memory_model/cheri_03_ii.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:56:14.569258", "duration": "4.598844" }, "binary_filename": "tests.bin/cheri_03_ii.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/cheri_03_ii.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "x[1]=1 *q=1\n", "stderr": "A pointer (or array subscript) outside the bounds of an object:\n > in main at tests/de_facto_memory_model/cheri_03_ii.c:6:3\n\n Undefined behavior (UB-CEA1):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 item 46 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nFound pointer that refers outside the bounds of an object + 1:\n > in main at tests/de_facto_memory_model/cheri_03_ii.c:6:3\n\n Undefined behavior (UB-CEE3):\n see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1\n see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nFound pointer that refers outside the bounds of an object + 1:\n > in main at tests/de_facto_memory_model/cheri_03_ii.c:7:3\n\n Undefined behavior (UB-CEE3):\n see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1\n see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:56:19.168196", "duration": "0.362435" }, "source_hashes": "2458c50a0a8333a84c15d1d8978a4ee0 tests/de_facto_memory_model/cheri_03_ii.c\n", "sources": "#include \nint main() {\n int x[2];\n int *p = &x[0];\n //is this free of undefined behaviour?\n int *q = p + 11;\n q = q - 10;\n *q = 1;\n printf(\"x[1]=%i *q=%i\\n\",x[1],*q);\n}\n" }, { "test_recipe": { "test_instance_name": "pointer_offset_from_ptr_subtraction_global_xy.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_ptr_subtraction_global_xy.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_ptr_subtraction_global_xy.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/pointer_offset_from_ptr_subtraction_global_xy.c.kcc-1.0.out tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_global_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:56:20.077744", "duration": "4.798737" }, "binary_filename": "tests.bin/pointer_offset_from_ptr_subtraction_global_xy.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_ptr_subtraction_global_xy.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "Computing pointer difference between two different objects:\n > in main at tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_global_xy.c:8:3\n\n Undefined behavior (UB-CEA5):\n see C11 section 6.5.6:9 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 item 48 http://rvdoc.org/C11/J.2\n see CERT-C section ARR36-C http://rvdoc.org/CERT-C/ARR36-C\n see MISRA-C section 8.18:2 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nA pointer (or array subscript) outside the bounds of an object:\n > in main at tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_global_xy.c:9:3\n\n Undefined behavior (UB-CEA1):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 item 46 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nFound pointer that refers outside the bounds of an object + 1:\n > in main at tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_global_xy.c:9:3\n\n Undefined behavior (UB-CEE3):\n see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1\n see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nCannot compare pointers with different base objects using '<':\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:181:19\n in main at tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_global_xy.c:10:3\n\n Undefined behavior (UB-CERL1):\n see C11 section 6.5.8:5 http://rvdoc.org/C11/6.5.8\n see C11 section J.2:1 item 53 http://rvdoc.org/C11/J.2\n see CERT-C section ARR36-C http://rvdoc.org/CERT-C/ARR36-C\n see MISRA-C section 8.18:3 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nComparison of unspecified value:\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:181:19\n in main at tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_global_xy.c:10:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:56:24.876658", "duration": "0.358147" }, "source_hashes": "4dc50e19733632b4c8bb7629fab319f6 tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_global_xy.c\n", "sources": "#include \n#include \n#include \nint x=1, y=2;\nint main() {\n int *p = &x;\n int *q = &y;\n ptrdiff_t offset = q - p;\n int *r = p + offset;\n if (memcmp(&r, &q, sizeof(r)) == 0) {\n *r = 11; // is this free of UB?\n printf(\"y=%d *q=%d *r=%d\\n\",y,*q,*r); \n }\n}\n" }, { "test_recipe": { "test_instance_name": "pointer_offset_from_ptr_subtraction_global_yx.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_ptr_subtraction_global_yx.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_ptr_subtraction_global_yx.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/pointer_offset_from_ptr_subtraction_global_yx.c.kcc-1.0.out tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_global_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:56:25.779733", "duration": "4.790038" }, "binary_filename": "tests.bin/pointer_offset_from_ptr_subtraction_global_yx.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_ptr_subtraction_global_yx.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "Computing pointer difference between two different objects:\n > in main at tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_global_yx.c:8:3\n\n Undefined behavior (UB-CEA5):\n see C11 section 6.5.6:9 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 item 48 http://rvdoc.org/C11/J.2\n see CERT-C section ARR36-C http://rvdoc.org/CERT-C/ARR36-C\n see MISRA-C section 8.18:2 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nA pointer (or array subscript) outside the bounds of an object:\n > in main at tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_global_yx.c:9:3\n\n Undefined behavior (UB-CEA1):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 item 46 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nFound pointer that refers outside the bounds of an object + 1:\n > in main at tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_global_yx.c:9:3\n\n Undefined behavior (UB-CEE3):\n see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1\n see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nCannot compare pointers with different base objects using '<':\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:181:19\n in main at tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_global_yx.c:10:3\n\n Undefined behavior (UB-CERL1):\n see C11 section 6.5.8:5 http://rvdoc.org/C11/6.5.8\n see C11 section J.2:1 item 53 http://rvdoc.org/C11/J.2\n see CERT-C section ARR36-C http://rvdoc.org/CERT-C/ARR36-C\n see MISRA-C section 8.18:3 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nComparison of unspecified value:\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:181:19\n in main at tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_global_yx.c:10:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:56:30.569862", "duration": "0.348464" }, "source_hashes": "052b7ba8e5fb40d5d0dd0e4c262a65e9 tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_global_yx.c\n", "sources": "#include \n#include \n#include \nint y=2, x=1;\nint main() {\n int *p = &x;\n int *q = &y;\n ptrdiff_t offset = q - p;\n int *r = p + offset;\n if (memcmp(&r, &q, sizeof(r)) == 0) {\n *r = 11; // is this free of UB?\n printf(\"y=%d *q=%d *r=%d\\n\",y,*q,*r); \n }\n}\n" }, { "test_recipe": { "test_instance_name": "pointer_offset_from_ptr_subtraction_auto_xy.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_ptr_subtraction_auto_xy.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_ptr_subtraction_auto_xy.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/pointer_offset_from_ptr_subtraction_auto_xy.c.kcc-1.0.out tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_auto_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:56:31.467335", "duration": "4.863275" }, "binary_filename": "tests.bin/pointer_offset_from_ptr_subtraction_auto_xy.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_ptr_subtraction_auto_xy.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "Computing pointer difference between two different objects:\n > in main at tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_auto_xy.c:8:3\n\n Undefined behavior (UB-CEA5):\n see C11 section 6.5.6:9 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 item 48 http://rvdoc.org/C11/J.2\n see CERT-C section ARR36-C http://rvdoc.org/CERT-C/ARR36-C\n see MISRA-C section 8.18:2 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nA pointer (or array subscript) outside the bounds of an object:\n > in main at tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_auto_xy.c:9:3\n\n Undefined behavior (UB-CEA1):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 item 46 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nFound pointer that refers outside the bounds of an object + 1:\n > in main at tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_auto_xy.c:9:3\n\n Undefined behavior (UB-CEE3):\n see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1\n see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nCannot compare pointers with different base objects using '<':\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:181:19\n in main at tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_auto_xy.c:10:3\n\n Undefined behavior (UB-CERL1):\n see C11 section 6.5.8:5 http://rvdoc.org/C11/6.5.8\n see C11 section J.2:1 item 53 http://rvdoc.org/C11/J.2\n see CERT-C section ARR36-C http://rvdoc.org/CERT-C/ARR36-C\n see MISRA-C section 8.18:3 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nComparison of unspecified value:\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:181:19\n in main at tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_auto_xy.c:10:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:56:36.330789", "duration": "0.359336" }, "source_hashes": "82761f546f0951c0635ca743d9f6497e tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_auto_xy.c\n", "sources": "#include \n#include \n#include \nint main() {\n int x=1, y=2;\n int *p = &x;\n int *q = &y;\n ptrdiff_t offset = q - p;\n int *r = p + offset;\n if (memcmp(&r, &q, sizeof(r)) == 0) {\n *r = 11; // is this free of UB?\n printf(\"y=%d *q=%d *r=%d\\n\",y,*q,*r); \n }\n}\n" }, { "test_recipe": { "test_instance_name": "pointer_offset_from_ptr_subtraction_auto_yx.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_ptr_subtraction_auto_yx.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_ptr_subtraction_auto_yx.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/pointer_offset_from_ptr_subtraction_auto_yx.c.kcc-1.0.out tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_auto_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:56:37.238202", "duration": "4.869625" }, "binary_filename": "tests.bin/pointer_offset_from_ptr_subtraction_auto_yx.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_ptr_subtraction_auto_yx.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "Computing pointer difference between two different objects:\n > in main at tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_auto_yx.c:8:3\n\n Undefined behavior (UB-CEA5):\n see C11 section 6.5.6:9 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 item 48 http://rvdoc.org/C11/J.2\n see CERT-C section ARR36-C http://rvdoc.org/CERT-C/ARR36-C\n see MISRA-C section 8.18:2 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nA pointer (or array subscript) outside the bounds of an object:\n > in main at tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_auto_yx.c:9:3\n\n Undefined behavior (UB-CEA1):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 item 46 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nFound pointer that refers outside the bounds of an object + 1:\n > in main at tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_auto_yx.c:9:3\n\n Undefined behavior (UB-CEE3):\n see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1\n see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nCannot compare pointers with different base objects using '<':\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:181:19\n in main at tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_auto_yx.c:10:3\n\n Undefined behavior (UB-CERL1):\n see C11 section 6.5.8:5 http://rvdoc.org/C11/6.5.8\n see C11 section J.2:1 item 53 http://rvdoc.org/C11/J.2\n see CERT-C section ARR36-C http://rvdoc.org/CERT-C/ARR36-C\n see MISRA-C section 8.18:3 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nComparison of unspecified value:\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:181:19\n in main at tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_auto_yx.c:10:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:56:42.107923", "duration": "0.354227" }, "source_hashes": "8c16d64c183ab4fe89b732c12c51dfce tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_auto_yx.c\n", "sources": "#include \n#include \n#include \nint main() {\n int y=2, x=1;\n int *p = &x;\n int *q = &y;\n ptrdiff_t offset = q - p;\n int *r = p + offset;\n if (memcmp(&r, &q, sizeof(r)) == 0) {\n *r = 11; // is this free of UB?\n printf(\"y=%d *q=%d *r=%d\\n\",y,*q,*r); \n }\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_equality_global_xy.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_global_xy.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_global_xy.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_equality_global_xy.c.kcc-1.0.out tests/de_facto_memory_model/provenance_equality_global_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:56:43.013120", "duration": "4.840202" }, "binary_filename": "tests.bin/provenance_equality_global_xy.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_global_xy.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(nil) q=(nil)\n(p==q) = true\n", "stderr": "Comparison of unspecified value:\n > in main at tests/de_facto_memory_model/provenance_equality_global_xy.c:10:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:56:47.853416", "duration": "0.379862" }, "source_hashes": "26aa40e6598dde9f450926064ff59e2e tests/de_facto_memory_model/provenance_equality_global_xy.c\n", "sources": "#include \n#include \nint x=1, y=2;\nint main() {\n int *p = &x + 1;\n int *q = &y;\n printf(\"Addresses: p=%p q=%p\\n\",(void*)p,(void*)q);\n _Bool b = (p==q);\n // can this be false even with identical addresses?\n printf(\"(p==q) = %s\\n\", b?\"true\":\"false\");\n return 0;\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_equality_global_yx.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_global_yx.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_global_yx.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_equality_global_yx.c.kcc-1.0.out tests/de_facto_memory_model/provenance_equality_global_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:56:48.787231", "duration": "4.899898" }, "binary_filename": "tests.bin/provenance_equality_global_yx.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_global_yx.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(nil) q=(nil)\n(p==q) = true\n", "stderr": "Comparison of unspecified value:\n > in main at tests/de_facto_memory_model/provenance_equality_global_yx.c:10:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:56:53.687256", "duration": "0.390714" }, "source_hashes": "ce6bf977d427e2e8b0aae575111e152f tests/de_facto_memory_model/provenance_equality_global_yx.c\n", "sources": "#include \n#include \nint y=2, x=1;\nint main() {\n int *p = &x + 1;\n int *q = &y;\n printf(\"Addresses: p=%p q=%p\\n\",(void*)p,(void*)q);\n _Bool b = (p==q);\n // can this be false even with identical addresses?\n printf(\"(p==q) = %s\\n\", b?\"true\":\"false\");\n return 0;\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_equality_auto_xy.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_auto_xy.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_auto_xy.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_equality_auto_xy.c.kcc-1.0.out tests/de_facto_memory_model/provenance_equality_auto_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:56:54.627768", "duration": "4.873840" }, "binary_filename": "tests.bin/provenance_equality_auto_xy.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_auto_xy.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(nil) q=(nil)\n(p==q) = true\n", "stderr": "Comparison of unspecified value:\n > in main at tests/de_facto_memory_model/provenance_equality_auto_xy.c:9:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:56:59.501787", "duration": "0.392056" }, "source_hashes": "7866bbe8548f716f1165ed42e1079085 tests/de_facto_memory_model/provenance_equality_auto_xy.c\n", "sources": "#include \n#include \nint main() {\n int x=1, y=2;\n int *p = &x + 1;\n int *q = &y;\n printf(\"Addresses: p=%p q=%p\\n\",(void*)p,(void*)q);\n _Bool b = (p==q);\n printf(\"(p==q) = %s\\n\", b?\"true\":\"false\");\n return 0;\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_equality_auto_yx.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_auto_yx.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_auto_yx.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_equality_auto_yx.c.kcc-1.0.out tests/de_facto_memory_model/provenance_equality_auto_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:57:00.444224", "duration": "4.819572" }, "binary_filename": "tests.bin/provenance_equality_auto_yx.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_auto_yx.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(nil) q=(nil)\n(p==q) = true\n", "stderr": "Comparison of unspecified value:\n > in main at tests/de_facto_memory_model/provenance_equality_auto_yx.c:9:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:57:05.263976", "duration": "0.393484" }, "source_hashes": "a3213c4e767aadff3ff15a634c60953c tests/de_facto_memory_model/provenance_equality_auto_yx.c\n", "sources": "#include \n#include \nint main() {\n int y=2, x=1;\n int *p = &x + 1;\n int *q = &y;\n printf(\"Addresses: p=%p q=%p\\n\",(void*)p,(void*)q);\n _Bool b = (p==q);\n printf(\"(p==q) = %s\\n\", b?\"true\":\"false\");\n return 0;\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_equality_global_fn_xy.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_global_fn_xy.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_global_fn_xy.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_equality_global_fn_xy.c.kcc-1.0.out tests/de_facto_memory_model/provenance_equality_global_fn_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:57:06.205589", "duration": "4.859690" }, "binary_filename": "tests.bin/provenance_equality_global_fn_xy.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_global_fn_xy.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(nil) q=(nil)\n(p==q) = true\n", "stderr": "Comparison of unspecified value:\n > in f at tests/de_facto_memory_model/provenance_equality_global_fn_xy.c:7:3\n in main at tests/de_facto_memory_model/provenance_equality_global_fn_xy.c:14:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:57:11.065458", "duration": "0.389332" }, "source_hashes": "8cc023f8b944cd6ae079cc66a83c6f6e tests/de_facto_memory_model/provenance_equality_global_fn_xy.c\n", "sources": "#include \n#include \nint x=1, y=2;\nvoid f(int* p, int* q) {\n _Bool b = (p==q);\n // can this be false even with identical addresses?\n printf(\"(p==q) = %s\\n\", b?\"true\":\"false\");\n return;\n}\nint main() {\n int *p = &x + 1;\n int *q = &y;\n printf(\"Addresses: p=%p q=%p\\n\",(void*)p,(void*)q);\n f(p,q);\n return 0;\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_equality_global_fn_yx.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_global_fn_yx.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_global_fn_yx.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_equality_global_fn_yx.c.kcc-1.0.out tests/de_facto_memory_model/provenance_equality_global_fn_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:57:12.004146", "duration": "4.846367" }, "binary_filename": "tests.bin/provenance_equality_global_fn_yx.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_global_fn_yx.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(nil) q=(nil)\n(p==q) = true\n", "stderr": "Comparison of unspecified value:\n > in f at tests/de_facto_memory_model/provenance_equality_global_fn_yx.c:7:3\n in main at tests/de_facto_memory_model/provenance_equality_global_fn_yx.c:14:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:57:16.850606", "duration": "0.390363" }, "source_hashes": "04cfab7ffb77ca25883d2a0c7f7446f5 tests/de_facto_memory_model/provenance_equality_global_fn_yx.c\n", "sources": "#include \n#include \nint y=2, x=1;\nvoid f(int* p, int* q) {\n _Bool b = (p==q);\n // can this be false even with identical addresses?\n printf(\"(p==q) = %s\\n\", b?\"true\":\"false\");\n return;\n}\nint main() {\n int *p = &x + 1;\n int *q = &y;\n printf(\"Addresses: p=%p q=%p\\n\",(void*)p,(void*)q);\n f(p,q);\n return 0;\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_roundtrip_via_intptr_t.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_roundtrip_via_intptr_t.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_roundtrip_via_intptr_t.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_roundtrip_via_intptr_t.c.kcc-1.0.out tests/de_facto_memory_model/provenance_roundtrip_via_intptr_t.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:57:17.788351", "duration": "4.789116" }, "binary_filename": "tests.bin/provenance_roundtrip_via_intptr_t.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_roundtrip_via_intptr_t.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "*p=11 *q=11\n", "stderr": "Conversion from an integer to non-null pointer:\n > in main at tests/de_facto_memory_model/provenance_roundtrip_via_intptr_t.c:7:3\n\n Implementation defined behavior (IMPL-CCV13):\n see C11 section 6.3.2.3:5 http://rvdoc.org/C11/6.3.2.3\n see CERT section INT36-C http://rvdoc.org/CERT/INT36-C\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:57:22.577561", "duration": "0.360764" }, "source_hashes": "90f4dd6baa96b2277af4047b02e6fadb tests/de_facto_memory_model/provenance_roundtrip_via_intptr_t.c\n", "sources": "#include \n#include \nint x=1;\nint main() {\n int *p = &x;\n intptr_t i = (intptr_t)p;\n int *q = (int *)i;\n *q = 11; // is this free of undefined behaviour?\n printf(\"*p=%d *q=%d\\n\",*p,*q); \n}\n" }, { "test_recipe": { "test_instance_name": "provenance_basic_using_uintptr_t_global_xy.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_using_uintptr_t_global_xy.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_using_uintptr_t_global_xy.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_basic_using_uintptr_t_global_xy.c.kcc-1.0.out tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:57:23.488916", "duration": "4.978691" }, "binary_filename": "tests.bin/provenance_basic_using_uintptr_t_global_xy.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_using_uintptr_t_global_xy.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=(nil) p=(nil) &y=0\nx=1 y=2 *p=0 *q=2\n", "stderr": "Conversion from an integer to non-null pointer:\n > in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_xy.c:11:3\n\n Implementation defined behavior (IMPL-CCV13):\n see C11 section 6.3.2.3:5 http://rvdoc.org/C11/6.3.2.3\n see CERT section INT36-C http://rvdoc.org/CERT/INT36-C\n\nPrinting an unspecified value:\n > in printf at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_xy.c:13:3\n in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_xy.c:13:3\n\n Unspecified value or behavior (USP-STDIO2):\n see C11 section 7.21.6.1:8 http://rvdoc.org/C11/7.21.6.1\n\nComparison of unspecified value:\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:180:13\n in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_xy.c:15:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_xy.c:16:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nTrying to write outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_xy.c:16:5\n\n Undefined behavior (UB-EIO2):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section MEM35-C http://rvdoc.org/CERT-C/MEM35-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_xy.c:17:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nReading outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_xy.c:17:5\n\n Undefined behavior (UB-EIO7):\n see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1\n see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see CERT-C section STR32-C http://rvdoc.org/CERT-C/STR32-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:57:28.467731", "duration": "0.484107" }, "source_hashes": "37e5bf255eb2d738d638740b9b73d6c5 tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_xy.c\n", "sources": "#include \n#include \n#include \n#include \nint x=1, y=2;\nint main() {\n uintptr_t ux = (uintptr_t)&x;\n uintptr_t uy = (uintptr_t)&y;\n uintptr_t offset = 4;\n ux = ux + offset;\n int *p = (int *)ux; // does this have undefined behaviour?\n int *q = &y;\n printf(\"Addresses: &x=%p p=%p &y=%\"PRIxPTR\\\n \"\\n\",(void*)&x,(void*)p,uy);\n if (memcmp(&p, &q, sizeof(p)) == 0) {\n *p = 11; // does this have undefined behaviour?\n printf(\"x=%d y=%d *p=%d *q=%d\\n\",x,y,*p,*q); \n }\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_basic_using_uintptr_t_global_yx.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_using_uintptr_t_global_yx.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_using_uintptr_t_global_yx.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_basic_using_uintptr_t_global_yx.c.kcc-1.0.out tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:57:29.495337", "duration": "5.045537" }, "binary_filename": "tests.bin/provenance_basic_using_uintptr_t_global_yx.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_using_uintptr_t_global_yx.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=(nil) p=(nil) &y=0\nx=1 y=2 *p=0 *q=2\n", "stderr": "Conversion from an integer to non-null pointer:\n > in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_yx.c:11:3\n\n Implementation defined behavior (IMPL-CCV13):\n see C11 section 6.3.2.3:5 http://rvdoc.org/C11/6.3.2.3\n see CERT section INT36-C http://rvdoc.org/CERT/INT36-C\n\nPrinting an unspecified value:\n > in printf at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_yx.c:13:3\n in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_yx.c:13:3\n\n Unspecified value or behavior (USP-STDIO2):\n see C11 section 7.21.6.1:8 http://rvdoc.org/C11/7.21.6.1\n\nComparison of unspecified value:\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:180:13\n in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_yx.c:15:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_yx.c:16:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nTrying to write outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_yx.c:16:5\n\n Undefined behavior (UB-EIO2):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section MEM35-C http://rvdoc.org/CERT-C/MEM35-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_yx.c:17:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nReading outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_yx.c:17:5\n\n Undefined behavior (UB-EIO7):\n see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1\n see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see CERT-C section STR32-C http://rvdoc.org/CERT-C/STR32-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:57:34.540978", "duration": "0.481817" }, "source_hashes": "853634a0bfae84d8315ce1d20524fd81 tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_yx.c\n", "sources": "#include \n#include \n#include \n#include \nint y=2, x=1;\nint main() {\n uintptr_t ux = (uintptr_t)&x;\n uintptr_t uy = (uintptr_t)&y;\n uintptr_t offset = 4;\n ux = ux + offset;\n int *p = (int *)ux; // does this have undefined behaviour?\n int *q = &y;\n printf(\"Addresses: &x=%p p=%p &y=%\"PRIxPTR\\\n \"\\n\",(void*)&x,(void*)p,uy);\n if (memcmp(&p, &q, sizeof(p)) == 0) {\n *p = 11; // does this have undefined behaviour?\n printf(\"x=%d y=%d *p=%d *q=%d\\n\",x,y,*p,*q); \n }\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_basic_using_uintptr_t_auto_xy.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_using_uintptr_t_auto_xy.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_using_uintptr_t_auto_xy.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_basic_using_uintptr_t_auto_xy.c.kcc-1.0.out tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:57:35.580538", "duration": "5.069294" }, "binary_filename": "tests.bin/provenance_basic_using_uintptr_t_auto_xy.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_using_uintptr_t_auto_xy.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=(nil) p=(nil) &y=0\nx=1 y=2 *p=0 *q=2\n", "stderr": "Conversion from an integer to non-null pointer:\n > in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_xy.c:11:3\n\n Implementation defined behavior (IMPL-CCV13):\n see C11 section 6.3.2.3:5 http://rvdoc.org/C11/6.3.2.3\n see CERT section INT36-C http://rvdoc.org/CERT/INT36-C\n\nPrinting an unspecified value:\n > in printf at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_xy.c:13:3\n in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_xy.c:13:3\n\n Unspecified value or behavior (USP-STDIO2):\n see C11 section 7.21.6.1:8 http://rvdoc.org/C11/7.21.6.1\n\nComparison of unspecified value:\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:180:13\n in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_xy.c:15:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_xy.c:16:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nTrying to write outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_xy.c:16:5\n\n Undefined behavior (UB-EIO2):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section MEM35-C http://rvdoc.org/CERT-C/MEM35-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_xy.c:17:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nReading outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_xy.c:17:5\n\n Undefined behavior (UB-EIO7):\n see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1\n see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see CERT-C section STR32-C http://rvdoc.org/CERT-C/STR32-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nIndeterminate value used in an expression:\n > in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_xy.c:17:5\n\n Undefined behavior (UB-CEE2):\n see C11 section 6.2.4 http://rvdoc.org/C11/6.2.4\n see C11 section 6.7.9 http://rvdoc.org/C11/6.7.9\n see C11 section 6.8 http://rvdoc.org/C11/6.8\n see C11 section J.2:1 item 11 http://rvdoc.org/C11/J.2\n see CERT-C section EXP33-C http://rvdoc.org/CERT-C/EXP33-C\n see MISRA-C section 8.9:1 http://rvdoc.org/MISRA-C/8.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:57:40.649926", "duration": "0.478458" }, "source_hashes": "0606f007d8e9e66b377466f53e40be41 tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_xy.c\n", "sources": "#include \n#include \n#include \n#include \nint main() {\n int x=1, y=2;\n uintptr_t ux = (uintptr_t)&x;\n uintptr_t uy = (uintptr_t)&y;\n uintptr_t offset = 4;\n ux = ux + offset;\n int *p = (int *)ux; // does this have undefined behaviour?\n int *q = &y;\n printf(\"Addresses: &x=%p p=%p &y=%\"PRIxPTR\\\n \"\\n\",(void*)&x,(void*)p,uy);\n if (memcmp(&p, &q, sizeof(p)) == 0) {\n *p = 11; // does this have undefined behaviour?\n printf(\"x=%d y=%d *p=%d *q=%d\\n\",x,y,*p,*q); \n }\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_basic_using_uintptr_t_auto_yx.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_using_uintptr_t_auto_yx.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_using_uintptr_t_auto_yx.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_basic_using_uintptr_t_auto_yx.c.kcc-1.0.out tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:57:41.680334", "duration": "5.023087" }, "binary_filename": "tests.bin/provenance_basic_using_uintptr_t_auto_yx.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_using_uintptr_t_auto_yx.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=(nil) p=(nil) &y=0\nx=1 y=2 *p=0 *q=2\n", "stderr": "Conversion from an integer to non-null pointer:\n > in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_yx.c:11:3\n\n Implementation defined behavior (IMPL-CCV13):\n see C11 section 6.3.2.3:5 http://rvdoc.org/C11/6.3.2.3\n see CERT section INT36-C http://rvdoc.org/CERT/INT36-C\n\nPrinting an unspecified value:\n > in printf at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_yx.c:13:3\n in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_yx.c:13:3\n\n Unspecified value or behavior (USP-STDIO2):\n see C11 section 7.21.6.1:8 http://rvdoc.org/C11/7.21.6.1\n\nComparison of unspecified value:\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:180:13\n in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_yx.c:15:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_yx.c:16:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nTrying to write outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_yx.c:16:5\n\n Undefined behavior (UB-EIO2):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section MEM35-C http://rvdoc.org/CERT-C/MEM35-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_yx.c:17:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nReading outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_yx.c:17:5\n\n Undefined behavior (UB-EIO7):\n see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1\n see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see CERT-C section STR32-C http://rvdoc.org/CERT-C/STR32-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nIndeterminate value used in an expression:\n > in main at tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_yx.c:17:5\n\n Undefined behavior (UB-CEE2):\n see C11 section 6.2.4 http://rvdoc.org/C11/6.2.4\n see C11 section 6.7.9 http://rvdoc.org/C11/6.7.9\n see C11 section 6.8 http://rvdoc.org/C11/6.8\n see C11 section J.2:1 item 11 http://rvdoc.org/C11/J.2\n see CERT-C section EXP33-C http://rvdoc.org/CERT-C/EXP33-C\n see MISRA-C section 8.9:1 http://rvdoc.org/MISRA-C/8.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:57:46.703512", "duration": "0.486379" }, "source_hashes": "a9805b664c69390b8a3d87eaea34edf4 tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_yx.c\n", "sources": "#include \n#include \n#include \n#include \nint main() {\n int y=2, x=1;\n uintptr_t ux = (uintptr_t)&x;\n uintptr_t uy = (uintptr_t)&y;\n uintptr_t offset = 4;\n ux = ux + offset;\n int *p = (int *)ux; // does this have undefined behaviour?\n int *q = &y;\n printf(\"Addresses: &x=%p p=%p &y=%\"PRIxPTR\\\n \"\\n\",(void*)&x,(void*)p,uy);\n if (memcmp(&p, &q, sizeof(p)) == 0) {\n *p = 11; // does this have undefined behaviour?\n printf(\"x=%d y=%d *p=%d *q=%d\\n\",x,y,*p,*q); \n }\n}\n" }, { "test_recipe": { "test_instance_name": "pointer_offset_from_int_subtraction_global_xy.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_int_subtraction_global_xy.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_int_subtraction_global_xy.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/pointer_offset_from_int_subtraction_global_xy.c.kcc-1.0.out tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:57:47.742107", "duration": "4.976922" }, "binary_filename": "tests.bin/pointer_offset_from_int_subtraction_global_xy.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_int_subtraction_global_xy.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=0 &y=0 offset=9223372036854775807 \n", "stderr": "Computing pointer difference between two different objects:\n > in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_xy.c:9:3\n\n Undefined behavior (UB-CEA5):\n see C11 section 6.5.6:9 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 item 48 http://rvdoc.org/C11/J.2\n see CERT-C section ARR36-C http://rvdoc.org/CERT-C/ARR36-C\n see MISRA-C section 8.18:2 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nPrinting an unspecified value:\n > in printf at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_xy.c:10:3\n in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_xy.c:10:3\n\n Unspecified value or behavior (USP-STDIO2):\n see C11 section 7.21.6.1:8 http://rvdoc.org/C11/7.21.6.1\n\nA pointer (or array subscript) outside the bounds of an object:\n > in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_xy.c:12:3\n\n Undefined behavior (UB-CEA1):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 item 46 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nConversion from an integer to non-null pointer:\n > in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_xy.c:12:3\n\n Implementation defined behavior (IMPL-CCV13):\n see C11 section 6.3.2.3:5 http://rvdoc.org/C11/6.3.2.3\n see CERT section INT36-C http://rvdoc.org/CERT/INT36-C\n\nFound pointer that refers outside the bounds of an object + 1:\n > in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_xy.c:12:3\n\n Undefined behavior (UB-CEE3):\n see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1\n see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nCannot compare pointers with different base objects using '<':\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:181:19\n in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_xy.c:14:3\n\n Undefined behavior (UB-CERL1):\n see C11 section 6.5.8:5 http://rvdoc.org/C11/6.5.8\n see C11 section J.2:1 item 53 http://rvdoc.org/C11/J.2\n see CERT-C section ARR36-C http://rvdoc.org/CERT-C/ARR36-C\n see MISRA-C section 8.18:3 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nComparison of unspecified value:\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:181:19\n in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_xy.c:14:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:57:52.719125", "duration": "0.389320" }, "source_hashes": "04ee4b647030005644c209b9bca0fb67 tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_xy.c\n", "sources": "#include \n#include \n#include \n#include \nint x=1, y=2;\nint main() {\n uintptr_t ux = (uintptr_t)&x;\n uintptr_t uy = (uintptr_t)&y;\n uintptr_t offset = uy - ux;\n printf(\"Addresses: &x=%\"PRIuPTR\" &y=%\"PRIuPTR\\\n \" offset=%\"PRIuPTR\" \\n\",ux,uy,offset);\n int *p = (int *)(ux + offset);\n int *q = &y;\n if (memcmp(&p, &q, sizeof(p)) == 0) {\n *p = 11; // is this free of UB?\n printf(\"x=%d y=%d *p=%d *q=%d\\n\",x,y,*p,*q); \n }\n}\n" }, { "test_recipe": { "test_instance_name": "pointer_offset_from_int_subtraction_global_yx.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_int_subtraction_global_yx.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_int_subtraction_global_yx.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/pointer_offset_from_int_subtraction_global_yx.c.kcc-1.0.out tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:57:53.657160", "duration": "4.981181" }, "binary_filename": "tests.bin/pointer_offset_from_int_subtraction_global_yx.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_int_subtraction_global_yx.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=0 &y=0 offset=9223372036854775807 \n", "stderr": "Computing pointer difference between two different objects:\n > in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_yx.c:9:3\n\n Undefined behavior (UB-CEA5):\n see C11 section 6.5.6:9 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 item 48 http://rvdoc.org/C11/J.2\n see CERT-C section ARR36-C http://rvdoc.org/CERT-C/ARR36-C\n see MISRA-C section 8.18:2 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nPrinting an unspecified value:\n > in printf at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_yx.c:10:3\n in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_yx.c:10:3\n\n Unspecified value or behavior (USP-STDIO2):\n see C11 section 7.21.6.1:8 http://rvdoc.org/C11/7.21.6.1\n\nA pointer (or array subscript) outside the bounds of an object:\n > in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_yx.c:12:3\n\n Undefined behavior (UB-CEA1):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 item 46 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nConversion from an integer to non-null pointer:\n > in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_yx.c:12:3\n\n Implementation defined behavior (IMPL-CCV13):\n see C11 section 6.3.2.3:5 http://rvdoc.org/C11/6.3.2.3\n see CERT section INT36-C http://rvdoc.org/CERT/INT36-C\n\nFound pointer that refers outside the bounds of an object + 1:\n > in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_yx.c:12:3\n\n Undefined behavior (UB-CEE3):\n see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1\n see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nCannot compare pointers with different base objects using '<':\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:181:19\n in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_yx.c:14:3\n\n Undefined behavior (UB-CERL1):\n see C11 section 6.5.8:5 http://rvdoc.org/C11/6.5.8\n see C11 section J.2:1 item 53 http://rvdoc.org/C11/J.2\n see CERT-C section ARR36-C http://rvdoc.org/CERT-C/ARR36-C\n see MISRA-C section 8.18:3 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nComparison of unspecified value:\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:181:19\n in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_yx.c:14:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:57:58.638436", "duration": "0.388592" }, "source_hashes": "b45cf249e2910a1102ce3c24ff3f582d tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_yx.c\n", "sources": "#include \n#include \n#include \n#include \nint y=2, x=1;\nint main() {\n uintptr_t ux = (uintptr_t)&x;\n uintptr_t uy = (uintptr_t)&y;\n uintptr_t offset = uy - ux;\n printf(\"Addresses: &x=%\"PRIuPTR\" &y=%\"PRIuPTR\\\n \" offset=%\"PRIuPTR\" \\n\",ux,uy,offset);\n int *p = (int *)(ux + offset);\n int *q = &y;\n if (memcmp(&p, &q, sizeof(p)) == 0) {\n *p = 11; // is this free of UB?\n printf(\"x=%d y=%d *p=%d *q=%d\\n\",x,y,*p,*q); \n }\n}\n" }, { "test_recipe": { "test_instance_name": "pointer_offset_from_int_subtraction_auto_xy.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_int_subtraction_auto_xy.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_int_subtraction_auto_xy.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/pointer_offset_from_int_subtraction_auto_xy.c.kcc-1.0.out tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:57:59.574359", "duration": "4.975657" }, "binary_filename": "tests.bin/pointer_offset_from_int_subtraction_auto_xy.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_int_subtraction_auto_xy.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=0 &y=0 offset=9223372036854775807 \n", "stderr": "Computing pointer difference between two different objects:\n > in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_xy.c:9:3\n\n Undefined behavior (UB-CEA5):\n see C11 section 6.5.6:9 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 item 48 http://rvdoc.org/C11/J.2\n see CERT-C section ARR36-C http://rvdoc.org/CERT-C/ARR36-C\n see MISRA-C section 8.18:2 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nPrinting an unspecified value:\n > in printf at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_xy.c:10:3\n in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_xy.c:10:3\n\n Unspecified value or behavior (USP-STDIO2):\n see C11 section 7.21.6.1:8 http://rvdoc.org/C11/7.21.6.1\n\nA pointer (or array subscript) outside the bounds of an object:\n > in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_xy.c:12:3\n\n Undefined behavior (UB-CEA1):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 item 46 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nConversion from an integer to non-null pointer:\n > in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_xy.c:12:3\n\n Implementation defined behavior (IMPL-CCV13):\n see C11 section 6.3.2.3:5 http://rvdoc.org/C11/6.3.2.3\n see CERT section INT36-C http://rvdoc.org/CERT/INT36-C\n\nFound pointer that refers outside the bounds of an object + 1:\n > in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_xy.c:12:3\n\n Undefined behavior (UB-CEE3):\n see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1\n see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nCannot compare pointers with different base objects using '<':\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:181:19\n in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_xy.c:14:3\n\n Undefined behavior (UB-CERL1):\n see C11 section 6.5.8:5 http://rvdoc.org/C11/6.5.8\n see C11 section J.2:1 item 53 http://rvdoc.org/C11/J.2\n see CERT-C section ARR36-C http://rvdoc.org/CERT-C/ARR36-C\n see MISRA-C section 8.18:3 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nComparison of unspecified value:\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:181:19\n in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_xy.c:14:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:58:04.550112", "duration": "0.394791" }, "source_hashes": "1135e6a02e05022f7a143808a2d15a10 tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_xy.c\n", "sources": "#include \n#include \n#include \n#include \nint main() {\n int x=1, y=2;\n uintptr_t ux = (uintptr_t)&x;\n uintptr_t uy = (uintptr_t)&y;\n uintptr_t offset = uy - ux;\n printf(\"Addresses: &x=%\"PRIuPTR\" &y=%\"PRIuPTR\\\n \" offset=%\"PRIuPTR\" \\n\",ux,uy,offset);\n int *p = (int *)(ux + offset);\n int *q = &y;\n if (memcmp(&p, &q, sizeof(p)) == 0) {\n *p = 11; // is this free of UB?\n printf(\"x=%d y=%d *p=%d *q=%d\\n\",x,y,*p,*q); \n }\n}\n" }, { "test_recipe": { "test_instance_name": "pointer_offset_from_int_subtraction_auto_yx.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_int_subtraction_auto_yx.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_int_subtraction_auto_yx.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/pointer_offset_from_int_subtraction_auto_yx.c.kcc-1.0.out tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:58:05.503519", "duration": "4.986225" }, "binary_filename": "tests.bin/pointer_offset_from_int_subtraction_auto_yx.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_int_subtraction_auto_yx.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=0 &y=0 offset=9223372036854775807 \n", "stderr": "Computing pointer difference between two different objects:\n > in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_yx.c:9:3\n\n Undefined behavior (UB-CEA5):\n see C11 section 6.5.6:9 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 item 48 http://rvdoc.org/C11/J.2\n see CERT-C section ARR36-C http://rvdoc.org/CERT-C/ARR36-C\n see MISRA-C section 8.18:2 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nPrinting an unspecified value:\n > in printf at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_yx.c:10:3\n in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_yx.c:10:3\n\n Unspecified value or behavior (USP-STDIO2):\n see C11 section 7.21.6.1:8 http://rvdoc.org/C11/7.21.6.1\n\nA pointer (or array subscript) outside the bounds of an object:\n > in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_yx.c:12:3\n\n Undefined behavior (UB-CEA1):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 item 46 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nConversion from an integer to non-null pointer:\n > in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_yx.c:12:3\n\n Implementation defined behavior (IMPL-CCV13):\n see C11 section 6.3.2.3:5 http://rvdoc.org/C11/6.3.2.3\n see CERT section INT36-C http://rvdoc.org/CERT/INT36-C\n\nFound pointer that refers outside the bounds of an object + 1:\n > in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_yx.c:12:3\n\n Undefined behavior (UB-CEE3):\n see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1\n see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nCannot compare pointers with different base objects using '<':\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:181:19\n in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_yx.c:14:3\n\n Undefined behavior (UB-CERL1):\n see C11 section 6.5.8:5 http://rvdoc.org/C11/6.5.8\n see C11 section J.2:1 item 53 http://rvdoc.org/C11/J.2\n see CERT-C section ARR36-C http://rvdoc.org/CERT-C/ARR36-C\n see MISRA-C section 8.18:3 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nComparison of unspecified value:\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:181:19\n in main at tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_yx.c:14:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:58:10.489925", "duration": "0.398883" }, "source_hashes": "fe7e4a244209d3ee98b0080ba0b16156 tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_yx.c\n", "sources": "#include \n#include \n#include \n#include \nint main() {\n int y=2, x=1;\n uintptr_t ux = (uintptr_t)&x;\n uintptr_t uy = (uintptr_t)&y;\n uintptr_t offset = uy - ux;\n printf(\"Addresses: &x=%\"PRIuPTR\" &y=%\"PRIuPTR\\\n \" offset=%\"PRIuPTR\" \\n\",ux,uy,offset);\n int *p = (int *)(ux + offset);\n int *q = &y;\n if (memcmp(&p, &q, sizeof(p)) == 0) {\n *p = 11; // is this free of UB?\n printf(\"x=%d y=%d *p=%d *q=%d\\n\",x,y,*p,*q); \n }\n}\n" }, { "test_recipe": { "test_instance_name": "pointer_offset_xor_global.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_xor_global.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_xor_global.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/pointer_offset_xor_global.c.kcc-1.0.out tests/de_facto_memory_model/pointer_offset_xor_global.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:58:11.440103", "duration": "4.751681" }, "binary_filename": "tests.bin/pointer_offset_xor_global.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_xor_global.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "Conversion from an integer to non-null pointer:\n > in main at tests/de_facto_memory_model/pointer_offset_xor_global.c:12:3\n\n Implementation defined behavior (IMPL-CCV13):\n see C11 section 6.3.2.3:5 http://rvdoc.org/C11/6.3.2.3\n see CERT section INT36-C http://rvdoc.org/CERT/INT36-C\n\nIndeterminate value used in an expression:\n > in main at tests/de_facto_memory_model/pointer_offset_xor_global.c:12:3\n\n Undefined behavior (UB-CEE2):\n see C11 section 6.2.4 http://rvdoc.org/C11/6.2.4\n see C11 section 6.7.9 http://rvdoc.org/C11/6.7.9\n see C11 section 6.8 http://rvdoc.org/C11/6.8\n see C11 section J.2:1 item 11 http://rvdoc.org/C11/J.2\n see CERT-C section EXP33-C http://rvdoc.org/CERT-C/EXP33-C\n see MISRA-C section 8.9:1 http://rvdoc.org/MISRA-C/8.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a null pointer:\n > in main at tests/de_facto_memory_model/pointer_offset_xor_global.c:14:3\n\n Undefined behavior (UB-CER3):\n see C11 section 6.5.3.2:4 http://rvdoc.org/C11/6.5.3.2\n see C11 section J.2:1 item 43 http://rvdoc.org/C11/J.2\n see CERT-C section EXP34-C http://rvdoc.org/CERT-C/EXP34-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nExecution failed (configuration dumped)\n", "exit_code": "139", "signals": "", "start_time": "2018.11.07 3:58:16.191874", "duration": "0.603409" }, "source_hashes": "05ff96f9a69da95a8d7c17c0ddbccde0 tests/de_facto_memory_model/pointer_offset_xor_global.c\n", "sources": "#include \n#include \nint x=1;\nint y=2; \nint main() {\n int *p = &x;\n int *q = &y;\n uintptr_t i = (uintptr_t) p;\n uintptr_t j = (uintptr_t) q;\n uintptr_t k = i ^ j;\n uintptr_t l = k ^ i;\n int *r = (int *)l;\n // are r and q now equivalent? \n *r = 11; // does this have defined behaviour? \n _Bool b = (r==q); \n printf(\"x=%i y=%i *r=%i (r==p)=%s\\n\",x,y,*r,\n b?\"true\":\"false\"); \n}\n" }, { "test_recipe": { "test_instance_name": "pointer_offset_xor_auto.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_xor_auto.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_xor_auto.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/pointer_offset_xor_auto.c.kcc-1.0.out tests/de_facto_memory_model/pointer_offset_xor_auto.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:58:17.360645", "duration": "4.831430" }, "binary_filename": "tests.bin/pointer_offset_xor_auto.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_xor_auto.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "Conversion from an integer to non-null pointer:\n > in main at tests/de_facto_memory_model/pointer_offset_xor_auto.c:11:3\n\n Implementation defined behavior (IMPL-CCV13):\n see C11 section 6.3.2.3:5 http://rvdoc.org/C11/6.3.2.3\n see CERT section INT36-C http://rvdoc.org/CERT/INT36-C\n\nIndeterminate value used in an expression:\n > in main at tests/de_facto_memory_model/pointer_offset_xor_auto.c:11:3\n\n Undefined behavior (UB-CEE2):\n see C11 section 6.2.4 http://rvdoc.org/C11/6.2.4\n see C11 section 6.7.9 http://rvdoc.org/C11/6.7.9\n see C11 section 6.8 http://rvdoc.org/C11/6.8\n see C11 section J.2:1 item 11 http://rvdoc.org/C11/J.2\n see CERT-C section EXP33-C http://rvdoc.org/CERT-C/EXP33-C\n see MISRA-C section 8.9:1 http://rvdoc.org/MISRA-C/8.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a null pointer:\n > in main at tests/de_facto_memory_model/pointer_offset_xor_auto.c:13:3\n\n Undefined behavior (UB-CER3):\n see C11 section 6.5.3.2:4 http://rvdoc.org/C11/6.5.3.2\n see C11 section J.2:1 item 43 http://rvdoc.org/C11/J.2\n see CERT-C section EXP34-C http://rvdoc.org/CERT-C/EXP34-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nExecution failed (configuration dumped)\n", "exit_code": "139", "signals": "", "start_time": "2018.11.07 3:58:22.192166", "duration": "0.627490" }, "source_hashes": "77a4e1c144667af5f55c6f80a0bef5db tests/de_facto_memory_model/pointer_offset_xor_auto.c\n", "sources": "#include \n#include \nint main() {\n int x=1, y=2;\n int *p = &x;\n int *q = &y;\n uintptr_t i = (uintptr_t) p;\n uintptr_t j = (uintptr_t) q;\n uintptr_t k = i ^ j;\n uintptr_t l = k ^ i;\n int *r = (int *)l;\n // are r and q now equivalent? \n *r = 11; // does this have defined behaviour? \n _Bool b = (r==q); \n printf(\"x=%i y=%i *r=%i (r==p)=%s\\n\",x,y,*r,\n b?\"true\":\"false\"); \n}\n" }, { "test_recipe": { "test_instance_name": "provenance_tag_bits_via_uintptr_t_1.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_tag_bits_via_uintptr_t_1.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_tag_bits_via_uintptr_t_1.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_tag_bits_via_uintptr_t_1.c.kcc-1.0.out tests/de_facto_memory_model/provenance_tag_bits_via_uintptr_t_1.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:58:23.357864", "duration": "4.804788" }, "binary_filename": "tests.bin/provenance_tag_bits_via_uintptr_t_1.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_tag_bits_via_uintptr_t_1.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "x=11 *r=11 (r==p)=true\n", "stderr": "Conversion from an integer to non-null pointer:\n > in main at tests/de_facto_memory_model/provenance_tag_bits_via_uintptr_t_1.c:15:3\n\n Implementation defined behavior (IMPL-CCV13):\n see C11 section 6.3.2.3:5 http://rvdoc.org/C11/6.3.2.3\n see CERT section INT36-C http://rvdoc.org/CERT/INT36-C\n\nConversion from an integer to non-null pointer:\n > in main at tests/de_facto_memory_model/provenance_tag_bits_via_uintptr_t_1.c:19:3\n\n Implementation defined behavior (IMPL-CCV13):\n see C11 section 6.3.2.3:5 http://rvdoc.org/C11/6.3.2.3\n see CERT section INT36-C http://rvdoc.org/CERT/INT36-C\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:58:28.162766", "duration": "0.373584" }, "source_hashes": "148613212aab083b3efb066445ca3bf6 tests/de_facto_memory_model/provenance_tag_bits_via_uintptr_t_1.c\n", "sources": "#include \n#include \n#include \nint x=1;\nint main() {\n int *p = &x;\n // cast &x to an integer \n uintptr_t i = (uintptr_t) p;\n // check the bottom two bits of an int* are not used\n assert(_Alignof(int) >= 4);\n assert((i & 3u) == 0u);\n // construct an integer like &x with low-order bit set\n i = i | 1u; \n // cast back to a pointer\n int *q = (int *) i; // does this have defined behaviour?\n // cast to integer and mask out the low-order two bits\n uintptr_t j = ((uintptr_t)q) & ~((uintptr_t)3u); \n // cast back to a pointer\n int *r = (int *) j; \n // are r and p now equivalent? \n *r = 11; // does this have defined behaviour? \n _Bool b = (r==p); // is this true?\n printf(\"x=%i *r=%i (r==p)=%s\\n\",x,*r,b?\"true\":\"false\"); \n}\n" }, { "test_recipe": { "test_instance_name": "pointer_arith_algebraic_properties_2_global.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_arith_algebraic_properties_2_global.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_arith_algebraic_properties_2_global.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/pointer_arith_algebraic_properties_2_global.c.kcc-1.0.out tests/de_facto_memory_model/pointer_arith_algebraic_properties_2_global.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "tests/de_facto_memory_model/pointer_arith_algebraic_properties_2_global.c:5:3: warning: Conversion from an integer to non-null pointer.\n\n Implementation defined behavior (IMPL-CCV13):\n see C11 section 6.3.2.3:5 http://rvdoc.org/C11/6.3.2.3\n see CERT section INT36-C http://rvdoc.org/CERT/INT36-C\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:58:29.086486", "duration": "4.856721" }, "binary_filename": "tests.bin/pointer_arith_algebraic_properties_2_global.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/pointer_arith_algebraic_properties_2_global.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "x[1]=11 *p=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:58:33.943420", "duration": "0.362446" }, "source_hashes": "9fd8a7d0f8bb3fa846121d301479cefa tests/de_facto_memory_model/pointer_arith_algebraic_properties_2_global.c\n", "sources": "#include \n#include \nint y[2], x[2];\nint main() {\n int *p=(int*)(((uintptr_t)&(x[0])) + \n (((uintptr_t)&(y[1]))-((uintptr_t)&(y[0]))));\n *p = 11; // is this free of undefined behaviour?\n printf(\"x[1]=%d *p=%d\\n\",x[1],*p);\n return 0;\n}\n" }, { "test_recipe": { "test_instance_name": "pointer_arith_algebraic_properties_3_global.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_arith_algebraic_properties_3_global.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_arith_algebraic_properties_3_global.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/pointer_arith_algebraic_properties_3_global.c.kcc-1.0.out tests/de_facto_memory_model/pointer_arith_algebraic_properties_3_global.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "tests/de_facto_memory_model/pointer_arith_algebraic_properties_3_global.c:5:3: error: A pointer (or array subscript) outside the bounds of an object.\n\n Undefined behavior (UB-CEA1):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 item 46 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\ntests/de_facto_memory_model/pointer_arith_algebraic_properties_3_global.c:5:3: error: Computing pointer difference between two different objects.\n\n Undefined behavior (UB-CEA5):\n see C11 section 6.5.6:9 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 item 48 http://rvdoc.org/C11/J.2\n see CERT-C section ARR36-C http://rvdoc.org/CERT-C/ARR36-C\n see MISRA-C section 8.18:2 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\ntests/de_facto_memory_model/pointer_arith_algebraic_properties_3_global.c:5:3: warning: Conversion from an integer to non-null pointer.\n\n Implementation defined behavior (IMPL-CCV13):\n see C11 section 6.3.2.3:5 http://rvdoc.org/C11/6.3.2.3\n see CERT section INT36-C http://rvdoc.org/CERT/INT36-C\n\ntests/de_facto_memory_model/pointer_arith_algebraic_properties_3_global.c:5:3: error: Indeterminate value used in an expression.\n\n Undefined behavior (UB-CEE2):\n see C11 section 6.2.4 http://rvdoc.org/C11/6.2.4\n see C11 section 6.7.9 http://rvdoc.org/C11/6.7.9\n see C11 section 6.8 http://rvdoc.org/C11/6.8\n see C11 section J.2:1 item 11 http://rvdoc.org/C11/J.2\n see CERT-C section EXP33-C http://rvdoc.org/CERT-C/EXP33-C\n see MISRA-C section 8.9:1 http://rvdoc.org/MISRA-C/8.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:58:34.857203", "duration": "4.854375" }, "binary_filename": "tests.bin/pointer_arith_algebraic_properties_3_global.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/pointer_arith_algebraic_properties_3_global.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "Dereferencing a null pointer:\n > in main at tests/de_facto_memory_model/pointer_arith_algebraic_properties_3_global.c:8:3\n\n Undefined behavior (UB-CER3):\n see C11 section 6.5.3.2:4 http://rvdoc.org/C11/6.5.3.2\n see C11 section J.2:1 item 43 http://rvdoc.org/C11/J.2\n see CERT-C section EXP34-C http://rvdoc.org/CERT-C/EXP34-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nExecution failed (configuration dumped)\n", "exit_code": "139", "signals": "", "start_time": "2018.11.07 3:58:39.711717", "duration": "0.468949" }, "source_hashes": "9504f7c91edcccc0e4f2b032eefe8087 tests/de_facto_memory_model/pointer_arith_algebraic_properties_3_global.c\n", "sources": "#include \n#include \nint y[2], x[2];\nint main() {\n int *p=(int*)(\n (((uintptr_t)&(x[0])) + ((uintptr_t)&(y[1])))\n -((uintptr_t)&(y[0])) );\n *p = 11; // is this free of undefined behaviour?\n //(equivalent to the &x[0]+(&(y[1])-&(y[0])) version?)\n printf(\"x[1]=%d *p=%d\\n\",x[1],*p);\n return 0;\n}\n" }, { "test_recipe": { "test_instance_name": "pointer_copy_memcpy.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_copy_memcpy.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_copy_memcpy.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/pointer_copy_memcpy.c.kcc-1.0.out tests/de_facto_memory_model/pointer_copy_memcpy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:58:40.728779", "duration": "4.974012" }, "binary_filename": "tests.bin/pointer_copy_memcpy.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/pointer_copy_memcpy.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "*p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:58:45.702883", "duration": "0.444073" }, "source_hashes": "2cc877ce1cfe4a0f0a76e9d004b84c72 tests/de_facto_memory_model/pointer_copy_memcpy.c\n", "sources": "#include \n#include \nint x=1;\nint main() {\n int *p = &x;\n int *q;\n memcpy (&q, &p, sizeof p); \n *q = 11; // is this free of undefined behaviour?\n printf(\"*p=%d *q=%d\\n\",*p,*q); \n}\n" }, { "test_recipe": { "test_instance_name": "pointer_copy_user_dataflow_direct_bytewise.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_copy_user_dataflow_direct_bytewise.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_copy_user_dataflow_direct_bytewise.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/pointer_copy_user_dataflow_direct_bytewise.c.kcc-1.0.out tests/de_facto_memory_model/pointer_copy_user_dataflow_direct_bytewise.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:58:46.703627", "duration": "4.883842" }, "binary_filename": "tests.bin/pointer_copy_user_dataflow_direct_bytewise.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/pointer_copy_user_dataflow_direct_bytewise.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "*p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:58:51.587560", "duration": "0.430845" }, "source_hashes": "000b50d0b2e6bf7cf821dd0b7ef04f6a tests/de_facto_memory_model/pointer_copy_user_dataflow_direct_bytewise.c\n", "sources": "#include \n#include \nint x=1;\nvoid user_memcpy(unsigned char* dest, \n unsigned char *src, size_t n) {\n while (n > 0) {\t\t\n *dest = *src;\n src += 1; dest += 1; n -= 1;\n }\n}\nint main() {\n int *p = &x;\n int *q;\n user_memcpy((unsigned char*)&q, \n (unsigned char*)&p, sizeof(int *));\n *q = 11; // is this free of undefined behaviour?\n printf(\"*p=%d *q=%d\\n\",*p,*q);\n}\n" }, { "test_recipe": { "test_instance_name": "pointer_copy_user_ctrlflow_bytewise.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_copy_user_ctrlflow_bytewise.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_copy_user_ctrlflow_bytewise.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/pointer_copy_user_ctrlflow_bytewise.c.kcc-1.0.out tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bytewise.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:58:52.564293", "duration": "7.191583" }, "binary_filename": "tests.bin/pointer_copy_user_ctrlflow_bytewise.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/pointer_copy_user_ctrlflow_bytewise.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "Switching on an unspecified controlling expression:\n > in control_flow_copy at tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bytewise.c:8:3\n in user_memcpy2 at tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bytewise.c:271:5\n in main at tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bytewise.c:280:3\n\n Unspecified value or behavior (USP-ESS1):\n see C11 section 6.8.4.2:5 http://rvdoc.org/C11/6.8.4.2\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nCasting empty value to type other than void:\n > in control_flow_copy at tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bytewise.c:8:3\n in user_memcpy2 at tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bytewise.c:271:5\n in main at tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bytewise.c:280:3\n\n Undefined behavior (UB-CCV5):\n see C11 section 6.3.2.2:1 http://rvdoc.org/C11/6.3.2.2\n see C11 section J.2:1 item 23 http://rvdoc.org/C11/J.2\n see CERT-C section MSC15-C http://rvdoc.org/CERT-C/MSC15-C\n see CERT-C section MSC37-C http://rvdoc.org/CERT-C/MSC37-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nIndeterminate value used in an expression:\n > in user_memcpy2 at tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bytewise.c:271:5\n in main at tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bytewise.c:280:3\n\n Undefined behavior (UB-CEE2):\n see C11 section 6.2.4 http://rvdoc.org/C11/6.2.4\n see C11 section 6.7.9 http://rvdoc.org/C11/6.7.9\n see C11 section 6.8 http://rvdoc.org/C11/6.8\n see C11 section J.2:1 item 11 http://rvdoc.org/C11/J.2\n see CERT-C section EXP33-C http://rvdoc.org/CERT-C/EXP33-C\n see MISRA-C section 8.9:1 http://rvdoc.org/MISRA-C/8.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a null pointer:\n > in main at tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bytewise.c:282:3\n\n Undefined behavior (UB-CER3):\n see C11 section 6.5.3.2:4 http://rvdoc.org/C11/6.5.3.2\n see C11 section J.2:1 item 43 http://rvdoc.org/C11/J.2\n see CERT-C section EXP34-C http://rvdoc.org/CERT-C/EXP34-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nExecution failed (configuration dumped)\n", "exit_code": "139", "signals": "", "start_time": "2018.11.07 3:58:59.755971", "duration": "3.257677" }, "source_hashes": "4a9bb684e2fb4f5cb2b08ef9f7c3841d tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bytewise.c\n", "sources": "#include \n#include \n#include \n#include \nint x=1;\nunsigned char control_flow_copy(unsigned char c) {\n assert(UCHAR_MAX==255);\n switch (c) {\n case 0: return(0);\n case 1: return(1);\n case 2: return(2);\n case 3: return(3);\n case 4: return(4);\n case 5: return(5);\n case 6: return(6);\n case 7: return(7);\n case 8: return(8);\n case 9: return(9);\n case 10: return(10);\n case 11: return(11);\n case 12: return(12);\n case 13: return(13);\n case 14: return(14);\n case 15: return(15);\n case 16: return(16);\n case 17: return(17);\n case 18: return(18);\n case 19: return(19);\n case 20: return(20);\n case 21: return(21);\n case 22: return(22);\n case 23: return(23);\n case 24: return(24);\n case 25: return(25);\n case 26: return(26);\n case 27: return(27);\n case 28: return(28);\n case 29: return(29);\n case 30: return(30);\n case 31: return(31);\n case 32: return(32);\n case 33: return(33);\n case 34: return(34);\n case 35: return(35);\n case 36: return(36);\n case 37: return(37);\n case 38: return(38);\n case 39: return(39);\n case 40: return(40);\n case 41: return(41);\n case 42: return(42);\n case 43: return(43);\n case 44: return(44);\n case 45: return(45);\n case 46: return(46);\n case 47: return(47);\n case 48: return(48);\n case 49: return(49);\n case 50: return(50);\n case 51: return(51);\n case 52: return(52);\n case 53: return(53);\n case 54: return(54);\n case 55: return(55);\n case 56: return(56);\n case 57: return(57);\n case 58: return(58);\n case 59: return(59);\n case 60: return(60);\n case 61: return(61);\n case 62: return(62);\n case 63: return(63);\n case 64: return(64);\n case 65: return(65);\n case 66: return(66);\n case 67: return(67);\n case 68: return(68);\n case 69: return(69);\n case 70: return(70);\n case 71: return(71);\n case 72: return(72);\n case 73: return(73);\n case 74: return(74);\n case 75: return(75);\n case 76: return(76);\n case 77: return(77);\n case 78: return(78);\n case 79: return(79);\n case 80: return(80);\n case 81: return(81);\n case 82: return(82);\n case 83: return(83);\n case 84: return(84);\n case 85: return(85);\n case 86: return(86);\n case 87: return(87);\n case 88: return(88);\n case 89: return(89);\n case 90: return(90);\n case 91: return(91);\n case 92: return(92);\n case 93: return(93);\n case 94: return(94);\n case 95: return(95);\n case 96: return(96);\n case 97: return(97);\n case 98: return(98);\n case 99: return(99);\n case 100: return(100);\n case 101: return(101);\n case 102: return(102);\n case 103: return(103);\n case 104: return(104);\n case 105: return(105);\n case 106: return(106);\n case 107: return(107);\n case 108: return(108);\n case 109: return(109);\n case 110: return(110);\n case 111: return(111);\n case 112: return(112);\n case 113: return(113);\n case 114: return(114);\n case 115: return(115);\n case 116: return(116);\n case 117: return(117);\n case 118: return(118);\n case 119: return(119);\n case 120: return(120);\n case 121: return(121);\n case 122: return(122);\n case 123: return(123);\n case 124: return(124);\n case 125: return(125);\n case 126: return(126);\n case 127: return(127);\n case 128: return(128);\n case 129: return(129);\n case 130: return(130);\n case 131: return(131);\n case 132: return(132);\n case 133: return(133);\n case 134: return(134);\n case 135: return(135);\n case 136: return(136);\n case 137: return(137);\n case 138: return(138);\n case 139: return(139);\n case 140: return(140);\n case 141: return(141);\n case 142: return(142);\n case 143: return(143);\n case 144: return(144);\n case 145: return(145);\n case 146: return(146);\n case 147: return(147);\n case 148: return(148);\n case 149: return(149);\n case 150: return(150);\n case 151: return(151);\n case 152: return(152);\n case 153: return(153);\n case 154: return(154);\n case 155: return(155);\n case 156: return(156);\n case 157: return(157);\n case 158: return(158);\n case 159: return(159);\n case 160: return(160);\n case 161: return(161);\n case 162: return(162);\n case 163: return(163);\n case 164: return(164);\n case 165: return(165);\n case 166: return(166);\n case 167: return(167);\n case 168: return(168);\n case 169: return(169);\n case 170: return(170);\n case 171: return(171);\n case 172: return(172);\n case 173: return(173);\n case 174: return(174);\n case 175: return(175);\n case 176: return(176);\n case 177: return(177);\n case 178: return(178);\n case 179: return(179);\n case 180: return(180);\n case 181: return(181);\n case 182: return(182);\n case 183: return(183);\n case 184: return(184);\n case 185: return(185);\n case 186: return(186);\n case 187: return(187);\n case 188: return(188);\n case 189: return(189);\n case 190: return(190);\n case 191: return(191);\n case 192: return(192);\n case 193: return(193);\n case 194: return(194);\n case 195: return(195);\n case 196: return(196);\n case 197: return(197);\n case 198: return(198);\n case 199: return(199);\n case 200: return(200);\n case 201: return(201);\n case 202: return(202);\n case 203: return(203);\n case 204: return(204);\n case 205: return(205);\n case 206: return(206);\n case 207: return(207);\n case 208: return(208);\n case 209: return(209);\n case 210: return(210);\n case 211: return(211);\n case 212: return(212);\n case 213: return(213);\n case 214: return(214);\n case 215: return(215);\n case 216: return(216);\n case 217: return(217);\n case 218: return(218);\n case 219: return(219);\n case 220: return(220);\n case 221: return(221);\n case 222: return(222);\n case 223: return(223);\n case 224: return(224);\n case 225: return(225);\n case 226: return(226);\n case 227: return(227);\n case 228: return(228);\n case 229: return(229);\n case 230: return(230);\n case 231: return(231);\n case 232: return(232);\n case 233: return(233);\n case 234: return(234);\n case 235: return(235);\n case 236: return(236);\n case 237: return(237);\n case 238: return(238);\n case 239: return(239);\n case 240: return(240);\n case 241: return(241);\n case 242: return(242);\n case 243: return(243);\n case 244: return(244);\n case 245: return(245);\n case 246: return(246);\n case 247: return(247);\n case 248: return(248);\n case 249: return(249);\n case 250: return(250);\n case 251: return(251);\n case 252: return(252);\n case 253: return(253);\n case 254: return(254);\n case 255: return(255);\n }\n}\n\nvoid user_memcpy2(unsigned char* dest, \n unsigned char *src, size_t n) {\n while (n > 0) {\t\t\n *dest = control_flow_copy(*src);\n src += 1;\n dest += 1;\n n -= 1;\n }\n}\nint main() {\n int *p = &x;\n int *q;\n user_memcpy2((unsigned char*)&q, (unsigned char*)&p, \n sizeof(p));\n *q = 11; // does this have undefined behaviour?\n printf(\"*p=%d *q=%d\\n\",*p,*q);\n}\n" }, { "test_recipe": { "test_instance_name": "pointer_copy_user_ctrlflow_bitwise.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_copy_user_ctrlflow_bitwise.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_copy_user_ctrlflow_bitwise.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/pointer_copy_user_ctrlflow_bitwise.c.kcc-1.0.out tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bitwise.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:59:03.722196", "duration": "5.070225" }, "binary_filename": "tests.bin/pointer_copy_user_ctrlflow_bitwise.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/pointer_copy_user_ctrlflow_bitwise.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "Comparison of unspecified value:\n > in main at tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bitwise.c:14:5\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nConversion from an integer to non-null pointer:\n > in main at tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bitwise.c:19:3\n\n Implementation defined behavior (IMPL-CCV13):\n see C11 section 6.3.2.3:5 http://rvdoc.org/C11/6.3.2.3\n see CERT section INT36-C http://rvdoc.org/CERT/INT36-C\n\n", "exit_code": "139", "signals": "", "start_time": "2018.11.07 3:59:08.792601", "duration": "1.691788" }, "source_hashes": "a660daa3e63c5a264110553469104168 tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bitwise.c\n", "sources": "#include \n#include \n#include \nint x=1;\nint main() {\n int *p = &x;\n uintptr_t i = (uintptr_t)p;\n int uintptr_t_width = sizeof(uintptr_t) * CHAR_BIT;\n uintptr_t bit, j;\n int k;\n j=0;\n for (k=0; k> k;\n if (bit == 1) \n j = j | ((uintptr_t)1 << k);\n else\n j = j;\n }\n int *q = (int *)j;\n *q = 11; // is this free of undefined behaviour?\n printf(\"*p=%d *q=%d\\n\",*p,*q); \n}\n" }, { "test_recipe": { "test_instance_name": "provenance_equality_uintptr_t_global_xy.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_uintptr_t_global_xy.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_uintptr_t_global_xy.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_equality_uintptr_t_global_xy.c.kcc-1.0.out tests/de_facto_memory_model/provenance_equality_uintptr_t_global_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:59:11.045676", "duration": "4.895707" }, "binary_filename": "tests.bin/provenance_equality_uintptr_t_global_xy.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_uintptr_t_global_xy.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0 q=0\n(p==q) = true\n", "stderr": "Printing an unspecified value:\n > in printf at tests/de_facto_memory_model/provenance_equality_uintptr_t_global_xy.c:7:3\n in main at tests/de_facto_memory_model/provenance_equality_uintptr_t_global_xy.c:7:3\n\n Unspecified value or behavior (USP-STDIO2):\n see C11 section 7.21.6.1:8 http://rvdoc.org/C11/7.21.6.1\n\nComparison of unspecified value:\n > in main at tests/de_facto_memory_model/provenance_equality_uintptr_t_global_xy.c:11:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:59:15.941490", "duration": "0.390211" }, "source_hashes": "7ab2ec61753e582b0cfd9363f5988c38 tests/de_facto_memory_model/provenance_equality_uintptr_t_global_xy.c\n", "sources": "#include \n#include \nint x=1, y=2;\nint main() {\n uintptr_t p = (uintptr_t)(&x + 1);\n uintptr_t q = (uintptr_t)&y;\n printf(\"Addresses: p=%\" PRIxPTR \" q=%\" PRIxPTR \"\\n\",\n p,q);\n _Bool b = (p==q);\n // can this be false even with identical addresses?\n printf(\"(p==q) = %s\\n\", b?\"true\":\"false\");\n return 0;\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_equality_uintptr_t_global_yx.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_uintptr_t_global_yx.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_uintptr_t_global_yx.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_equality_uintptr_t_global_yx.c.kcc-1.0.out tests/de_facto_memory_model/provenance_equality_uintptr_t_global_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:59:16.878489", "duration": "4.869192" }, "binary_filename": "tests.bin/provenance_equality_uintptr_t_global_yx.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_uintptr_t_global_yx.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0 q=0\n(p==q) = true\n", "stderr": "Printing an unspecified value:\n > in printf at tests/de_facto_memory_model/provenance_equality_uintptr_t_global_yx.c:7:3\n in main at tests/de_facto_memory_model/provenance_equality_uintptr_t_global_yx.c:7:3\n\n Unspecified value or behavior (USP-STDIO2):\n see C11 section 7.21.6.1:8 http://rvdoc.org/C11/7.21.6.1\n\nComparison of unspecified value:\n > in main at tests/de_facto_memory_model/provenance_equality_uintptr_t_global_yx.c:11:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:59:21.747773", "duration": "0.531865" }, "source_hashes": "4098227ab8032c721d214670745bd780 tests/de_facto_memory_model/provenance_equality_uintptr_t_global_yx.c\n", "sources": "#include \n#include \nint y=2, x=1;\nint main() {\n uintptr_t p = (uintptr_t)(&x + 1);\n uintptr_t q = (uintptr_t)&y;\n printf(\"Addresses: p=%\" PRIxPTR \" q=%\" PRIxPTR \"\\n\",\n p,q);\n _Bool b = (p==q);\n // can this be false even with identical addresses?\n printf(\"(p==q) = %s\\n\", b?\"true\":\"false\");\n return 0;\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_equality_uintptr_t_auto_xy.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_uintptr_t_auto_xy.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_uintptr_t_auto_xy.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_equality_uintptr_t_auto_xy.c.kcc-1.0.out tests/de_facto_memory_model/provenance_equality_uintptr_t_auto_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:59:22.834219", "duration": "4.829730" }, "binary_filename": "tests.bin/provenance_equality_uintptr_t_auto_xy.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_uintptr_t_auto_xy.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0 q=0\n(p==q) = true\n", "stderr": "Printing an unspecified value:\n > in printf at tests/de_facto_memory_model/provenance_equality_uintptr_t_auto_xy.c:7:3\n in main at tests/de_facto_memory_model/provenance_equality_uintptr_t_auto_xy.c:7:3\n\n Unspecified value or behavior (USP-STDIO2):\n see C11 section 7.21.6.1:8 http://rvdoc.org/C11/7.21.6.1\n\nComparison of unspecified value:\n > in main at tests/de_facto_memory_model/provenance_equality_uintptr_t_auto_xy.c:11:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:59:27.664054", "duration": "0.390399" }, "source_hashes": "7650d085a5c01ec2b5ca944f09d84421 tests/de_facto_memory_model/provenance_equality_uintptr_t_auto_xy.c\n", "sources": "#include \n#include \nint main() {\n int x=1, y=2;\n uintptr_t p = (uintptr_t)(&x + 1);\n uintptr_t q = (uintptr_t)&y;\n printf(\"Addresses: p=%\" PRIxPTR \" q=%\" PRIxPTR \"\\n\",\n p,q);\n _Bool b = (p==q);\n // can this be false even with identical addresses?\n printf(\"(p==q) = %s\\n\", b?\"true\":\"false\");\n return 0;\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_equality_uintptr_t_auto_yx.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_uintptr_t_auto_yx.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_uintptr_t_auto_yx.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_equality_uintptr_t_auto_yx.c.kcc-1.0.out tests/de_facto_memory_model/provenance_equality_uintptr_t_auto_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:59:28.600318", "duration": "4.808306" }, "binary_filename": "tests.bin/provenance_equality_uintptr_t_auto_yx.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_uintptr_t_auto_yx.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0 q=0\n(p==q) = true\n", "stderr": "Printing an unspecified value:\n > in printf at tests/de_facto_memory_model/provenance_equality_uintptr_t_auto_yx.c:7:3\n in main at tests/de_facto_memory_model/provenance_equality_uintptr_t_auto_yx.c:7:3\n\n Unspecified value or behavior (USP-STDIO2):\n see C11 section 7.21.6.1:8 http://rvdoc.org/C11/7.21.6.1\n\nComparison of unspecified value:\n > in main at tests/de_facto_memory_model/provenance_equality_uintptr_t_auto_yx.c:11:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:59:33.408718", "duration": "0.389243" }, "source_hashes": "133d0b865fdea02e8fb70047d2e5f5d2 tests/de_facto_memory_model/provenance_equality_uintptr_t_auto_yx.c\n", "sources": "#include \n#include \nint main() {\n int y=2, x=1;\n uintptr_t p = (uintptr_t)(&x + 1);\n uintptr_t q = (uintptr_t)&y;\n printf(\"Addresses: p=%\" PRIxPTR \" q=%\" PRIxPTR \"\\n\",\n p,q);\n _Bool b = (p==q);\n // can this be false even with identical addresses?\n printf(\"(p==q) = %s\\n\", b?\"true\":\"false\");\n return 0;\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_union_punning_2_global_xy.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_union_punning_2_global_xy.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_union_punning_2_global_xy.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_union_punning_2_global_xy.c.kcc-1.0.out tests/de_facto_memory_model/provenance_union_punning_2_global_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:59:34.347036", "duration": "5.042127" }, "binary_filename": "tests.bin/provenance_union_punning_2_global_xy.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_union_punning_2_global_xy.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(nil) q=(nil)\nx=1 y=2 *p=0 *q=2\n", "stderr": "Comparison of unspecified value:\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:180:13\n in main at tests/de_facto_memory_model/provenance_union_punning_2_global_xy.c:15:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_union_punning_2_global_xy.c:16:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nTrying to write outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_union_punning_2_global_xy.c:16:5\n\n Undefined behavior (UB-EIO2):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section MEM35-C http://rvdoc.org/CERT-C/MEM35-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_union_punning_2_global_xy.c:17:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nReading outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_union_punning_2_global_xy.c:17:5\n\n Undefined behavior (UB-EIO7):\n see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1\n see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see CERT-C section STR32-C http://rvdoc.org/CERT-C/STR32-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:59:39.389266", "duration": "0.561221" }, "source_hashes": "5642ebdcc8bbcdce9e7943725187d7ba tests/de_facto_memory_model/provenance_union_punning_2_global_xy.c\n", "sources": "#include \n#include \n#include \nint x=1, y=2;\ntypedef union { uintptr_t ui; int *p; } un;\nint main() {\n un u; \n int *px = &x;\n uintptr_t i = (uintptr_t)px;\n i = i + sizeof(int);\n u.ui = i;\n int *p = u.p;\n int *q = &y;\n printf(\"Addresses: p=%p q=%p\\n\",(void*)p,(void*)q);\n if (memcmp(&p, &q, sizeof(p)) == 0) {\n *p = 11; // does this have undefined behaviour?\n printf(\"x=%d y=%d *p=%d *q=%d\\n\",x,y,*p,*q);\n }\n return 0;\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_union_punning_2_global_yx.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_union_punning_2_global_yx.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_union_punning_2_global_yx.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_union_punning_2_global_yx.c.kcc-1.0.out tests/de_facto_memory_model/provenance_union_punning_2_global_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:59:40.493736", "duration": "5.136099" }, "binary_filename": "tests.bin/provenance_union_punning_2_global_yx.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_union_punning_2_global_yx.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(nil) q=(nil)\nx=1 y=2 *p=0 *q=2\n", "stderr": "Comparison of unspecified value:\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:180:13\n in main at tests/de_facto_memory_model/provenance_union_punning_2_global_yx.c:15:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_union_punning_2_global_yx.c:16:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nTrying to write outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_union_punning_2_global_yx.c:16:5\n\n Undefined behavior (UB-EIO2):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section MEM35-C http://rvdoc.org/CERT-C/MEM35-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_union_punning_2_global_yx.c:17:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nReading outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_union_punning_2_global_yx.c:17:5\n\n Undefined behavior (UB-EIO7):\n see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1\n see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see CERT-C section STR32-C http://rvdoc.org/CERT-C/STR32-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:59:45.630013", "duration": "0.603412" }, "source_hashes": "3be5ef318742ac61bdcd4cc145739220 tests/de_facto_memory_model/provenance_union_punning_2_global_yx.c\n", "sources": "#include \n#include \n#include \nint y=2, x=1;\ntypedef union { uintptr_t ui; int *p; } un;\nint main() {\n un u; \n int *px = &x;\n uintptr_t i = (uintptr_t)px;\n i = i + sizeof(int);\n u.ui = i;\n int *p = u.p;\n int *q = &y;\n printf(\"Addresses: p=%p q=%p\\n\",(void*)p,(void*)q);\n if (memcmp(&p, &q, sizeof(p)) == 0) {\n *p = 11; // does this have undefined behaviour?\n printf(\"x=%d y=%d *p=%d *q=%d\\n\",x,y,*p,*q);\n }\n return 0;\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_union_punning_2_auto_xy.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_union_punning_2_auto_xy.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_union_punning_2_auto_xy.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_union_punning_2_auto_xy.c.kcc-1.0.out tests/de_facto_memory_model/provenance_union_punning_2_auto_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:59:46.778185", "duration": "5.022840" }, "binary_filename": "tests.bin/provenance_union_punning_2_auto_xy.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_union_punning_2_auto_xy.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(nil) q=(nil)\nx=1 y=2 *p=0 *q=2\n", "stderr": "Comparison of unspecified value:\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:180:13\n in main at tests/de_facto_memory_model/provenance_union_punning_2_auto_xy.c:15:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_union_punning_2_auto_xy.c:16:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nTrying to write outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_union_punning_2_auto_xy.c:16:5\n\n Undefined behavior (UB-EIO2):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section MEM35-C http://rvdoc.org/CERT-C/MEM35-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_union_punning_2_auto_xy.c:17:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nReading outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_union_punning_2_auto_xy.c:17:5\n\n Undefined behavior (UB-EIO7):\n see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1\n see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see CERT-C section STR32-C http://rvdoc.org/CERT-C/STR32-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:59:51.801119", "duration": "0.478638" }, "source_hashes": "5642ebdcc8bbcdce9e7943725187d7ba tests/de_facto_memory_model/provenance_union_punning_2_auto_xy.c\n", "sources": "#include \n#include \n#include \nint x=1, y=2;\ntypedef union { uintptr_t ui; int *p; } un;\nint main() {\n un u; \n int *px = &x;\n uintptr_t i = (uintptr_t)px;\n i = i + sizeof(int);\n u.ui = i;\n int *p = u.p;\n int *q = &y;\n printf(\"Addresses: p=%p q=%p\\n\",(void*)p,(void*)q);\n if (memcmp(&p, &q, sizeof(p)) == 0) {\n *p = 11; // does this have undefined behaviour?\n printf(\"x=%d y=%d *p=%d *q=%d\\n\",x,y,*p,*q);\n }\n return 0;\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_union_punning_2_auto_yx.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_union_punning_2_auto_yx.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_union_punning_2_auto_yx.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_union_punning_2_auto_yx.c.kcc-1.0.out tests/de_facto_memory_model/provenance_union_punning_2_auto_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:59:52.827784", "duration": "4.894097" }, "binary_filename": "tests.bin/provenance_union_punning_2_auto_yx.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_union_punning_2_auto_yx.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(nil) q=(nil)\nx=1 y=2 *p=0 *q=2\n", "stderr": "Comparison of unspecified value:\n > in memcmp at /opt/rv-match/c-semantics/profiles/x86_64-linux-gcc-glibc/src/string.c:180:13\n in main at tests/de_facto_memory_model/provenance_union_punning_2_auto_yx.c:15:3\n\n Unspecified value or behavior (USP-CERL7):\n see C11 section 6.5.9 http://rvdoc.org/C11/6.5.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_union_punning_2_auto_yx.c:16:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nTrying to write outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_union_punning_2_auto_yx.c:16:5\n\n Undefined behavior (UB-EIO2):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section MEM35-C http://rvdoc.org/CERT-C/MEM35-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nDereferencing a pointer past the end of an array:\n > in main at tests/de_facto_memory_model/provenance_union_punning_2_auto_yx.c:17:5\n\n Undefined behavior (UB-CER4):\n see C11 section 6.5.6:8 http://rvdoc.org/C11/6.5.6\n see C11 section J.2:1 items 47 and 49 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see MISRA-C section 8.18:1 http://rvdoc.org/MISRA-C/8.18\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nReading outside the bounds of an object:\n > in main at tests/de_facto_memory_model/provenance_union_punning_2_auto_yx.c:17:5\n\n Undefined behavior (UB-EIO7):\n see C11 section 6.3.2.1:1 http://rvdoc.org/C11/6.3.2.1\n see C11 section J.2:1 item 19 http://rvdoc.org/C11/J.2\n see CERT-C section ARR30-C http://rvdoc.org/CERT-C/ARR30-C\n see CERT-C section ARR37-C http://rvdoc.org/CERT-C/ARR37-C\n see CERT-C section STR31-C http://rvdoc.org/CERT-C/STR31-C\n see CERT-C section STR32-C http://rvdoc.org/CERT-C/STR32-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nIndeterminate value used in an expression:\n > in main at tests/de_facto_memory_model/provenance_union_punning_2_auto_yx.c:17:5\n\n Undefined behavior (UB-CEE2):\n see C11 section 6.2.4 http://rvdoc.org/C11/6.2.4\n see C11 section 6.7.9 http://rvdoc.org/C11/6.7.9\n see C11 section 6.8 http://rvdoc.org/C11/6.8\n see C11 section J.2:1 item 11 http://rvdoc.org/C11/J.2\n see CERT-C section EXP33-C http://rvdoc.org/CERT-C/EXP33-C\n see MISRA-C section 8.9:1 http://rvdoc.org/MISRA-C/8.9\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:59:57.721976", "duration": "0.490208" }, "source_hashes": "e8e626364c705b927bd9c68e137a4434 tests/de_facto_memory_model/provenance_union_punning_2_auto_yx.c\n", "sources": "#include \n#include \n#include \ntypedef union { uintptr_t ui; int *p; } un;\nint main() {\n int y=2, x=1;\n un u; \n int *px = &x;\n uintptr_t i = (uintptr_t)px;\n i = i + sizeof(int);\n u.ui = i;\n int *p = u.p;\n int *q = &y;\n printf(\"Addresses: p=%p q=%p\\n\",(void*)p,(void*)q);\n if (memcmp(&p, &q, sizeof(p)) == 0) {\n *p = 11; // does this have undefined behaviour?\n printf(\"x=%d y=%d *p=%d *q=%d\\n\",x,y,*p,*q);\n }\n return 0;\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_via_io_percentp_global.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_via_io_percentp_global.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_via_io_percentp_global.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_via_io_percentp_global.c.kcc-1.0.out tests/de_facto_memory_model/provenance_via_io_percentp_global.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 3:59:58.762844", "duration": "5.814453" }, "binary_filename": "tests.bin/provenance_via_io_percentp_global.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_via_io_percentp_global.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(nil)\nAddresses: r=(nil)\n", "stderr": "Dereferencing a null pointer:\n > in main at tests/de_facto_memory_model/provenance_via_io_percentp_global.c:20:3\n\n Undefined behavior (UB-CER3):\n see C11 section 6.5.3.2:4 http://rvdoc.org/C11/6.5.3.2\n see C11 section J.2:1 item 43 http://rvdoc.org/C11/J.2\n see CERT-C section EXP34-C http://rvdoc.org/CERT-C/EXP34-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nExecution failed (configuration dumped)\n", "exit_code": "139", "signals": "", "start_time": "2018.11.07 4:00:04.577390", "duration": "1.281640" }, "source_hashes": "5cbe3d65ac16f5cccd2e1067e040627d tests/de_facto_memory_model/provenance_via_io_percentp_global.c\n", "sources": "#include \n#include \n#include \n#include \nint x=1;\nint main() {\n int *p = &x;\n FILE *f = fopen(\n \"provenance_via_io_percentp_global.tmp\",\"w+b\");\n printf(\"Addresses: p=%p\\n\",(void*)p);\n // print pointer address to a file\n fprintf(f,\"%p\\n\",(void*)p);\n rewind(f);\n void *rv;\n int n = fscanf(f,\"%p\\n\",&rv);\n int *r = (int *)rv;\n if (n != 1) exit(EXIT_FAILURE);\n printf(\"Addresses: r=%p\\n\",(void*)r);\n // are r and p now equivalent? \n *r=12; // is this free of undefined behaviour? \n _Bool b1 = (r==p); // do they compare equal? \n _Bool b2 = (0==memcmp(&r,&p,sizeof(r)));//same reps?\n printf(\"x=%i *r=%i b1=%s b2=%s\\n\",x,*r,\n b1?\"true\":\"false\",b2?\"true\":\"false\");\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_via_io_bytewise_global.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_via_io_bytewise_global.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_via_io_bytewise_global.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_via_io_bytewise_global.c.kcc-1.0.out tests/de_facto_memory_model/provenance_via_io_bytewise_global.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 4:00:06.410375", "duration": "5.731383" }, "binary_filename": "tests.bin/provenance_via_io_bytewise_global.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_via_io_bytewise_global.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(nil)\nAddresses: r=(nil)\n", "stderr": "Dereferencing a null pointer:\n > in main at tests/de_facto_memory_model/provenance_via_io_bytewise_global.c:20:3\n\n Undefined behavior (UB-CER3):\n see C11 section 6.5.3.2:4 http://rvdoc.org/C11/6.5.3.2\n see C11 section J.2:1 item 43 http://rvdoc.org/C11/J.2\n see CERT-C section EXP34-C http://rvdoc.org/CERT-C/EXP34-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nExecution failed (configuration dumped)\n", "exit_code": "139", "signals": "", "start_time": "2018.11.07 4:00:12.141852", "duration": "1.096369" }, "source_hashes": "ce774c57d04dfb99dcc7a555aa99d291 tests/de_facto_memory_model/provenance_via_io_bytewise_global.c\n", "sources": "#include \n#include \n#include \n#include \nint x=1;\nint main() {\n int *p = &x;\n FILE *f = fopen(\n \"provenance_via_io_bytewise_global.tmp\",\"w+b\");\n printf(\"Addresses: p=%p\\n\",(void*)p);\n // output pointer address to a file\n int nw = fwrite(&p, 1, sizeof(int *), f);\n if (nw != sizeof(int *)) exit(EXIT_FAILURE); \n rewind(f);\n int *r;\n int nr = fread(&r, 1, sizeof(int *), f);\n if (nr != sizeof(int *)) exit(EXIT_FAILURE); \n printf(\"Addresses: r=%p\\n\",(void*)r);\n // are r and p now equivalent? \n *r=12; // is this free of undefined behaviour? \n _Bool b1 = (r==p); // do they compare equal? \n _Bool b2 = (0==memcmp(&r,&p,sizeof(r)));//same reps?\n printf(\"x=%i *r=%i b1=%s b2=%s\\n\",x,*r,\n b1?\"true\":\"false\",b2?\"true\":\"false\");\n}\n" }, { "test_recipe": { "test_instance_name": "provenance_via_io_uintptr_t_global.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_via_io_uintptr_t_global.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_via_io_uintptr_t_global.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/provenance_via_io_uintptr_t_global.c.kcc-1.0.out tests/de_facto_memory_model/provenance_via_io_uintptr_t_global.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 4:00:13.782183", "duration": "5.820220" }, "binary_filename": "tests.bin/provenance_via_io_uintptr_t_global.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/provenance_via_io_uintptr_t_global.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: i=0 \nAddresses: k=0\n", "stderr": "Printing an unspecified value:\n > in printf at tests/de_facto_memory_model/provenance_via_io_uintptr_t_global.c:11:3\n in main at tests/de_facto_memory_model/provenance_via_io_uintptr_t_global.c:11:3\n\n Unspecified value or behavior (USP-STDIO2):\n see C11 section 7.21.6.1:8 http://rvdoc.org/C11/7.21.6.1\n\nPrinting an unspecified value:\n > in fprintf at tests/de_facto_memory_model/provenance_via_io_uintptr_t_global.c:13:3\n in main at tests/de_facto_memory_model/provenance_via_io_uintptr_t_global.c:13:3\n\n Unspecified value or behavior (USP-STDIO2):\n see C11 section 7.21.6.1:8 http://rvdoc.org/C11/7.21.6.1\n\nConversion from an integer to non-null pointer:\n > in main at tests/de_facto_memory_model/provenance_via_io_uintptr_t_global.c:20:3\n\n Implementation defined behavior (IMPL-CCV13):\n see C11 section 6.3.2.3:5 http://rvdoc.org/C11/6.3.2.3\n see CERT section INT36-C http://rvdoc.org/CERT/INT36-C\n\nDereferencing a null pointer:\n > in main at tests/de_facto_memory_model/provenance_via_io_uintptr_t_global.c:22:3\n\n Undefined behavior (UB-CER3):\n see C11 section 6.5.3.2:4 http://rvdoc.org/C11/6.5.3.2\n see C11 section J.2:1 item 43 http://rvdoc.org/C11/J.2\n see CERT-C section EXP34-C http://rvdoc.org/CERT-C/EXP34-C\n see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1\n\nExecution failed (configuration dumped)\n", "exit_code": "139", "signals": "", "start_time": "2018.11.07 4:00:19.602584", "duration": "0.922755" }, "source_hashes": "98a9109cddab0d5103de66f8f0be8d02 tests/de_facto_memory_model/provenance_via_io_uintptr_t_global.c\n", "sources": "#include \n#include \n#include \n#include \nint x=1;\nint main() {\n int *p = &x;\n uintptr_t i = (uintptr_t) p;\n FILE *f = fopen(\n \"provenance_via_io_uintptr_t_global.tmp\",\"w+b\");\n printf(\"Addresses: i=%\"PRIuPTR\" \\n\",i);\n // print pointer address to a file\n fprintf(f,\"%\"PRIuPTR\"\\n\",i);\n rewind(f);\n uintptr_t k;\n // read a pointer address from the file\n int n = fscanf(f,\"%\"SCNuPTR\"\\n\",&k);\n if (n != 1) exit(EXIT_FAILURE);\n printf(\"Addresses: k=%\"PRIuPTR\"\\n\",k);\n int *r = (int *)k;\n // are r and q now equivalent? \n *r=12; // is this free of undefined behaviour? \n _Bool b1 = (r==p); // do they compare equal? \n _Bool b2 = (0==memcmp(&r,&p,sizeof(r)));//same reps?\n printf(\"x=%i *r=%i b1=%s b2=%s\\n\",x,*r,\n b1?\"true\":\"false\",b2?\"true\":\"false\");\n}\n" }, { "test_recipe": { "test_instance_name": "init.c.kcc-1.0", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "init.c" }, "tool": { "tool_name": "kcc", "tool_args": "-DKCC", "tool_instance_name": "kcc-1.0", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "init.c", "tool_version": "", "compile_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "compile_output": { "command": "LANG=C kcc -DKCC -o tests.bin/init.c.kcc-1.0.out tests/de_facto_memory_model/init.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "tests/de_facto_memory_model/init.c:10:1: error: Encountered an unknown error. This may be due to encountering undefined behavior, an unsupported language feature, or a bug in this tool.\n\n Unknown error (UNK-1)\n\nFatal error: exception Stack overflow\nTranslation failed (kcc_config dumped). To repeat, run this command in directory charon2:\nkcc -d -DKCC -o tests.bin/init.c.kcc-1.0.out tests/de_facto_memory_model/init.c\n", "exit_code": "2", "signals": "", "start_time": "2018.11.07 4:00:21.079277", "duration": "110.781511" }, "binary_filename": "tests.bin/init.c.kcc-1.0.out", "execute_host": { "host_name": "simurgh", "host_os": "Linux", "host_os_version": "3.14.32-xxxx-grs-ipv6-64 #7 SMP Wed Jan 27 18:05:09 CET 2016", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Atom(TM) CPU N2800 @ 1.86GHz" }, "execute_output": { "command": "tests.bin/init.c.kcc-1.0.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "sh: tests.bin/init.c.kcc-1.0.out: No such file or directory\n", "exit_code": "127", "signals": "", "start_time": "2018.11.07 4:02:11.860940", "duration": "0.009099" }, "source_hashes": "000be3b18c0a17b0b100dfd4f98815ec tests/de_facto_memory_model/init.c\n", "sources": "struct T {\n int x;\n struct T2 {\n int y[2];\n char z;\n } st;\n char c[3];\n};\n\nstruct T arr1[3] =\n { 1, {{2,3,40,50}, 6,\n {\"foo\"}}, [2].st.z= 7};\n" } ]