From cd395348fd3de2da7b328eb9cbfcbcaede3fb5c9 Mon Sep 17 00:00:00 2001 From: Nat Karmios Date: Sun, 14 Jan 2024 17:04:40 +0000 Subject: [PATCH] WIP --- for_test.c | 5 + for_test.c.symtab.json | 8217 +++++++++++++++++++ kanillian/lib/compiler/compile_expr.ml | 81 +- kanillian/lib/goto_program/dune | 2 +- kanillian/lib/goto_program/expr_and_stmt.ml | 36 +- kanillian/lib/goto_program/goto_lib.mli | 7 +- kanillian/lib/goto_program/ops.ml | 16 + kanillian/lib/goto_program/visitors.ml | 12 +- kanillian/lib/lifter/kani_c_lifter.ml | 58 +- while_test.c | 8 + while_test.c.symtab.json | 898 ++ 11 files changed, 9289 insertions(+), 51 deletions(-) create mode 100644 for_test.c create mode 100644 for_test.c.symtab.json create mode 100644 while_test.c create mode 100644 while_test.c.symtab.json diff --git a/for_test.c b/for_test.c new file mode 100644 index 00000000..77eae987 --- /dev/null +++ b/for_test.c @@ -0,0 +1,5 @@ +int main() { + for (int i = 0; i < 10; i++) + printf("%d\n", i); + return 0; +} diff --git a/for_test.c.symtab.json b/for_test.c.symtab.json new file mode 100644 index 00000000..697b3923 --- /dev/null +++ b/for_test.c.symtab.json @@ -0,0 +1,8217 @@ +[ + { + "program": "CBMC 5.12 (cbmc-5.12)" + }, + { + "messageText": "CBMC version 5.12 (cbmc-5.12) 64-bit x86_64 linux", + "messageType": "STATUS-MESSAGE" + }, + { + "messageText": "Parsing for_test.c", + "messageType": "STATUS-MESSAGE" + }, + { + "messageText": "Converting", + "messageType": "STATUS-MESSAGE" + }, + { + "messageText": "Type-checking for_test", + "messageType": "STATUS-MESSAGE" + }, + { + "messageText": "function 'printf' is not declared", + "messageType": "WARNING", + "sourceLocation": { + "file": "for_test.c", + "function": "main", + "line": "3", + "workingDirectory": "/home/nat/code/Gillian" + } + }, + { + "messageText": "Generating GOTO Program", + "messageType": "STATUS-MESSAGE" + }, + { + "symbolTable": { + "__CPROVER__start": { + "baseName": "", + "isAuxiliary": true, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": false, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "nil" + }, + "mode": "C", + "module": "", + "name": "__CPROVER__start", + "prettyName": "", + "prettyType": "void (void)", + "prettyValue": "{\n\n__CPROVER_HIDE:\n ;\n __CPROVER_initialize();\n return'=main();\n OUTPUT(\"return'\", return');\n}", + "type": { + "id": "code", + "namedSub": { + "parameters": { + "id": "" + }, + "return_type": { + "id": "empty" + } + } + }, + "value": { + "id": "code", + "namedSub": { + "statement": { + "id": "block" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "label": { + "id": "__CPROVER_HIDE" + }, + "statement": { + "id": "label" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "statement": { + "id": "skip" + }, + "type": { + "id": "empty" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "function_call" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "nil" + }, + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "__CPROVER_initialize" + }, + "type": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "35" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "parameters": { + "id": "" + }, + "return_type": { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "35" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + } + } + } + }, + { + "id": "arguments" + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "function_call" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "return'" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "identifier": { + "id": "main" + }, + "type": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "parameters": { + "id": "", + "namedSub": { + "ellipsis": { + "id": "1" + } + } + }, + "return_type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + } + }, + { + "id": "arguments" + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "output" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "address_of", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + ] + } + }, + "sub": [ + { + "id": "index", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + }, + "sub": [ + { + "id": "string_constant", + "namedSub": { + "type": { + "id": "array", + "namedSub": { + "size": { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "8" + } + } + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + ] + }, + "value": { + "id": "return'" + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + ] + }, + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "return'" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + ] + } + ] + } + }, + "main::1::1::i": { + "baseName": "i", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": true, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "main::1::1::i", + "prettyName": "main::1::1::i", + "prettyType": "signed int", + "prettyValue": "0", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + }, + "__CPROVER_architecture_NULL_is_zero": { + "baseName": "__CPROVER_architecture_NULL_is_zero", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_architecture_NULL_is_zero", + "prettyName": "__CPROVER_architecture_NULL_is_zero", + "prettyType": "const signed int", + "prettyValue": "1", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "1" + } + } + } + }, + "__CPROVER_architecture_os": { + "baseName": "__CPROVER_architecture_os", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "19" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_architecture_os", + "prettyName": "__CPROVER_architecture_os", + "prettyType": "const char *", + "prettyValue": "\"linux\"", + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "19" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "8" + } + } + } + ] + }, + "value": { + "id": "address_of", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + ] + } + }, + "sub": [ + { + "id": "index", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + }, + "sub": [ + { + "id": "string_constant", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "19" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "array", + "namedSub": { + "size": { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "6" + } + } + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + ] + }, + "value": { + "id": "linux" + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + ] + } + }, + "__CPROVER_architecture_arch": { + "baseName": "__CPROVER_architecture_arch", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "18" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_architecture_arch", + "prettyName": "__CPROVER_architecture_arch", + "prettyType": "const char *", + "prettyValue": "\"x86_64\"", + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "18" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "8" + } + } + } + ] + }, + "value": { + "id": "address_of", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + ] + } + }, + "sub": [ + { + "id": "index", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + }, + "sub": [ + { + "id": "string_constant", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "18" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "array", + "namedSub": { + "size": { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "7" + } + } + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + ] + }, + "value": { + "id": "x86_64" + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + ] + } + }, + "__CPROVER_architecture_alignment": { + "baseName": "__CPROVER_architecture_alignment", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "15" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_architecture_alignment", + "prettyName": "__CPROVER_architecture_alignment", + "prettyType": "const signed int", + "prettyValue": "1", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "15" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "1" + } + } + } + }, + "__CPROVER_architecture_wchar_t_is_unsigned": { + "baseName": "__CPROVER_architecture_wchar_t_is_unsigned", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "14" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_architecture_wchar_t_is_unsigned", + "prettyName": "__CPROVER_architecture_wchar_t_is_unsigned", + "prettyType": "const signed int", + "prettyValue": "0", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "14" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + }, + "__CPROVER_architecture_char_is_unsigned": { + "baseName": "__CPROVER_architecture_char_is_unsigned", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "13" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_architecture_char_is_unsigned", + "prettyName": "__CPROVER_architecture_char_is_unsigned", + "prettyType": "const signed int", + "prettyValue": "0", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "13" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + }, + "__CPROVER_architecture_wchar_t_width": { + "baseName": "__CPROVER_architecture_wchar_t_width", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "12" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_architecture_wchar_t_width", + "prettyName": "__CPROVER_architecture_wchar_t_width", + "prettyType": "const signed int", + "prettyValue": "32", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "12" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "20" + } + } + } + }, + "__CPROVER_architecture_long_double_width": { + "baseName": "__CPROVER_architecture_long_double_width", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "11" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_architecture_long_double_width", + "prettyName": "__CPROVER_architecture_long_double_width", + "prettyType": "const signed int", + "prettyValue": "128", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "11" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "80" + } + } + } + }, + "__CPROVER_architecture_double_width": { + "baseName": "__CPROVER_architecture_double_width", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_architecture_double_width", + "prettyName": "__CPROVER_architecture_double_width", + "prettyType": "const signed int", + "prettyValue": "64", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "40" + } + } + } + }, + "__CPROVER_architecture_single_width": { + "baseName": "__CPROVER_architecture_single_width", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_architecture_single_width", + "prettyName": "__CPROVER_architecture_single_width", + "prettyType": "const signed int", + "prettyValue": "32", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "20" + } + } + } + }, + "__CPROVER_deallocated": { + "baseName": "__CPROVER_deallocated", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "13" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_deallocated", + "prettyName": "__CPROVER_deallocated", + "prettyType": "const void *", + "prettyValue": "NULL", + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "13" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "13" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + }, + "value": { + "id": "constant", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "13" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "13" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + }, + "value": { + "id": "NULL" + } + } + } + }, + "__CPROVER_memory": { + "baseName": "__CPROVER_memory", + "isAuxiliary": false, + "isExported": false, + "isExtern": true, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "12" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_memory", + "prettyName": "__CPROVER_memory", + "prettyType": "unsigned char [INFINITY()]", + "prettyValue": "", + "type": { + "id": "array", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "12" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "size": { + "id": "infinity", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "12" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + } + } + } + }, + "sub": [ + { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_char" + }, + "width": { + "id": "8" + } + } + } + ] + }, + "value": { + "id": "nil" + } + }, + "__CPROVER_next_thread_key": { + "baseName": "__CPROVER_next_thread_key", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "11" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_next_thread_key", + "prettyName": "__CPROVER_next_thread_key", + "prettyType": "unsigned long int", + "prettyValue": "(unsigned long int)0", + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "typecast", + "namedSub": { + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "width": { + "id": "64" + } + } + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "11" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + }, + "__CPROVER_thread_key_dtors": { + "baseName": "__CPROVER_thread_key_dtors", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_thread_key_dtors", + "prettyName": "__CPROVER_thread_key_dtors", + "prettyType": "void (*[INFINITY()])(void *)", + "prettyValue": "", + "type": { + "id": "array", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "size": { + "id": "infinity", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + } + } + } + }, + "sub": [ + { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "parameters": { + "id": "", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + } + } + } + ] + }, + "return_type": { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + } + } + ] + } + ] + }, + "value": { + "id": "nil" + } + }, + "__CPROVER_next_thread_id": { + "baseName": "__CPROVER_next_thread_id", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_next_thread_id", + "prettyName": "__CPROVER_next_thread_id", + "prettyType": "unsigned long int", + "prettyValue": "(unsigned long int)0", + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "typecast", + "namedSub": { + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "width": { + "id": "64" + } + } + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + }, + "__CPROVER_architecture_endianness": { + "baseName": "__CPROVER_architecture_endianness", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "17" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_architecture_endianness", + "prettyName": "__CPROVER_architecture_endianness", + "prettyType": "const signed int", + "prettyValue": "1", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "17" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "1" + } + } + } + }, + "__CPROVER_initialize": { + "baseName": "__CPROVER_initialize", + "isAuxiliary": true, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "35" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_initialize", + "prettyName": "__CPROVER_initialize", + "prettyType": "void (void)", + "prettyValue": "{\n\n__CPROVER_HIDE:\n ;\n __CPROVER_alloca_object = NULL;\n __CPROVER_dead_object = NULL;\n __CPROVER_deallocated = NULL;\n __CPROVER_malloc_is_new_array = 0 != 0;\n __CPROVER_malloc_object = NULL;\n __CPROVER_malloc_size = 0ul;\n __CPROVER_memory_leak = NULL;\n __CPROVER_next_thread_id = (unsigned long int)0;\n __CPROVER_next_thread_key = (unsigned long int)0;\n __CPROVER_pipe_count = (unsigned int)0;\n __CPROVER_rounding_mode = 0;\n __CPROVER_thread_id = (unsigned long int)0;\n __CPROVER_thread_key_dtors = ARRAY_OF(((void (*)(void *))NULL));\n __CPROVER_thread_keys = ARRAY_OF(NULL);\n __CPROVER_threads_exited = ARRAY_OF(FALSE);\n}", + "type": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "35" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "parameters": { + "id": "" + }, + "return_type": { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "35" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + } + }, + "value": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "block" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "label": { + "id": "__CPROVER_HIDE" + }, + "statement": { + "id": "label" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "statement": { + "id": "skip" + }, + "type": { + "id": "empty" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "assign" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "__CPROVER_alloca_object" + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + }, + "value": { + "id": "NULL" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "14" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "assign" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "__CPROVER_dead_object" + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "14" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "14" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "14" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "14" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + }, + "value": { + "id": "NULL" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "13" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "assign" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "__CPROVER_deallocated" + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "13" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "13" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "13" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "13" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + }, + "value": { + "id": "NULL" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "17" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "assign" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "__CPROVER_malloc_is_new_array" + }, + "type": { + "id": "bool" + } + } + }, + { + "id": "notequal", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "17" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "bool" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "17" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "15" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "assign" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "__CPROVER_malloc_object" + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "15" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "15" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "15" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "15" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + }, + "value": { + "id": "NULL" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "16" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "assign" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "__CPROVER_malloc_size" + }, + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "#typedef": { + "id": "__CPROVER_size_t" + }, + "width": { + "id": "64" + } + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "16" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "#typedef": { + "id": "__CPROVER_size_t" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "18" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "assign" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "__CPROVER_memory_leak" + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "18" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "18" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "18" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "18" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + }, + "value": { + "id": "NULL" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "assign" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "__CPROVER_next_thread_id" + }, + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "width": { + "id": "64" + } + } + } + } + }, + { + "id": "typecast", + "namedSub": { + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "width": { + "id": "64" + } + } + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "11" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "assign" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "__CPROVER_next_thread_key" + }, + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "width": { + "id": "64" + } + } + } + } + }, + { + "id": "typecast", + "namedSub": { + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "width": { + "id": "64" + } + } + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "11" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "33" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "assign" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "__CPROVER_pipe_count" + }, + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + { + "id": "typecast", + "namedSub": { + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_int" + }, + "width": { + "id": "32" + } + } + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "33" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "24" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "assign" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "__CPROVER_rounding_mode" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "24" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "6" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "assign" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "__CPROVER_thread_id" + }, + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "width": { + "id": "64" + } + } + } + } + }, + { + "id": "typecast", + "namedSub": { + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "width": { + "id": "64" + } + } + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "6" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "assign" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "__CPROVER_thread_key_dtors" + }, + "type": { + "id": "array", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "size": { + "id": "infinity", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + } + } + } + }, + "sub": [ + { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "parameters": { + "id": "", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + } + } + } + ] + }, + "return_type": { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + } + } + ] + } + ] + } + } + }, + { + "id": "array_of", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "array", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "size": { + "id": "infinity", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + } + } + } + }, + "sub": [ + { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "parameters": { + "id": "", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + } + } + } + ] + }, + "return_type": { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + } + } + ] + } + ] + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "parameters": { + "id": "", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + } + } + } + ] + }, + "return_type": { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + } + } + ] + }, + "value": { + "id": "NULL" + } + } + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "assign" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "__CPROVER_thread_keys" + }, + "type": { + "id": "array", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "size": { + "id": "infinity", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + } + } + } + }, + "sub": [ + { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + } + ] + } + } + }, + { + "id": "array_of", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "array", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "size": { + "id": "infinity", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + } + } + } + }, + "sub": [ + { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + } + ] + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + }, + "value": { + "id": "NULL" + } + } + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "assign" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "__CPROVER_threads_exited" + }, + "type": { + "id": "array", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "size": { + "id": "infinity", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + } + } + } + }, + "sub": [ + { + "id": "bool" + } + ] + } + } + }, + { + "id": "array_of", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "array", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "size": { + "id": "infinity", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + } + } + } + }, + "sub": [ + { + "id": "bool" + } + ] + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "bool" + }, + "value": { + "id": "false" + } + } + } + ] + } + ] + } + ] + } + }, + "return'": { + "baseName": "return'", + "isAuxiliary": true, + "isExported": false, + "isExtern": false, + "isFileLocal": true, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": true, + "isStaticLifetime": false, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "nil" + }, + "mode": "C", + "module": "", + "name": "return'", + "prettyName": "", + "prettyType": "signed int", + "prettyValue": "", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "nil" + } + }, + "__CPROVER_threads_exited": { + "baseName": "__CPROVER_threads_exited", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_threads_exited", + "prettyName": "__CPROVER_threads_exited", + "prettyType": "__CPROVER_bool [INFINITY()]", + "prettyValue": "", + "type": { + "id": "array", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "size": { + "id": "infinity", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + } + } + } + }, + "sub": [ + { + "id": "bool" + } + ] + }, + "value": { + "id": "nil" + } + }, + "__CPROVER_architecture_memory_operand_size": { + "baseName": "__CPROVER_architecture_memory_operand_size", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "16" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_architecture_memory_operand_size", + "prettyName": "__CPROVER_architecture_memory_operand_size", + "prettyType": "const signed int", + "prettyValue": "4", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "16" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "4" + } + } + } + }, + "__CPROVER_pipe_count": { + "baseName": "__CPROVER_pipe_count", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "33" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_pipe_count", + "prettyName": "__CPROVER_pipe_count", + "prettyType": "unsigned int", + "prettyValue": "(unsigned int)0", + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "typecast", + "namedSub": { + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_int" + }, + "width": { + "id": "32" + } + } + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "33" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + }, + "__CPROVER_thread_id": { + "baseName": "__CPROVER_thread_id", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "6" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_thread_id", + "prettyName": "__CPROVER_thread_id", + "prettyType": "unsigned long int", + "prettyValue": "(unsigned long int)0", + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "typecast", + "namedSub": { + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "width": { + "id": "64" + } + } + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "6" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + }, + "__CPROVER_dead_object": { + "baseName": "__CPROVER_dead_object", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "14" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_dead_object", + "prettyName": "__CPROVER_dead_object", + "prettyType": "const void *", + "prettyValue": "NULL", + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "14" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "14" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + }, + "value": { + "id": "constant", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "14" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "14" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + }, + "value": { + "id": "NULL" + } + } + } + }, + "main": { + "baseName": "main", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "main", + "prettyName": "main", + "prettyType": "signed int ()", + "prettyValue": "{\n {\n signed int i=0;\n for( ; i < 10; i++)\n printf((const void *)\"%d\\n\", i);\n }\n return 0;\n}", + "type": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "parameters": { + "id": "", + "namedSub": { + "ellipsis": { + "id": "1" + } + } + }, + "return_type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + "value": { + "id": "code", + "namedSub": { + "#end_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "5" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "block" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#end_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "block" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "decl" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "identifier": { + "id": "main::1::1::i" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "for" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "nil" + }, + { + "id": "<", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "bool" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "identifier": { + "id": "main::1::1::i" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "A" + } + } + } + ] + }, + { + "id": "side_effect", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "postincrement" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "identifier": { + "id": "main::1::1::i" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "expression" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "side_effect", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "function_call" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "identifier": { + "id": "printf" + }, + "type": { + "id": "code", + "namedSub": { + "#incomplete": { + "id": "1" + }, + "parameters": { + "id": "" + }, + "return_type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + } + }, + { + "id": "arguments", + "sub": [ + { + "id": "typecast", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + } + } + } + ] + } + }, + "sub": [ + { + "id": "address_of", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + ] + } + }, + "sub": [ + { + "id": "index", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + }, + "sub": [ + { + "id": "string_constant", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "array", + "namedSub": { + "size": { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "4" + } + } + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + ] + }, + "value": { + "id": "%d\n" + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + ] + } + ] + }, + { + "id": "symbol", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "identifier": { + "id": "main::1::1::i" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + ] + } + ] + } + ] + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "4" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "return" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "4" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + ] + } + }, + "__CPROVER_size_t": { + "baseName": "__CPROVER_size_t", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": true, + "isInput": false, + "isLvalue": false, + "isMacro": true, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": true, + "isType": true, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_size_t", + "prettyName": "__CPROVER_size_t", + "prettyType": "__CPROVER_size_t", + "prettyValue": "", + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "#typedef": { + "id": "__CPROVER_size_t" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "nil" + } + }, + "__CPROVER_constant_infinity_uint": { + "baseName": "__CPROVER_constant_infinity_uint", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_constant_infinity_uint", + "prettyName": "__CPROVER_constant_infinity_uint", + "prettyType": "const unsigned int", + "prettyValue": "", + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_int" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "nil" + } + }, + "__CPROVER_thread_keys": { + "baseName": "__CPROVER_thread_keys", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_thread_keys", + "prettyName": "__CPROVER_thread_keys", + "prettyType": "const void *[INFINITY()]", + "prettyValue": "", + "type": { + "id": "array", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "size": { + "id": "infinity", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + } + } + } + }, + "sub": [ + { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + } + ] + }, + "value": { + "id": "nil" + } + }, + "printf": { + "baseName": "printf", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": false, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "for_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "printf", + "prettyName": "", + "prettyType": "signed int (void)", + "prettyValue": "", + "type": { + "id": "code", + "namedSub": { + "#incomplete": { + "id": "1" + }, + "parameters": { + "id": "" + }, + "return_type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + "value": { + "id": "nil" + } + }, + "__CPROVER_architecture_short_int_width": { + "baseName": "__CPROVER_architecture_short_int_width", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "6" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_architecture_short_int_width", + "prettyName": "__CPROVER_architecture_short_int_width", + "prettyType": "const signed int", + "prettyValue": "16", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "6" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "10" + } + } + } + }, + "__CPROVER_malloc_object": { + "baseName": "__CPROVER_malloc_object", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "15" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_malloc_object", + "prettyName": "__CPROVER_malloc_object", + "prettyType": "const void *", + "prettyValue": "NULL", + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "15" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "15" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + }, + "value": { + "id": "constant", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "15" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "15" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + }, + "value": { + "id": "NULL" + } + } + } + }, + "__CPROVER_malloc_size": { + "baseName": "__CPROVER_malloc_size", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "16" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_malloc_size", + "prettyName": "__CPROVER_malloc_size", + "prettyType": "__CPROVER_size_t", + "prettyValue": "", + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "#typedef": { + "id": "__CPROVER_size_t" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "nil" + } + }, + "__CPROVER_malloc_is_new_array": { + "baseName": "__CPROVER_malloc_is_new_array", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "17" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_malloc_is_new_array", + "prettyName": "__CPROVER_malloc_is_new_array", + "prettyType": "__CPROVER_bool", + "prettyValue": "0 != 0", + "type": { + "id": "bool" + }, + "value": { + "id": "notequal", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "17" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "bool" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "17" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + }, + "__CPROVER_memory_leak": { + "baseName": "__CPROVER_memory_leak", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "18" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_memory_leak", + "prettyName": "__CPROVER_memory_leak", + "prettyType": "const void *", + "prettyValue": "NULL", + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "18" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "18" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + }, + "value": { + "id": "constant", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "18" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "18" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + }, + "value": { + "id": "NULL" + } + } + } + }, + "__CPROVER_architecture_long_int_width": { + "baseName": "__CPROVER_architecture_long_int_width", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_architecture_long_int_width", + "prettyName": "__CPROVER_architecture_long_int_width", + "prettyType": "const signed int", + "prettyValue": "64", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "40" + } + } + } + }, + "__CPROVER_architecture_long_long_int_width": { + "baseName": "__CPROVER_architecture_long_long_int_width", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_architecture_long_long_int_width", + "prettyName": "__CPROVER_architecture_long_long_int_width", + "prettyType": "const signed int", + "prettyValue": "64", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "40" + } + } + } + }, + "__CPROVER_architecture_int_width": { + "baseName": "__CPROVER_architecture_int_width", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_architecture_int_width", + "prettyName": "__CPROVER_architecture_int_width", + "prettyType": "const signed int", + "prettyValue": "32", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "20" + } + } + } + }, + "__CPROVER_architecture_word_size": { + "baseName": "__CPROVER_architecture_word_size", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_architecture_word_size", + "prettyName": "__CPROVER_architecture_word_size", + "prettyType": "const signed int", + "prettyValue": "32", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "20" + } + } + } + }, + "__CPROVER_alloca_object": { + "baseName": "__CPROVER_alloca_object", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_alloca_object", + "prettyName": "__CPROVER_alloca_object", + "prettyType": "const void *", + "prettyValue": "NULL", + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + }, + "value": { + "id": "constant", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + } + } + } + ] + }, + "value": { + "id": "NULL" + } + } + } + }, + "__CPROVER_architecture_bool_width": { + "baseName": "__CPROVER_architecture_bool_width", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "4" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_architecture_bool_width", + "prettyName": "__CPROVER_architecture_bool_width", + "prettyType": "const signed int", + "prettyValue": "8", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "4" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "8" + } + } + } + }, + "__CPROVER_architecture_char_width": { + "baseName": "__CPROVER_architecture_char_width", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "5" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_architecture_char_width", + "prettyName": "__CPROVER_architecture_char_width", + "prettyType": "const signed int", + "prettyValue": "8", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "5" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "8" + } + } + } + }, + "__CPROVER_rounding_mode": { + "baseName": "__CPROVER_rounding_mode", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "24" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_rounding_mode", + "prettyName": "__CPROVER_rounding_mode", + "prettyType": "signed int", + "prettyValue": "0", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "24" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + }, + "__CPROVER_architecture_pointer_width": { + "baseName": "__CPROVER_architecture_pointer_width", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "for_test", + "name": "__CPROVER_architecture_pointer_width", + "prettyName": "__CPROVER_architecture_pointer_width", + "prettyType": "const signed int", + "prettyValue": "64", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "40" + } + } + } + } + } + } +] diff --git a/kanillian/lib/compiler/compile_expr.ml b/kanillian/lib/compiler/compile_expr.ml index 8969ddf6..19347ddf 100644 --- a/kanillian/lib/compiler/compile_expr.ml +++ b/kanillian/lib/compiler/compile_expr.ml @@ -971,43 +971,84 @@ and poison ~ctx ~annot (lhs : GExpr.t) = in pre @ [ annot write ] -and compile_assign ~ctx ~annot ~lhs ~rhs = - let v, pre1 = compile_expr ~ctx rhs in - let access, pre2 = lvalue_as_access ~ctx ~read:false lhs in - let write = - match (access, v) with +and compile_assign_val ~ctx ~annot ~lhs ~(rhs : Val_repr.t) = + let ( let++ ) f o = Result.map o f in + let access, pre = lvalue_as_access ~ctx ~read:false lhs in + let++ write = + match (access, rhs) with | ZST, _ -> - [ annot Cmd.Skip ] + Ok [ annot Cmd.Skip ] (* We need a command in case we try want to add a label *) - | Direct x, ByValue v -> [ annot (Assignment (x, v)) ] + | Direct x, ByValue v -> Ok [ annot (Assignment (x, v)) ] | InMemoryScalar { ptr; _ }, ByValue v -> - [ annot (Memory.store_scalar ~ctx ptr v lhs.type_) ] + Ok [ annot (Memory.store_scalar ~ctx ptr v lhs.type_) ] | ( InMemoryComposit { ptr = ptr_access; type_ = type_access }, ByCopy { ptr = ptr_v; type_ = type_v } ) -> if not (Ctx.type_equal ctx type_v type_access) then - Error.unexpected "ByCopy assignment with different types on each side" + Result.Error (Error.unexpected, "ByCopy assignment with different types on each side") else let copy_cmd = Memory.memcpy ~ctx ~type_:type_access ~dst:ptr_access ~src:ptr_v in - [ annot copy_cmd ] + Ok [ annot copy_cmd ] | InMemoryComposit { ptr = dst; _ }, ByCompositValue { writes; _ } -> - Memory.write_composit ~ctx ~annot ~dst writes + Ok (Memory.write_composit ~ctx ~annot ~dst writes) | _ -> Error.code_error (Fmt.str - "Invalid assignement, wrong mix of ByCopy and Direct assignments:\n\ - %a = %a.\n\ - Originally: %a = %a\n\n\ - \ Left type is %a and right type is %a" pp_access - access Val_repr.pp v GExpr.pp lhs GExpr.pp rhs GType.pp lhs.type_ - GType.pp rhs.type_) + "Invalid assignement, wrong mix of ByCopy and Direct assignments.\n\ + %a = %a." pp_access + access Val_repr.pp rhs) in Debugger_log.to_file (Fmt.str ">>> %d" (List.length write)); write |> List.iter (fun (_, _, c) -> Debugger_log.to_file (Fmt.str "%a" Cmd.pp_labeled c)); - (v, pre1 @ pre2 @ write) + pre @ write + +and compile_assign ~ctx ~annot ~lhs ~rhs = + let v, pre = compile_expr ~ctx rhs in + let comp_assign = match + compile_assign_val ~ctx ~annot ~lhs ~rhs:v + with + | Ok c -> c + | Error (throw, msg) -> + let msg = Fmt.str + "%s\n\ + Originally: %a = %a\n\n\ + \ Left type is %a and right type is %a" + msg GExpr.pp lhs Val_repr.pp v GType.pp lhs.type_ GType.pp rhs.type_ + in + throw msg + in + (v, pre @ comp_assign) + +and compile_selfop ~ctx ~ty ~annot op (e : GExpr.t) = + let open Ops.Self in + let open Ops.Binary in + let is_pre, op = match op with + | Preincrement -> true, Plus + | Predecrement -> true, Minus + | Postincrement -> false, Plus + | Postdecrement -> false, Minus + in + let e_pre, comp_expr = compile_expr ~ctx e in + let e_pre = Val_repr.as_value ~msg:"Selfop operand" e_pre in + let e_post, comp_op = + let lhs = Val_repr.ByValue e_pre in + let rhs = Val_repr.ByValue (Lit (Int Z.one)) in + compile_binop ~ctx ~lty:ty ~rty:ty op lhs rhs + in + let comp_op = List.map annot comp_op in + let comp_assign = match + compile_assign_val ~ctx ~annot ~lhs:e ~rhs:(ByValue e_post) + with + | Ok c -> c + | Error (throw, msg) -> throw msg + in + let v = if is_pre then e_post else e_pre in + let v = Val_repr.ByValue v in + v, (comp_expr @ comp_op @ comp_assign) and compile_symbol ~ctx ~b expr = if Ctx.is_zst_access ctx GExpr.(expr.type_) then by_value (Lit Null) @@ -1129,6 +1170,8 @@ and compile_expr ~(ctx : Ctx.t) (expr : GExpr.t) : Val_repr.t Cs.with_body = | op -> let cmd = b (Helpers.assert_unhandled ~feature:(UnOp op) []) in Cs.return ~app:[ cmd ] (Val_repr.ByValue (Lit Nono))) + | SelfOp { op; e } -> + compile_selfop ~ctx ~ty:e.type_ ~annot:b op e |> Cs.set_end | Nondet -> nondet_expr ~ctx ~loc:expr.location ~type_:expr.type_ ~display:default_display () @@ -1588,7 +1631,7 @@ and compile_statement ~ctx (stmt : Stmt.t) : Val_repr.t Cs.with_body = let guard_var = Val_repr.as_value ~msg:"for guard" guard_var in let _, comp_body = compile_statement_c body in let body_lab, comp_body = Body_item.get_or_set_fresh_lab ~ctx comp_body in - let _, comp_update = compile_statement_c update in + let _, comp_update = compile_expr_c update in let goto_guard = let cmd = Cmd.GuardedGoto (guard_var, body_lab, end_lab) in b ~cmd_kind:(Normal true) cmd diff --git a/kanillian/lib/goto_program/dune b/kanillian/lib/goto_program/dune index 46d53852..9ed3bc53 100644 --- a/kanillian/lib/goto_program/dune +++ b/kanillian/lib/goto_program/dune @@ -1,6 +1,6 @@ (library (name goto_lib) - (libraries irep_lib zarith kcommons) + (libraries irep_lib zarith kcommons gillian) (flags :standard -open Irep_lib -open Kcommons) (preprocess (pps ppx_deriving.std ppx_deriving_yojson))) diff --git a/kanillian/lib/goto_program/expr_and_stmt.ml b/kanillian/lib/goto_program/expr_and_stmt.ml index 7824deb7..b0f25ccb 100644 --- a/kanillian/lib/goto_program/expr_and_stmt.ml +++ b/kanillian/lib/goto_program/expr_and_stmt.ml @@ -1,3 +1,5 @@ +open Gillian.Utils.Syntaxes.Option + module rec Expr : sig type value = | Array of t list @@ -14,6 +16,7 @@ module rec Expr : sig | Dereference of t | EAssign of { lhs : t; rhs : t } | UnOp of { op : Ops.Unary.t; e : t } + | SelfOp of { op : Ops.Self.t; e : t } | Struct of t list | Member of { lhs : t; field : string } | AddressOf of t @@ -50,6 +53,7 @@ end = struct | Dereference of t | EAssign of { lhs : t; rhs : t } | UnOp of { op : Ops.Unary.t; e : t } + | SelfOp of { op : Ops.Self.t; e : t } | Struct of t list | Member of { lhs : t; field : string } | AddressOf of t @@ -81,6 +85,7 @@ end = struct | BinOp { op; lhs; rhs } -> pf ft "(%a %a %a)" pp lhs Ops.Binary.pp op pp rhs | UnOp { op; e } -> pf ft "(%a %a)" Ops.Unary.pp op pp e + | SelfOp { op; e } -> pf ft "%a%a%a" Ops.Self.pp_pre op pp e Ops.Self.pp_post op | ByteExtract { e; offset } -> pf ft "EXTRACT(%a, %a, %d)" pp e pp_type t.type_ offset | Struct xs -> pf ft "{ %a }" (list ~sep:semi pp) xs @@ -128,9 +133,22 @@ end = struct |> Z.to_int in ByteExtract { e = of_irep ~machine e; offset } + + and selfop_of_irep ~(machine : Machine_model.t) (irep : Irep.t) = + let open Ops.Self in + let lift_selfop op = lift_selfop ~machine irep op |> Option.some in + let* stmt = List.assoc_opt Id.Statement irep.named_sub in + match stmt.id with + | Postincrement -> lift_selfop Postincrement + | Postdecrement -> lift_selfop Postdecrement + | Preincrement -> lift_selfop Preincrement + | Predecrement -> lift_selfop Predecrement + | _ -> None + and side_effecting_of_irep ~(machine : Machine_model.t) (irep : Irep.t) = let of_irep = of_irep ~machine in + let- () = selfop_of_irep ~machine irep in match (irep $ Statement).id with | FunctionCall -> let func, args = @@ -168,6 +186,15 @@ end = struct Gerror.unexpected ~irep "Unary operator doesn't have exactly one operand" + and lift_selfop ~(machine : Machine_model.t) (irep : Irep.t) (op : Ops.Self.t) + = + let of_irep = of_irep ~machine in + match irep.sub with + | [ a ] -> SelfOp { op; e = of_irep a } + | _ -> + Gerror.unexpected ~irep + "Self operator doesn't have exactly one operand" + and value_of_irep ~(machine : Machine_model.t) ~(type_ : Type.t) @@ -338,7 +365,7 @@ and Stmt : sig default : t option; } | Ifthenelse of { guard : Expr.t; then_ : t; else_ : t option } - | For of { init : t; guard : Expr.t; update : t; body : t } + | For of { init : t; guard : Expr.t; update : Expr.t; body : t } | While of { guard : Expr.t; body : t } | Break | Skip @@ -381,7 +408,7 @@ end = struct default : t option; } | Ifthenelse of { guard : Expr.t; then_ : t; else_ : t option } - | For of { init : t; guard : Expr.t; update : t; body : t } + | For of { init : t; guard : Expr.t; update : Expr.t; body : t } | While of { guard : Expr.t; body : t } | Break | Skip @@ -449,7 +476,7 @@ end = struct in pf ft "@[if (%a)@\n%a%a@]" pp_expr guard pp then_ pp_else else_ | For { init; guard; update; body } -> - pf ft "@[for (%a; %a; %a)@\n%a@]" pp init pp_expr guard pp update + pf ft "@[for (%a; %a; %a)@\n%a@]" pp init pp_expr guard pp_expr update pp body | While { guard; body } -> pf ft "@[while (%a)@\n%a@]" pp_expr guard pp body @@ -618,6 +645,7 @@ end = struct and for_loop_of_irep ~machine ~unexpected (sub : Irep.t list) = (* For some reason, CBMC compiles for loops as a block with the init statement and *then* the loop, whose first sub is nil. *) + let e_of_irep = Expr.of_irep ~machine in let of_irep = of_irep ~machine in match sub with | [ init; loop ] -> ( @@ -626,7 +654,7 @@ end = struct let guard, update, body = match loop.sub with | [ _; guard; update; body ] -> - (Expr.of_irep ~machine guard, of_irep update, of_irep body) + (e_of_irep guard, e_of_irep update, of_irep body) | _ -> unexpected "Invalid for-loop statement" in let init = of_irep init in diff --git a/kanillian/lib/goto_program/goto_lib.mli b/kanillian/lib/goto_program/goto_lib.mli index b7b5f8ad..357f3f09 100644 --- a/kanillian/lib/goto_program/goto_lib.mli +++ b/kanillian/lib/goto_program/goto_lib.mli @@ -172,6 +172,7 @@ module rec Expr : sig | Dereference of t | EAssign of { lhs : t; rhs : t } | UnOp of { op : Ops.Unary.t; e : t } + | SelfOp of { op : Ops.Self.t; e : t } | Struct of t list | Member of { lhs : t; field : string } | AddressOf of t @@ -187,7 +188,7 @@ module rec Expr : sig [@@deriving show] val pp_custom : pp:t Fmt.t -> ?pp_type:Type.t Fmt.t -> t Fmt.t - val pp_full : Format.formatter -> t -> unit + val pp_full : t Fmt.t val as_symbol : t -> string val value_of_irep : machine:Machine_model.t -> type_:Type.t -> Irep.t -> value val of_irep : machine:Machine_model.t -> Irep.t -> t @@ -213,7 +214,7 @@ and Stmt : sig default : t option; } | Ifthenelse of { guard : Expr.t; then_ : t; else_ : t option } - | For of { init : t; guard : Expr.t; update : t; body : t } + | For of { init : t; guard : Expr.t; update : Expr.t; body : t } | While of { guard : Expr.t; body : t } | Break | Skip @@ -225,7 +226,7 @@ and Stmt : sig and switch_case = { case : Expr.t; sw_body : t } and t = { stmt_location : Location.t; body : body; comment : string option } - val pp : Format.formatter -> t -> unit + val pp : t Fmt.t val pp_custom : ?semi:bool -> diff --git a/kanillian/lib/goto_program/ops.ml b/kanillian/lib/goto_program/ops.ml index 38fd4ccf..3a62243f 100644 --- a/kanillian/lib/goto_program/ops.ml +++ b/kanillian/lib/goto_program/ops.ml @@ -39,6 +39,22 @@ end module Self = struct type t = Postdecrement | Postincrement | Predecrement | Preincrement [@@deriving show { with_path = false }] + + let pp_pre fmt t = + let f = Fmt.pf fmt in + match t with + | Preincrement -> f "++" + | Predecrement -> f "--" + | Postincrement + | Postdecrement -> () + + let pp_post fmt t = + let f = Fmt.pf fmt in + match t with + | Preincrement + | Predecrement -> () + | Postincrement -> f "++" + | Postdecrement -> f "--" end module Unary = struct diff --git a/kanillian/lib/goto_program/visitors.ml b/kanillian/lib/goto_program/visitors.ml index 8b9a8d14..2115ea4a 100644 --- a/kanillian/lib/goto_program/visitors.ml +++ b/kanillian/lib/goto_program/visitors.ml @@ -68,6 +68,9 @@ class ['a] iter = | UnOp { op; e } -> self#visit_unop ~ctx op; self#visit_expr ~ctx e + | SelfOp { op; e } -> + self#visit_selfop ~ctx op; + self#visit_expr ~ctx e | ByteExtract { e; _ } | Dereference e | AddressOf e | TypeCast e -> self#visit_expr ~ctx e | Index { array; index } -> @@ -126,7 +129,7 @@ class ['a] iter = | For { init; guard; update; body } -> self#visit_stmt ~ctx init; self#visit_expr ~ctx guard; - self#visit_stmt ~ctx update; + self#visit_expr ~ctx update; self#visit_stmt ~ctx body | While { guard; body } -> self#visit_expr ~ctx guard; @@ -282,6 +285,11 @@ class ['a] map = let new_e = self#visit_expr ~ctx e in if new_op == op && new_e == e then ev else UnOp { op = new_op; e = new_e } + | SelfOp { op; e } -> + let new_op = self#visit_selfop ~ctx op in + let new_e = self#visit_expr ~ctx e in + if new_op == op && new_e == e then ev + else SelfOp { op = new_op; e = new_e } | ByteExtract { e; offset } -> let new_e = self#visit_expr ~ctx e in if new_e == e then ev else ByteExtract { e = new_e; offset } @@ -389,7 +397,7 @@ class ['a] map = | For { init; guard; update; body = body' } -> let new_init = self#visit_stmt ~ctx init in let new_guard = self#visit_expr ~ctx guard in - let new_update = self#visit_stmt ~ctx update in + let new_update = self#visit_expr ~ctx update in let new_body = self#visit_stmt ~ctx body' in if new_init == init && new_guard == guard && new_update == update diff --git a/kanillian/lib/lifter/kani_c_lifter.ml b/kanillian/lib/lifter/kani_c_lifter.ml index 3772f63b..bf392be9 100644 --- a/kanillian/lib/lifter/kani_c_lifter.ml +++ b/kanillian/lib/lifter/kani_c_lifter.ml @@ -72,6 +72,7 @@ struct display : string; callers : rid list; stack_direction : stack_direction option; + nest_kind : nest_kind option; } [@@deriving to_yojson] @@ -89,7 +90,6 @@ struct (** Unifications contained in this command *) errors : string Ext_list.t; (** Errors occurring during this command *) mutable canonical_data : canonical_cmd_data option; - mutable nest_kind : nest_kind option; } [@@deriving to_yojson] @@ -150,11 +150,11 @@ struct |> Result.ok let finish partial = - let ({ prev; canonical_data; all_ids; ends; nest_kind; _ } : partial_data) + let ({ prev; canonical_data; all_ids; ends; _ } : partial_data) = partial in - let** { id; display; callers; stack_direction } = + let** { id; display; callers; stack_direction; nest_kind } = Result_utils.of_option ~none:"Trying to finish partial with no canonical data!" canonical_data @@ -166,12 +166,24 @@ struct let all_ids = all_ids |> Ext_list.to_list |> List.map fst in let ends = Ext_list.to_list ends in let++ kind = - match ends with - | [] -> Ok Final - | [ (Unknown, _) ] -> Ok Normal - | ends -> - let++ cases = ends_to_cases ~nest_kind ends in - Branch cases + let++ cases = ends_to_cases ~nest_kind ends in + let () = + let ends = ends |> List.map (fun (case, bd) -> + let case = Branch_case.case_to_yojson case in + let bd = branch_data_to_yojson bd in + `List [case; bd]) + in + let cases = cases |> List.map (fun (case, bd) -> + let case = Branch_case.to_yojson case in + let bd = branch_data_to_yojson bd in + `List [case; bd]) + in + DL.log (fun m -> m ~json:[("ends", `List ends); ("cases", `List cases)] "ENDS") + in + match cases with + | [] -> Final + | [ (Case (Unknown, _), _) ] -> Normal + | _ -> Branch cases in Finished { @@ -197,7 +209,6 @@ struct unifys = Ext_list.make (); errors = Ext_list.make (); canonical_data = None; - nest_kind = None; } module Update = struct @@ -226,23 +237,24 @@ struct | Some _, _ -> Error "HORROR - branch kind is set with pre-existing case!" - let update_paths ~is_end ~exec_data ~branch_case ~branch_kind partial = + let update_paths ~is_end ~exec_data ~branch_case ~annot ~branch_kind partial = let ({ id; kind; _ } : exec_data) = exec_data in let { ends; unexplored_paths; _ } = partial in - match (kind, is_end) with - | Final, _ -> Ok () - | Normal, false -> + match (annot.cmd_kind, kind, is_end) with + | Return, _, _ + | _, Final, _ -> Ok () + | _, Normal, false -> Stack.push (id, None) unexplored_paths; Ok () - | Branch cases, false -> + | _, Branch cases, false -> cases |> List.iter (fun (gil_case, ()) -> Stack.push (id, Some gil_case) unexplored_paths); Ok () - | Normal, true -> + | _, Normal, true -> Ext_list.add (branch_case, (id, None)) ends; Ok () - | Branch cases, true -> + | _, Branch cases, true -> cases |> List_utils.iter_results (fun (gil_case, ()) -> let++ case = @@ -280,7 +292,7 @@ struct ~stack_direction (partial : partial_data) = partial.canonical_data <- - Some { id; display = ""; callers; stack_direction }; + Some { id; display = ""; callers; stack_direction; nest_kind = None }; Ok () let update_canonical_data @@ -309,8 +321,9 @@ struct let** callers, stack_direction = get_stack_info ~partial exec_data in + let Annot.{ nest_kind; _ } = annot in partial.canonical_data <- - Some { id; display; callers; stack_direction }; + Some { id; display; callers; stack_direction; nest_kind }; Ok () | _ -> Ok () @@ -348,7 +361,7 @@ struct insert_id_and_case ~prev_id ~exec_data ~id partial in let** () = - update_paths ~is_end ~exec_data ~branch_case ~branch_kind partial + update_paths ~is_end ~exec_data ~branch_case ~annot ~branch_kind partial in let** () = update_canonical_data ~id ~annot ~exec_data partial in @@ -546,9 +559,10 @@ struct state.map <- new_cmd; Ok () | _, _, None -> Error "inserting to non-empty map with no prev!" - | Some In, _, Some (_, Some _) -> Error "stepping in with branch case!" + | Some In, _, Some (parent_id, Some Func_exit_placeholder) | Some In, _, Some (parent_id, None) -> - insert_as_submap ~state ~parent_id new_cmd + insert_as_submap ~state ~parent_id new_cmd + | Some In, _, Some (_, Some _) -> Error "stepping in with branch case!" | None, _, Some (prev_id, case) -> insert_as_next ~state ~prev_id ?case new_cmd | Some (Out prev_id), _, _ -> diff --git a/while_test.c b/while_test.c new file mode 100644 index 00000000..7242e058 --- /dev/null +++ b/while_test.c @@ -0,0 +1,8 @@ +int main() { + int i = 0; + while (i < 10) { + printf("%d\n", i); + i++; + } + return 0; +} diff --git a/while_test.c.symtab.json b/while_test.c.symtab.json new file mode 100644 index 00000000..98c2b9cf --- /dev/null +++ b/while_test.c.symtab.json @@ -0,0 +1,898 @@ +{ + "baseName": "main", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "mode": "C", + "module": "while_test", + "name": "main", + "prettyName": "main", + "prettyType": "signed int ()", + "prettyValue": "{\n signed int i=0;\n while(i < 10)\n {\n printf((const void *)\"%d\\n\", i);\n i++;\n }\n return 0;\n}", + "type": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "parameters": { + "id": "", + "namedSub": { + "ellipsis": { + "id": "1" + } + } + }, + "return_type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + "value": { + "id": "code", + "namedSub": { + "#end_location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "block" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "decl" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "identifier": { + "id": "main::1::i" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "while" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "<", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "bool" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "identifier": { + "id": "main::1::i" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "A" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#end_location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "block" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "4" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "expression" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "side_effect", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "4" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "function_call" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "4" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "identifier": { + "id": "printf" + }, + "type": { + "id": "code", + "namedSub": { + "#incomplete": { + "id": "1" + }, + "parameters": { + "id": "" + }, + "return_type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + } + }, + { + "id": "arguments", + "sub": [ + { + "id": "typecast", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + } + } + } + ] + } + }, + "sub": [ + { + "id": "address_of", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + ] + } + }, + "sub": [ + { + "id": "index", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + }, + "sub": [ + { + "id": "string_constant", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "4" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "array", + "namedSub": { + "size": { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "4" + } + } + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + ] + }, + "value": { + "id": "%d\n" + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + ] + } + ] + }, + { + "id": "symbol", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "4" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "identifier": { + "id": "main::1::i" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + ] + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "5" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "expression" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "side_effect", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "5" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "postincrement" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "5" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "identifier": { + "id": "main::1::i" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + ] + } + ] + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "statement": { + "id": "return" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "while_test.c" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/home/nat/code/Gillian" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + ] + } +} \ No newline at end of file