From f70304870af6a4c28e4871b7a8375f01f95de4ec Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Fri, 3 May 2019 13:16:34 +0100 Subject: [PATCH 1/3] Link JSON symbol tables Instead of trying to merge them and throwing exception for every symbol conflict. --- src/json-symtab-language/json_symtab_language.cpp | 8 ++++++-- src/json-symtab-language/module_dependencies.txt | 1 + 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/src/json-symtab-language/json_symtab_language.cpp b/src/json-symtab-language/json_symtab_language.cpp index aaf2def0574..309a3b60d67 100644 --- a/src/json-symtab-language/json_symtab_language.cpp +++ b/src/json-symtab-language/json_symtab_language.cpp @@ -13,6 +13,8 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include #include +#include + /// Parse a goto program in json form. /// \param instream: The input stream /// \param path: A file path @@ -34,10 +36,12 @@ bool json_symtab_languaget::typecheck( { (void)module; // unused parameter + symbol_tablet new_symbol_table; + try { - symbol_table_from_json(parsed_json_file, symbol_table); - return false; + symbol_table_from_json(parsed_json_file, new_symbol_table); + return linking(symbol_table, new_symbol_table, get_message_handler()); } catch(const std::string &str) { diff --git a/src/json-symtab-language/module_dependencies.txt b/src/json-symtab-language/module_dependencies.txt index b4db43a0dd0..c303f96beef 100644 --- a/src/json-symtab-language/module_dependencies.txt +++ b/src/json-symtab-language/module_dependencies.txt @@ -1,4 +1,5 @@ goto-programs json langapi +linking util From a88a188245388dd32e738b2ef5f72aef0175c4cf Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Mon, 13 May 2019 13:57:06 +0100 Subject: [PATCH 2/3] Add regression test for linking JSONs generated from Ada files. These are included as a documentation. --- regression/cbmc/link_json_symtabs/one.adb | 4 + .../cbmc/link_json_symtabs/one.json_symtab | 2258 +++++++++++ regression/cbmc/link_json_symtabs/test.desc | 11 + regression/cbmc/link_json_symtabs/two.adb | 7 + .../cbmc/link_json_symtabs/two.json_symtab | 3402 +++++++++++++++++ 5 files changed, 5682 insertions(+) create mode 100644 regression/cbmc/link_json_symtabs/one.adb create mode 100644 regression/cbmc/link_json_symtabs/one.json_symtab create mode 100644 regression/cbmc/link_json_symtabs/test.desc create mode 100644 regression/cbmc/link_json_symtabs/two.adb create mode 100644 regression/cbmc/link_json_symtabs/two.json_symtab diff --git a/regression/cbmc/link_json_symtabs/one.adb b/regression/cbmc/link_json_symtabs/one.adb new file mode 100644 index 00000000000..7a8e4b07979 --- /dev/null +++ b/regression/cbmc/link_json_symtabs/one.adb @@ -0,0 +1,4 @@ +procedure One (X : in out Integer) is +begin + X := X + 1; +end One; diff --git a/regression/cbmc/link_json_symtabs/one.json_symtab b/regression/cbmc/link_json_symtabs/one.json_symtab new file mode 100644 index 00000000000..0133fb6dab7 --- /dev/null +++ b/regression/cbmc/link_json_symtabs/one.json_symtab @@ -0,0 +1,2258 @@ +{ + "symbolTable": { + "standard__short_short_integer": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "8", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__short_short_integer", + "module": "", + "baseName": "standard__short_short_integer", + "mode": "C", + "prettyName": "standard__short_short_integer", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "memcpy::__source3": { + "type": { + "id": "pointer", + "sub": [ + { + "id": "empty" + } + ], + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "memcpy::__source3", + "module": "", + "baseName": "memcpy::__source3", + "mode": "C", + "prettyName": "memcpy::__source3", + "isType": false, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": true, + "isLvalue": true, + "isFileLocal": true, + "isExtern": false, + "isVolatile": false, + "isParameter": true, + "isAuxiliary": false, + "isWeak": false + }, + "standard__long_float": { + "type": { + "id": "floatbv", + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + }, + "f": { + "id": "52", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__long_float", + "module": "", + "baseName": "standard__long_float", + "mode": "C", + "prettyName": "standard__long_float", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "one": { + "type": { + "id": "code", + "namedSub": { + "parameters": { + "id": "parameters", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "one.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "1", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "16", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "#default_value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "pointer", + "sub": [ + { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#base_name": { + "id": "one__x", + "sub": [ + ], + "namedSub": { + } + }, + "#this": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#identifier": { + "id": "one__x", + "sub": [ + ], + "namedSub": { + } + } + } + } + ] + }, + "ellipsis": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "return_type": { + "id": "empty" + }, + "#inlined": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#KnR": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "code", + "sub": [ + { + "id": "code", + "sub": [ + { + "id": "code", + "sub": [ + { + "id": "dereference", + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "one.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "1", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "16", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "pointer", + "sub": [ + { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "identifier": { + "id": "one__x", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "+", + "sub": [ + { + "id": "dereference", + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "one.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "1", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "16", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "pointer", + "sub": [ + { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "identifier": { + "id": "one__x", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "one.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "3", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "13", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "value": { + "id": "1", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "one.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "3", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "11", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "overflow_check": { + "id": "1", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "one.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "3", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "6", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "statement": { + "id": "assign", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "statement": { + "id": "block", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "one.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "1", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "1", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "statement": { + "id": "block", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "one", + "module": "", + "baseName": "one", + "mode": "C", + "prettyName": "one", + "isType": false, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__natural": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__natural", + "module": "", + "baseName": "standard__natural", + "mode": "C", + "prettyName": "standard__natural", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__short_float": { + "type": { + "id": "floatbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + }, + "f": { + "id": "23", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__short_float", + "module": "", + "baseName": "standard__short_float", + "mode": "C", + "prettyName": "standard__short_float", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__positive": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__positive", + "module": "", + "baseName": "standard__positive", + "mode": "C", + "prettyName": "standard__positive", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "memcpy": { + "type": { + "id": "code", + "namedSub": { + "parameters": { + "id": "parameters", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "#default_value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "pointer", + "sub": [ + { + "id": "empty" + } + ], + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#base_name": { + "id": "memcpy::__destination2", + "sub": [ + ], + "namedSub": { + } + }, + "#this": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#identifier": { + "id": "memcpy::__destination2", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "parameter", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "#default_value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "pointer", + "sub": [ + { + "id": "empty" + } + ], + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#base_name": { + "id": "memcpy::__source3", + "sub": [ + ], + "namedSub": { + } + }, + "#this": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#identifier": { + "id": "memcpy::__source3", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "parameter", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "#default_value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#base_name": { + "id": "memcpy::__num4", + "sub": [ + ], + "namedSub": { + } + }, + "#this": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#identifier": { + "id": "memcpy::__num4", + "sub": [ + ], + "namedSub": { + } + } + } + } + ] + }, + "ellipsis": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "return_type": { + "id": "pointer", + "sub": [ + { + "id": "empty" + } + ], + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "#inlined": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#KnR": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "memcpy", + "module": "", + "baseName": "memcpy", + "mode": "C", + "prettyName": "memcpy", + "isType": false, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "one__x": { + "type": { + "id": "pointer", + "sub": [ + { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "one__x", + "module": "", + "baseName": "one__x", + "mode": "C", + "prettyName": "one__x", + "isType": false, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": true, + "isLvalue": true, + "isFileLocal": true, + "isExtern": false, + "isVolatile": false, + "isParameter": true, + "isAuxiliary": false, + "isWeak": false + }, + "memcpy::__destination2": { + "type": { + "id": "pointer", + "sub": [ + { + "id": "empty" + } + ], + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "memcpy::__destination2", + "module": "", + "baseName": "memcpy::__destination2", + "mode": "C", + "prettyName": "memcpy::__destination2", + "isType": false, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": true, + "isLvalue": true, + "isFileLocal": true, + "isExtern": false, + "isVolatile": false, + "isParameter": true, + "isAuxiliary": false, + "isWeak": false + }, + "standard__integer": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__integer", + "module": "", + "baseName": "standard__integer", + "mode": "C", + "prettyName": "standard__integer", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__boolean": { + "type": { + "id": "bool" + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__boolean", + "module": "", + "baseName": "standard__boolean", + "mode": "C", + "prettyName": "standard__boolean", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "malloc::__size1": { + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "malloc::__size1", + "module": "", + "baseName": "malloc::__size1", + "mode": "C", + "prettyName": "malloc::__size1", + "isType": false, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": true, + "isLvalue": true, + "isFileLocal": true, + "isExtern": false, + "isVolatile": false, + "isParameter": true, + "isAuxiliary": false, + "isWeak": false + }, + "standard__long_long_integer": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__long_long_integer", + "module": "", + "baseName": "standard__long_long_integer", + "mode": "C", + "prettyName": "standard__long_long_integer", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "malloc": { + "type": { + "id": "code", + "namedSub": { + "parameters": { + "id": "parameters", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "#default_value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#base_name": { + "id": "malloc::__size1", + "sub": [ + ], + "namedSub": { + } + }, + "#this": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#identifier": { + "id": "malloc::__size1", + "sub": [ + ], + "namedSub": { + } + } + } + } + ] + }, + "ellipsis": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "return_type": { + "id": "pointer", + "sub": [ + { + "id": "empty" + } + ], + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "#inlined": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#KnR": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "malloc", + "module": "", + "baseName": "malloc", + "mode": "C", + "prettyName": "malloc", + "isType": false, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__wide_character": { + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "16", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__wide_character", + "module": "", + "baseName": "standard__wide_character", + "mode": "C", + "prettyName": "standard__wide_character", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "memcpy::__num4": { + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "memcpy::__num4", + "module": "", + "baseName": "memcpy::__num4", + "mode": "C", + "prettyName": "memcpy::__num4", + "isType": false, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": true, + "isLvalue": true, + "isFileLocal": true, + "isExtern": false, + "isVolatile": false, + "isParameter": true, + "isAuxiliary": false, + "isWeak": false + }, + "__CPROVER_rounding_mode": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "__CPROVER_rounding_mode", + "module": "", + "baseName": "__CPROVER_rounding_mode", + "mode": "C", + "prettyName": "__CPROVER_rounding_mode", + "isType": false, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isLvalue": true, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__universal_integer": { + "type": { + "id": "integer" + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__universal_integer", + "module": "", + "baseName": "standard__universal_integer", + "mode": "C", + "prettyName": "standard__universal_integer", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "__CPROVER_size_t": { + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "__CPROVER_size_t", + "module": "", + "baseName": "__CPROVER_size_t", + "mode": "C", + "prettyName": "__CPROVER_size_t", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__long_integer": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__long_integer", + "module": "", + "baseName": "standard__long_integer", + "mode": "C", + "prettyName": "standard__long_integer", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__character": { + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "8", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__character", + "module": "", + "baseName": "standard__character", + "mode": "C", + "prettyName": "standard__character", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__float": { + "type": { + "id": "floatbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + }, + "f": { + "id": "23", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__float", + "module": "", + "baseName": "standard__float", + "mode": "C", + "prettyName": "standard__float", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__long_long_float": { + "type": { + "id": "floatbv", + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + }, + "f": { + "id": "52", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__long_long_float", + "module": "", + "baseName": "standard__long_long_float", + "mode": "C", + "prettyName": "standard__long_long_float", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__wide_wide_character": { + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__wide_wide_character", + "module": "", + "baseName": "standard__wide_wide_character", + "mode": "C", + "prettyName": "standard__wide_wide_character", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__string": { + "type": { + "id": "string" + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__string", + "module": "", + "baseName": "standard__string", + "mode": "C", + "prettyName": "standard__string", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__short_integer": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "16", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__short_integer", + "module": "", + "baseName": "standard__short_integer", + "mode": "C", + "prettyName": "standard__short_integer", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + } + } +} diff --git a/regression/cbmc/link_json_symtabs/test.desc b/regression/cbmc/link_json_symtabs/test.desc new file mode 100644 index 00000000000..c6f6ebe9068 --- /dev/null +++ b/regression/cbmc/link_json_symtabs/test.desc @@ -0,0 +1,11 @@ +CORE +one.json_symtab +two.json_symtab +^EXIT=0$ +^SIGNAL=0$ +\[1\] file two.adb line [0-9]+ assertion: SUCCESS +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +The two symbol tables are generated from the respective Ada files. The file `two` contains CPROVER start and initialize and call the function defined in `one`. diff --git a/regression/cbmc/link_json_symtabs/two.adb b/regression/cbmc/link_json_symtabs/two.adb new file mode 100644 index 00000000000..7812ad01f13 --- /dev/null +++ b/regression/cbmc/link_json_symtabs/two.adb @@ -0,0 +1,7 @@ +with One; +procedure Two is + X : Integer := 1; +begin + One (X); + pragma Assert (X=2); +end Two; diff --git a/regression/cbmc/link_json_symtabs/two.json_symtab b/regression/cbmc/link_json_symtabs/two.json_symtab new file mode 100644 index 00000000000..045f9b6bfe1 --- /dev/null +++ b/regression/cbmc/link_json_symtabs/two.json_symtab @@ -0,0 +1,3402 @@ +{ + "symbolTable": { + "standard__short_short_integer": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "8", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__short_short_integer", + "module": "", + "baseName": "standard__short_short_integer", + "mode": "C", + "prettyName": "standard__short_short_integer", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "memcpy::__source3": { + "type": { + "id": "pointer", + "sub": [ + { + "id": "empty" + } + ], + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "memcpy::__source3", + "module": "", + "baseName": "memcpy::__source3", + "mode": "C", + "prettyName": "memcpy::__source3", + "isType": false, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": true, + "isLvalue": true, + "isFileLocal": true, + "isExtern": false, + "isVolatile": false, + "isParameter": true, + "isAuxiliary": false, + "isWeak": false + }, + "standard__long_float": { + "type": { + "id": "floatbv", + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + }, + "f": { + "id": "52", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__long_float", + "module": "", + "baseName": "standard__long_float", + "mode": "C", + "prettyName": "standard__long_float", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "one": { + "type": { + "id": "code", + "namedSub": { + "parameters": { + "id": "parameters", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "one.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "1", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "16", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "#default_value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "pointer", + "sub": [ + { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#base_name": { + "id": "one__x", + "sub": [ + ], + "namedSub": { + } + }, + "#this": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#identifier": { + "id": "one__x", + "sub": [ + ], + "namedSub": { + } + } + } + } + ] + }, + "ellipsis": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "return_type": { + "id": "empty" + }, + "#inlined": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#KnR": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "one.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "1", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "1", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "one", + "module": "", + "baseName": "one", + "mode": "C", + "prettyName": "one", + "isType": false, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__natural": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__natural", + "module": "", + "baseName": "standard__natural", + "mode": "C", + "prettyName": "standard__natural", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__short_float": { + "type": { + "id": "floatbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + }, + "f": { + "id": "23", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__short_float", + "module": "", + "baseName": "standard__short_float", + "mode": "C", + "prettyName": "standard__short_float", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__positive": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__positive", + "module": "", + "baseName": "standard__positive", + "mode": "C", + "prettyName": "standard__positive", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "memcpy": { + "type": { + "id": "code", + "namedSub": { + "parameters": { + "id": "parameters", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "#default_value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "pointer", + "sub": [ + { + "id": "empty" + } + ], + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#base_name": { + "id": "memcpy::__destination2", + "sub": [ + ], + "namedSub": { + } + }, + "#this": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#identifier": { + "id": "memcpy::__destination2", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "parameter", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "#default_value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "pointer", + "sub": [ + { + "id": "empty" + } + ], + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#base_name": { + "id": "memcpy::__source3", + "sub": [ + ], + "namedSub": { + } + }, + "#this": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#identifier": { + "id": "memcpy::__source3", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "parameter", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "#default_value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#base_name": { + "id": "memcpy::__num4", + "sub": [ + ], + "namedSub": { + } + }, + "#this": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#identifier": { + "id": "memcpy::__num4", + "sub": [ + ], + "namedSub": { + } + } + } + } + ] + }, + "ellipsis": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "return_type": { + "id": "pointer", + "sub": [ + { + "id": "empty" + } + ], + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "#inlined": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#KnR": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "memcpy", + "module": "", + "baseName": "memcpy", + "mode": "C", + "prettyName": "memcpy", + "isType": false, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "one__x": { + "type": { + "id": "pointer", + "sub": [ + { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "one__x", + "module": "", + "baseName": "one__x", + "mode": "C", + "prettyName": "one__x", + "isType": false, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": true, + "isLvalue": true, + "isFileLocal": true, + "isExtern": false, + "isVolatile": false, + "isParameter": true, + "isAuxiliary": false, + "isWeak": false + }, + "memcpy::__destination2": { + "type": { + "id": "pointer", + "sub": [ + { + "id": "empty" + } + ], + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "memcpy::__destination2", + "module": "", + "baseName": "memcpy::__destination2", + "mode": "C", + "prettyName": "memcpy::__destination2", + "isType": false, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": true, + "isLvalue": true, + "isFileLocal": true, + "isExtern": false, + "isVolatile": false, + "isParameter": true, + "isAuxiliary": false, + "isWeak": false + }, + "standard__integer": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__integer", + "module": "", + "baseName": "standard__integer", + "mode": "C", + "prettyName": "standard__integer", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "__CPROVER__start": { + "type": { + "id": "code", + "namedSub": { + "parameters": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "ellipsis": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "return_type": { + "id": "empty" + }, + "#inlined": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#KnR": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "code", + "sub": [ + { + "id": "code", + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "signedbv", + "sub": [ + { + "id": "" + } + ], + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "identifier": { + "id": "__CPROVER_rounding_mode", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "signedbv", + "sub": [ + { + "id": "" + } + ], + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "value": { + "id": "00000000000000000000000000000000", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "statement": { + "id": "assign", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "code", + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "empty" + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "identifier": { + "id": "return'", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "statement": { + "id": "decl", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "code", + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "empty" + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "identifier": { + "id": "return'", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "code", + "namedSub": { + "parameters": { + "id": "parameters" + }, + "ellipsis": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "return_type": { + "id": "empty" + }, + "#inlined": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#KnR": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "identifier": { + "id": "two", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "arguments" + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "statement": { + "id": "function_call", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "statement": { + "id": "block", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "__CPROVER__start", + "module": "", + "baseName": "__CPROVER__start", + "mode": "C", + "prettyName": "__CPROVER__start", + "isType": false, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "return'": { + "type": { + "id": "empty" + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "return'", + "module": "", + "baseName": "return'", + "mode": "C", + "prettyName": "return'", + "isType": false, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__boolean": { + "type": { + "id": "bool" + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__boolean", + "module": "", + "baseName": "standard__boolean", + "mode": "C", + "prettyName": "standard__boolean", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "malloc::__size1": { + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "malloc::__size1", + "module": "", + "baseName": "malloc::__size1", + "mode": "C", + "prettyName": "malloc::__size1", + "isType": false, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": true, + "isLvalue": true, + "isFileLocal": true, + "isExtern": false, + "isVolatile": false, + "isParameter": true, + "isAuxiliary": false, + "isWeak": false + }, + "two__x": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "two.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "3", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "4", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "two__x", + "module": "", + "baseName": "two__x", + "mode": "C", + "prettyName": "two__x", + "isType": false, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": true, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": true, + "isLvalue": true, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__long_long_integer": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__long_long_integer", + "module": "", + "baseName": "standard__long_long_integer", + "mode": "C", + "prettyName": "standard__long_long_integer", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "malloc": { + "type": { + "id": "code", + "namedSub": { + "parameters": { + "id": "parameters", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "#default_value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#base_name": { + "id": "malloc::__size1", + "sub": [ + ], + "namedSub": { + } + }, + "#this": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#identifier": { + "id": "malloc::__size1", + "sub": [ + ], + "namedSub": { + } + } + } + } + ] + }, + "ellipsis": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "return_type": { + "id": "pointer", + "sub": [ + { + "id": "empty" + } + ], + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "#inlined": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#KnR": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "malloc", + "module": "", + "baseName": "malloc", + "mode": "C", + "prettyName": "malloc", + "isType": false, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__wide_character": { + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "16", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__wide_character", + "module": "", + "baseName": "standard__wide_character", + "mode": "C", + "prettyName": "standard__wide_character", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "memcpy::__num4": { + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "memcpy::__num4", + "module": "", + "baseName": "memcpy::__num4", + "mode": "C", + "prettyName": "memcpy::__num4", + "isType": false, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": true, + "isLvalue": true, + "isFileLocal": true, + "isExtern": false, + "isVolatile": false, + "isParameter": true, + "isAuxiliary": false, + "isWeak": false + }, + "__CPROVER_rounding_mode": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "__CPROVER_rounding_mode", + "module": "", + "baseName": "__CPROVER_rounding_mode", + "mode": "C", + "prettyName": "__CPROVER_rounding_mode", + "isType": false, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isLvalue": true, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__universal_integer": { + "type": { + "id": "integer" + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__universal_integer", + "module": "", + "baseName": "standard__universal_integer", + "mode": "C", + "prettyName": "standard__universal_integer", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "__CPROVER_size_t": { + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "__CPROVER_size_t", + "module": "", + "baseName": "__CPROVER_size_t", + "mode": "C", + "prettyName": "__CPROVER_size_t", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__long_integer": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__long_integer", + "module": "", + "baseName": "standard__long_integer", + "mode": "C", + "prettyName": "standard__long_integer", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__character": { + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "8", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__character", + "module": "", + "baseName": "standard__character", + "mode": "C", + "prettyName": "standard__character", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__float": { + "type": { + "id": "floatbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + }, + "f": { + "id": "23", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__float", + "module": "", + "baseName": "standard__float", + "mode": "C", + "prettyName": "standard__float", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__long_long_float": { + "type": { + "id": "floatbv", + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + }, + "f": { + "id": "52", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__long_long_float", + "module": "", + "baseName": "standard__long_long_float", + "mode": "C", + "prettyName": "standard__long_long_float", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__wide_wide_character": { + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__wide_wide_character", + "module": "", + "baseName": "standard__wide_wide_character", + "mode": "C", + "prettyName": "standard__wide_wide_character", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__string": { + "type": { + "id": "string" + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__string", + "module": "", + "baseName": "standard__string", + "mode": "C", + "prettyName": "standard__string", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "two": { + "type": { + "id": "code", + "namedSub": { + "parameters": { + "id": "parameters" + }, + "ellipsis": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "return_type": { + "id": "empty" + }, + "#inlined": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#KnR": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "code", + "sub": [ + { + "id": "code", + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "two.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "3", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "4", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "identifier": { + "id": "two__x", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "two.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "3", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "4", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "statement": { + "id": "decl", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "code", + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "two.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "3", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "4", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "identifier": { + "id": "two__x", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "two.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "3", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "19", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "value": { + "id": "1", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "two.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "3", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "4", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "statement": { + "id": "assign", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "code", + "sub": [ + { + "id": "code", + "sub": [ + { + "id": "nil", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "two.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "5", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "4", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "code", + "namedSub": { + "parameters": { + "id": "parameters", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "one.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "1", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "16", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "#default_value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "pointer", + "sub": [ + { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#base_name": { + "id": "one__x", + "sub": [ + ], + "namedSub": { + } + }, + "#this": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#identifier": { + "id": "one__x", + "sub": [ + ], + "namedSub": { + } + } + } + } + ] + }, + "ellipsis": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "return_type": { + "id": "empty" + }, + "#inlined": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#KnR": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "identifier": { + "id": "one", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "arguments", + "sub": [ + { + "id": "address_of", + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "two.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "3", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "4", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "identifier": { + "id": "two__x", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "pointer", + "sub": [ + { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "width": { + "id": "64", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + } + } + } + ] + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "two.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "5", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "4", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "statement": { + "id": "function_call", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "code", + "sub": [ + { + "id": "=", + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "two.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "3", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "4", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "identifier": { + "id": "two__x", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "two.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "6", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "21", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "value": { + "id": "2", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "two.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "6", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "20", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "overflow_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "bool" + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "two.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "6", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "4", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "statement": { + "id": "assert", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "statement": { + "id": "block", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "two.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "2", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "1", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "statement": { + "id": "block", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "two", + "module": "", + "baseName": "two", + "mode": "C", + "prettyName": "two", + "isType": false, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + }, + "standard__short_integer": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "16", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__short_integer", + "module": "", + "baseName": "standard__short_integer", + "mode": "C", + "prettyName": "standard__short_integer", + "isType": true, + "isMacro": false, + "isExported": false, + "isInput": false, + "isOutput": false, + "isStateVar": false, + "isProperty": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isLvalue": false, + "isFileLocal": false, + "isExtern": false, + "isVolatile": false, + "isParameter": false, + "isAuxiliary": false, + "isWeak": false + } + } +} From 16e2a14009d66c60f480e4804d8201d76bc4ee60 Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Tue, 14 May 2019 11:25:37 +0100 Subject: [PATCH 3/3] Unify the remove-returns query between goto-program/remove-return and the respective validation check. Update the unit-test accordingly. --- src/goto-programs/remove_returns.cpp | 12 ++++++++---- src/goto-programs/remove_returns.h | 6 ++++++ src/goto-programs/validate_goto_model.cpp | 3 ++- unit/goto-programs/goto_program_validate.cpp | 3 ++- 4 files changed, 18 insertions(+), 6 deletions(-) diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index 57d515d4865..f00d8078830 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/src/goto-programs/remove_returns.cpp @@ -162,10 +162,7 @@ bool remove_returnst::do_function_calls( to_symbol_expr(function_call.function()).get_identifier(); // Do we return anything? - if( - to_code_type(function_call.function().type()).return_type() != - empty_typet() && - function_call.lhs().is_not_nil()) + if(does_function_call_return(function_call)) { // replace "lhs=f(...)" by // "f(...); lhs=f#return_value; DEAD f#return_value;" @@ -430,3 +427,10 @@ bool is_return_value_symbol(const symbol_exprt &symbol_expr) { return is_return_value_identifier(symbol_expr.get_identifier()); } + +bool does_function_call_return(const code_function_callt &function_call) +{ + return to_code_type(function_call.function().type()).return_type() != + empty_typet() && + function_call.lhs().is_not_nil(); +} diff --git a/src/goto-programs/remove_returns.h b/src/goto-programs/remove_returns.h index 5d990f82e60..80aa3f7584d 100644 --- a/src/goto-programs/remove_returns.h +++ b/src/goto-programs/remove_returns.h @@ -73,6 +73,7 @@ Date: September 2009 #include +#include #include class goto_functionst; @@ -111,4 +112,9 @@ bool is_return_value_identifier(const irep_idt &id); /// \ref return_value_symbol bool is_return_value_symbol(const symbol_exprt &symbol_expr); +/// Check if the \p function_call returns anything +/// \param function_call: the function call to be investigated +/// \return true if non-void return type and non-nil lhs +bool does_function_call_return(const code_function_callt &function_call); + #endif // CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H diff --git a/src/goto-programs/validate_goto_model.cpp b/src/goto-programs/validate_goto_model.cpp index 7aefc947a8c..39c76380d42 100644 --- a/src/goto-programs/validate_goto_model.cpp +++ b/src/goto-programs/validate_goto_model.cpp @@ -14,6 +14,7 @@ Date: Oct 2018 #include #include "goto_functions.h" +#include "remove_returns.h" namespace { @@ -132,7 +133,7 @@ void validate_goto_modelt::check_returns_removed() const auto &function_call = instr.get_function_call(); DATA_CHECK( vm, - function_call.lhs().is_nil(), + !does_function_call_return(function_call), "function call lhs return should be nil"); } } diff --git a/unit/goto-programs/goto_program_validate.cpp b/unit/goto-programs/goto_program_validate.cpp index 6e67e6ccdc5..095a9f7f2f0 100644 --- a/unit/goto-programs/goto_program_validate.cpp +++ b/unit/goto-programs/goto_program_validate.cpp @@ -217,10 +217,11 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") WHEN("not all returns have been removed - a function call lhs is not nil") { + // int h(); symbolt h; h.name = "h"; h.mode = ID_C; - h.type = code_typet({}, empty_typet{}); + h.type = code_typet({}, signed_int_type()); h.value = code_blockt{}; goto_model.symbol_table.add(h);