diff --git a/CMakeLists.txt b/CMakeLists.txt index 73a43ba8068..e043a28bbe4 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -141,6 +141,7 @@ set_target_properties( linking pointer-analysis solvers + symtab2gb testing-utils unit util diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index aea76941868..c14b7734d55 100644 --- a/regression/CMakeLists.txt +++ b/regression/CMakeLists.txt @@ -52,3 +52,4 @@ add_subdirectory(contracts) add_subdirectory(goto-harness) add_subdirectory(goto-cc-file-local) add_subdirectory(linking-goto-binaries) +add_subdirectory(symtab2gb) diff --git a/regression/Makefile b/regression/Makefile index d99dff1f388..0af06be799a 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -27,6 +27,7 @@ DIRS = cbmc \ contracts \ goto-cc-file-local \ linking-goto-binaries \ + symtab2gb \ # Empty last line # Run all test directories in sequence diff --git a/regression/symtab2gb/CMakeLists.txt b/regression/symtab2gb/CMakeLists.txt new file mode 100644 index 00000000000..a8c851843b8 --- /dev/null +++ b/regression/symtab2gb/CMakeLists.txt @@ -0,0 +1,3 @@ +add_test_pl_tests( + "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $ $" +) diff --git a/regression/symtab2gb/Makefile b/regression/symtab2gb/Makefile new file mode 100644 index 00000000000..e0ec85eede2 --- /dev/null +++ b/regression/symtab2gb/Makefile @@ -0,0 +1,27 @@ +default: tests.log + +include ../../src/config.inc +include ../../src/common + +test: + @../test.pl -e -p -c '../chain.sh $(exe) ../../../src/symtab2gb/symtab2gb ../../../src/cbmc/cbmc' + +tests.log: + @../test.pl -e -p -c '../chain.sh $(exe) ../../../src/symtab2gb/symtab2gb ../../../src/cbmc/cbmc' + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.c" "$$dir/*.out"; \ + fi; \ + done; + +clean: + @for dir in *; do \ + $(RM) tests.log; \ + if [ -d "$$dir" ]; then \ + cd "$$dir"; \ + $(RM) *.out *.gb; \ + cd ..; \ + fi \ + done diff --git a/regression/symtab2gb/chain.sh b/regression/symtab2gb/chain.sh new file mode 100755 index 00000000000..cbe80512f7c --- /dev/null +++ b/regression/symtab2gb/chain.sh @@ -0,0 +1,6 @@ +#!/bin/bash +symtab2gb_exe=$1 +cbmc_exe=$2 + +$symtab2gb_exe "${@:3}" +$cbmc_exe a.out diff --git a/regression/symtab2gb/multiple_symtabs/README.md b/regression/symtab2gb/multiple_symtabs/README.md new file mode 100644 index 00000000000..12ee5cc8d35 --- /dev/null +++ b/regression/symtab2gb/multiple_symtabs/README.md @@ -0,0 +1,19 @@ +The `*.json_symtab` in this directory was created from the Ada source +files `*.adb` using the +[gnat2goto](https://github.com/diffblue/gnat2goto) compiler. + +``` +gnat2goto user.adb # produces user.json_symtab + +# produces library.json_symtab +# and user.json_symtab +# the --no-cprover-start option is to prevent +# emitting a __CPROVER_start function for these modules, +# as there can only be one of those in a program + +gnat2goto --no-cprover-start library.adb +gnat2goto --no-cprover-start user.adb +``` + +Note that as of now, this requires the patch found in +[this PR](https://github.com/diffblue/gnat2goto/pull/212) diff --git a/regression/symtab2gb/multiple_symtabs/entry_point.adb b/regression/symtab2gb/multiple_symtabs/entry_point.adb new file mode 100644 index 00000000000..793504ffebd --- /dev/null +++ b/regression/symtab2gb/multiple_symtabs/entry_point.adb @@ -0,0 +1,7 @@ +with User; +with Library; +procedure Entry_Point is +begin + User; + Library (-5); +end Entry_Point; diff --git a/regression/symtab2gb/multiple_symtabs/entry_point.json_symtab b/regression/symtab2gb/multiple_symtabs/entry_point.json_symtab new file mode 100644 index 00000000000..a2583ff57eb --- /dev/null +++ b/regression/symtab2gb/multiple_symtabs/entry_point.json_symtab @@ -0,0 +1,2982 @@ +{ + "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 + }, + "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 + }, + "library": { + "type": { + "id": "code", + "namedSub": { + "parameters": { + "id": "parameters", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "library.ads", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "1", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "20", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "#default_value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#base_name": { + "id": "library__x", + "sub": [ + ], + "namedSub": { + } + }, + "#this": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#identifier": { + "id": "library__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": "library.ads", + "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": "library", + "module": "", + "baseName": "library", + "mode": "C", + "prettyName": "library", + "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__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 + }, + "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": "entry_point", + "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 + }, + "library__x": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "library__x", + "module": "", + "baseName": "library__x", + "mode": "C", + "prettyName": "library__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 + }, + "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 + }, + "user": { + "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": "nil", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "user.ads", + "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": "user", + "module": "", + "baseName": "user", + "mode": "C", + "prettyName": "user", + "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 + }, + "entry_point": { + "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": "code", + "sub": [ + { + "id": "nil", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "entry_point.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "5", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "3", + "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" + }, + "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": "user", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "arguments" + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "entry_point.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "5", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "3", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "statement": { + "id": "function_call", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "code", + "sub": [ + { + "id": "nil", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "entry_point.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "6", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "3", + "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": "library.ads", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "1", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "20", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "#default_value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#base_name": { + "id": "library__x", + "sub": [ + ], + "namedSub": { + } + }, + "#this": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#identifier": { + "id": "library__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": "library", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "arguments", + "sub": [ + { + "id": "constant", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "entry_point.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "6", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "12", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "value": { + "id": "FFFFFFFB", + "sub": [ + ], + "namedSub": { + } + } + } + } + ] + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "entry_point.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "6", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "3", + "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": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "entry_point.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "3", + "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": "entry_point", + "module": "", + "baseName": "entry_point", + "mode": "C", + "prettyName": "entry_point", + "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 + } + } +} diff --git a/regression/symtab2gb/multiple_symtabs/library.adb b/regression/symtab2gb/multiple_symtabs/library.adb new file mode 100644 index 00000000000..c54c2171730 --- /dev/null +++ b/regression/symtab2gb/multiple_symtabs/library.adb @@ -0,0 +1,7 @@ +procedure Library (X : Integer) is +begin + -- Failure + pragma Assert (X < 10); + -- Success + pragma Assert (X > 0); +end Library; diff --git a/regression/symtab2gb/multiple_symtabs/library.ads b/regression/symtab2gb/multiple_symtabs/library.ads new file mode 100644 index 00000000000..9a0ba3113ec --- /dev/null +++ b/regression/symtab2gb/multiple_symtabs/library.ads @@ -0,0 +1 @@ +procedure Library (X : Integer); diff --git a/regression/symtab2gb/multiple_symtabs/library.json_symtab b/regression/symtab2gb/multiple_symtabs/library.json_symtab new file mode 100644 index 00000000000..9ad44a40a7c --- /dev/null +++ b/regression/symtab2gb/multiple_symtabs/library.json_symtab @@ -0,0 +1,2294 @@ +{ + "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 + }, + "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 + }, + "library": { + "type": { + "id": "code", + "namedSub": { + "parameters": { + "id": "parameters", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "library.ads", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "1", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "20", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "#default_value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#base_name": { + "id": "library__x", + "sub": [ + ], + "namedSub": { + } + }, + "#this": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#identifier": { + "id": "library__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": "<", + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "library.ads", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "1", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "20", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "identifier": { + "id": "library__x", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "library.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "4", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "22", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "value": { + "id": "A", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "library.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "4", + "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": "library.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "4", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "3", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "statement": { + "id": "assert", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "code", + "sub": [ + { + "id": ">", + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "library.ads", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "1", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "20", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "identifier": { + "id": "library__x", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "library.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "6", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "22", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "value": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "library.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": "library.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "6", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "3", + "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": "library.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": "library", + "module": "", + "baseName": "library", + "mode": "C", + "prettyName": "library", + "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__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 + }, + "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 + }, + "library__x": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "library__x", + "module": "", + "baseName": "library__x", + "mode": "C", + "prettyName": "library__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 + }, + "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/symtab2gb/multiple_symtabs/test.desc b/regression/symtab2gb/multiple_symtabs/test.desc new file mode 100644 index 00000000000..8e91b64c60d --- /dev/null +++ b/regression/symtab2gb/multiple_symtabs/test.desc @@ -0,0 +1,10 @@ +CORE +entry_point.json_symtab +user.json_symtab library.json_symtab +^EXIT=10$ +^SIGNAL=0$ +^\[1\] file library.adb line \d+ assertion: FAILURE$ +^\[2\] file library.adb line \d+ assertion: FAILURE$ +^VERIFICATION FAILED$ +-- +error diff --git a/regression/symtab2gb/multiple_symtabs/user.adb b/regression/symtab2gb/multiple_symtabs/user.adb new file mode 100644 index 00000000000..fbaf59fb9c0 --- /dev/null +++ b/regression/symtab2gb/multiple_symtabs/user.adb @@ -0,0 +1,6 @@ +with Library; + +procedure User is +begin + Library (11); +end User; diff --git a/regression/symtab2gb/multiple_symtabs/user.ads b/regression/symtab2gb/multiple_symtabs/user.ads new file mode 100644 index 00000000000..b1e31409573 --- /dev/null +++ b/regression/symtab2gb/multiple_symtabs/user.ads @@ -0,0 +1 @@ +procedure User; diff --git a/regression/symtab2gb/multiple_symtabs/user.json_symtab b/regression/symtab2gb/multiple_symtabs/user.json_symtab new file mode 100644 index 00000000000..768a8bfa964 --- /dev/null +++ b/regression/symtab2gb/multiple_symtabs/user.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 + }, + "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 + }, + "library": { + "type": { + "id": "code", + "namedSub": { + "parameters": { + "id": "parameters", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "library.ads", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "1", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "20", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "#default_value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#base_name": { + "id": "library__x", + "sub": [ + ], + "namedSub": { + } + }, + "#this": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#identifier": { + "id": "library__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": "library.ads", + "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": "library", + "module": "", + "baseName": "library", + "mode": "C", + "prettyName": "library", + "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__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 + }, + "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 + }, + "library__x": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "library__x", + "module": "", + "baseName": "library__x", + "mode": "C", + "prettyName": "library__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 + }, + "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 + }, + "user": { + "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": "code", + "sub": [ + { + "id": "nil", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "user.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "5", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "3", + "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": "library.ads", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "1", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "20", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "#default_value": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#base_name": { + "id": "library__x", + "sub": [ + ], + "namedSub": { + } + }, + "#this": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "#identifier": { + "id": "library__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": "library", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "arguments", + "sub": [ + { + "id": "constant", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "user.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "5", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "12", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "value": { + "id": "B", + "sub": [ + ], + "namedSub": { + } + } + } + } + ] + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "user.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "5", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "3", + "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": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "user.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "3", + "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": "user", + "module": "", + "baseName": "user", + "mode": "C", + "prettyName": "user", + "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 + } + } +} diff --git a/regression/symtab2gb/single_symtab/README.md b/regression/symtab2gb/single_symtab/README.md new file mode 100644 index 00000000000..44fcc070a78 --- /dev/null +++ b/regression/symtab2gb/single_symtab/README.md @@ -0,0 +1,7 @@ +The `entry_point.json_symtab` in this directory was created from the Ada source +file `entry_point.adb` using the +[gnat2goto](https://github.com/diffblue/gnat2goto) compiler. + +``` +gnat2goto entry_point.adb +``` diff --git a/regression/symtab2gb/single_symtab/entry_point.adb b/regression/symtab2gb/single_symtab/entry_point.adb new file mode 100644 index 00000000000..5b175d7125e --- /dev/null +++ b/regression/symtab2gb/single_symtab/entry_point.adb @@ -0,0 +1,8 @@ +procedure Entry_Point is + X : constant Integer := 11; +begin + -- Failure + pragma Assert (X < 10); + -- Success + pragma Assert (X > 0); +end Entry_Point; diff --git a/regression/symtab2gb/single_symtab/entry_point.json_symtab b/regression/symtab2gb/single_symtab/entry_point.json_symtab new file mode 100644 index 00000000000..8276db2cdf0 --- /dev/null +++ b/regression/symtab2gb/single_symtab/entry_point.json_symtab @@ -0,0 +1,3090 @@ +{ + "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 + }, + "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 + }, + "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": "bool" + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "identifier": { + "id": "standard__boolean__true", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "typecast", + "sub": [ + { + "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": "1", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "bool" + }, + "range_check": { + "id": "0", + "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": "bool" + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "identifier": { + "id": "standard__boolean__false", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "typecast", + "sub": [ + { + "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": "0", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "bool" + }, + "range_check": { + "id": "0", + "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": "entry_point", + "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 + }, + "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 + }, + "standard__boolean__false": { + "type": { + "id": "bool" + }, + "value": { + "id": "nil", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__boolean__false", + "module": "", + "baseName": "standard__boolean__false", + "mode": "C", + "prettyName": "standard__boolean__false", + "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 + }, + "__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__boolean__true": { + "type": { + "id": "bool" + }, + "value": { + "id": "nil", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "standard__boolean__true", + "module": "", + "baseName": "standard__boolean__true", + "mode": "C", + "prettyName": "standard__boolean__true", + "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__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 + }, + "entry_point__x": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "value": { + "id": "nil", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "entry_point.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "2", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "3", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "location": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "name": "entry_point__x", + "module": "", + "baseName": "entry_point__x", + "mode": "C", + "prettyName": "entry_point__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 + }, + "entry_point": { + "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": "entry_point.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "2", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "3", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "identifier": { + "id": "entry_point__x", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "entry_point.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "2", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "3", + "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": "entry_point.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "2", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "3", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "identifier": { + "id": "entry_point__x", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "entry_point.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "2", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "27", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "32", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "value": { + "id": "B", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "entry_point.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "2", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "3", + "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": "symbol", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "bool" + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "identifier": { + "id": "standard__boolean__false", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "entry_point.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "4", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "3", + "sub": [ + ], + "namedSub": { + } + } + } + }, + "type": { + "id": "nil", + "sub": [ + ], + "namedSub": { + } + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "statement": { + "id": "assert", + "sub": [ + ], + "namedSub": { + } + } + } + }, + { + "id": "code", + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + } + }, + "type": { + "id": "bool" + }, + "range_check": { + "id": "0", + "sub": [ + ], + "namedSub": { + } + }, + "identifier": { + "id": "standard__boolean__true", + "sub": [ + ], + "namedSub": { + } + } + } + } + ], + "namedSub": { + "#source_location": { + "id": "source_location", + "sub": [ + ], + "namedSub": { + "file": { + "id": "entry_point.adb", + "sub": [ + ], + "namedSub": { + } + }, + "line": { + "id": "5", + "sub": [ + ], + "namedSub": { + } + }, + "column": { + "id": "3", + "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": "entry_point.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": "entry_point", + "module": "", + "baseName": "entry_point", + "mode": "C", + "prettyName": "entry_point", + "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 + } + } +} diff --git a/regression/symtab2gb/single_symtab/test.desc b/regression/symtab2gb/single_symtab/test.desc new file mode 100644 index 00000000000..317003031f5 --- /dev/null +++ b/regression/symtab2gb/single_symtab/test.desc @@ -0,0 +1,10 @@ +CORE +entry_point.json_symtab + +^EXIT=10$ +^SIGNAL=0$ +^\[1\] file entry_point.adb line \d+ assertion: FAILURE$ +^\[2\] file entry_point.adb line \d+ assertion: SUCCESS$ +^VERIFICATION FAILED$ +-- +error diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index ad059eb0ad8..d2c3dc2fdd5 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -104,3 +104,4 @@ add_subdirectory(goto-instrument) add_subdirectory(goto-analyzer) add_subdirectory(goto-diff) add_subdirectory(goto-harness) +add_subdirectory(symtab2gb) diff --git a/src/Makefile b/src/Makefile index 8cc57dda514..b2f49d510f1 100644 --- a/src/Makefile +++ b/src/Makefile @@ -19,6 +19,7 @@ DIRS = analyses \ linking \ pointer-analysis \ solvers \ + symtab2gb \ util \ xmllang \ # Empty last line @@ -29,6 +30,7 @@ all: cbmc.dir \ goto-diff.dir \ goto-instrument.dir \ goto-harness.dir \ + symtab2gb.dir \ # Empty last line ############################################################################### @@ -70,6 +72,8 @@ goto-diff.dir: languages goto-programs.dir pointer-analysis.dir \ goto-cc.dir: languages goto-programs.dir linking.dir +symtab2gb.dir: util.dir goto-programs.dir json-symtab-language.dir + # building for a particular directory $(patsubst %, %.dir, $(DIRS)): diff --git a/src/symtab2gb/CMakeLists.txt b/src/symtab2gb/CMakeLists.txt new file mode 100644 index 00000000000..0c1e9620d7c --- /dev/null +++ b/src/symtab2gb/CMakeLists.txt @@ -0,0 +1,11 @@ +add_executable(symtab2gb + symtab2gb_main.cpp + symtab2gb_parse_options.cpp + symtab2gb_parse_options.h) + +generic_includes(symtab2gb) + +target_link_libraries(symtab2gb + util + goto-programs + json-symtab-language) diff --git a/src/symtab2gb/Makefile b/src/symtab2gb/Makefile new file mode 100644 index 00000000000..dd18aaa51c0 --- /dev/null +++ b/src/symtab2gb/Makefile @@ -0,0 +1,35 @@ +SRC = \ + symtab2gb_main.cpp \ + symtab2gb_parse_options.cpp \ + # Empty last line + +OBJ += \ + ../util/util$(LIBEXT) \ + ../goto-programs/goto-programs$(LIBEXT) \ + ../big-int/big-int$(LIBEXT) \ + ../langapi/langapi$(LIBEXT) \ + ../linking/linking$(LIBEXT) \ + ../json/json$(LIBEXT) \ + ../json-symtab-language/json-symtab-language$(LIBEXT) \ + # Empty last line + +INCLUDES= -I .. + +LIBS = + +CLEANFILES = symtab2gb$(EXEEXT) + +include ../config.inc +include ../common + +all: symtab2gb$(EXEEXT) + +############################################################################### + +symtab2gb$(EXEEXT): $(OBJ) + $(LINKBIN) + +.PHONY: symtab2gb-mac-signed + +symtab2gb-mac-signed: symtab2gb$(EXEEXT) + codesign -v -s $(OSX_IDENTITY) symtab2gb2$(EXEEXT) diff --git a/src/symtab2gb/module_dependencies.txt b/src/symtab2gb/module_dependencies.txt new file mode 100644 index 00000000000..3c4e277c350 --- /dev/null +++ b/src/symtab2gb/module_dependencies.txt @@ -0,0 +1,3 @@ +util +json-symtab-language +goto-programs diff --git a/src/symtab2gb/symtab2gb_main.cpp b/src/symtab2gb/symtab2gb_main.cpp new file mode 100644 index 00000000000..db0f34943c6 --- /dev/null +++ b/src/symtab2gb/symtab2gb_main.cpp @@ -0,0 +1,18 @@ +/******************************************************************\ + +Module: symtab2gb_main + +Author: Diffblue Ltd. + +\******************************************************************/ + +/// \file +/// symtab2gb Main Module + +#include "symtab2gb_parse_options.h" + +int main(int argc, const char *argv[]) +{ + symtab2gb_parse_optionst parse_options{argc, argv}; + return parse_options.main(); +} diff --git a/src/symtab2gb/symtab2gb_parse_options.cpp b/src/symtab2gb/symtab2gb_parse_options.cpp new file mode 100644 index 00000000000..da3de863218 --- /dev/null +++ b/src/symtab2gb/symtab2gb_parse_options.cpp @@ -0,0 +1,138 @@ +/******************************************************************\ + +Module: symtab2gb_parse_options + +Author: Diffblue Ltd. + +\******************************************************************/ + +#include "symtab2gb_parse_options.h" + +#include +#include +#include + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +symtab2gb_parse_optionst::symtab2gb_parse_optionst(int argc, const char *argv[]) + : parse_options_baset{SYMTAB2GB_OPTIONS, + argc, + argv, + std::string("SYMTAB2GB ") + CBMC_VERSION} +{ +} + +static inline bool failed(bool error_indicator) +{ + return error_indicator; +} + +static void run_symtab2gb( + const std::vector &symtab_filenames, + const std::string &gb_filename) +{ + // try opening all the files first to make sure we can + // even read/write what we want + std::ofstream out_file{gb_filename, std::ios::binary}; + if(!out_file.is_open()) + { + throw system_exceptiont{"couldn't open output file `" + gb_filename + "'"}; + } + std::vector symtab_files; + for(auto const &symtab_filename : symtab_filenames) + { + std::ifstream symtab_file{symtab_filename}; + if(!symtab_file.is_open()) + { + throw system_exceptiont{"couldn't open input file `" + symtab_filename + + "'"}; + } + symtab_files.emplace_back(std::move(symtab_file)); + } + + stream_message_handlert message_handler{std::cerr}; + + auto const symtab_language = new_json_symtab_language(); + symtab_language->set_message_handler(message_handler); + + goto_modelt linked_goto_model{}; + + for(std::size_t ix = 0; ix < symtab_files.size(); ++ix) + { + auto const &symtab_filename = symtab_filenames[ix]; + auto &symtab_file = symtab_files[ix]; + if(failed(symtab_language->parse(symtab_file, symtab_filename))) + { + throw invalid_source_file_exceptiont{ + "failed to parse symbol table from file `" + symtab_filename + "'"}; + } + symbol_tablet symtab{}; + if(failed(symtab_language->typecheck(symtab, ""))) + { + throw invalid_source_file_exceptiont{ + "failed to typecheck symbol table from file `" + symtab_filename + "'"}; + } + goto_modelt goto_model{}; + goto_model.symbol_table = symtab; + goto_convert(goto_model, message_handler); + link_goto_model(linked_goto_model, goto_model, message_handler); + } + if(failed(write_goto_binary(out_file, linked_goto_model))) + { + throw system_exceptiont{"failed to write goto binary to " + gb_filename}; + } +} + +int symtab2gb_parse_optionst::doit() +{ + if(cmdline.isset("version")) + { + log.status() << CBMC_VERSION << '\n'; + return CPROVER_EXIT_SUCCESS; + } + if(cmdline.args.empty()) + { + throw invalid_command_line_argument_exceptiont{ + "expect at least one input file", ""}; + } + std::vector symtab_filenames = cmdline.args; + std::string gb_filename = "a.out"; + if(cmdline.isset(SYMTAB2GB_OUT_FILE_OPT)) + { + gb_filename = cmdline.get_value(SYMTAB2GB_OUT_FILE_OPT); + } + run_symtab2gb(symtab_filenames, gb_filename); + return CPROVER_EXIT_SUCCESS; +} + +void symtab2gb_parse_optionst::help() +{ + log.status() + << '\n' + << banner_string("symtab2gb", CBMC_VERSION) << '\n' + << align_center_with_border("Copyright (C) 2019") << '\n' + << align_center_with_border("Diffblue Ltd.") << '\n' + << align_center_with_border("info@diffblue.com") << '\n' + << '\n' + << "Usage: Purpose:\n" + << '\n' + << "symtab2gb [-?] [-h] [--help] show help\n" + "symtab2gb compile .json_symtabs\n" + " + to a single goto-binary\n" + " [--out ]\n\n" + " a CBMC symbol table in\n" + " JSON format\n" + "--out specify the filename of\n" + " the resulting binary\n" + " (default: a.out)\n" + << messaget::eom; +} diff --git a/src/symtab2gb/symtab2gb_parse_options.h b/src/symtab2gb/symtab2gb_parse_options.h new file mode 100644 index 00000000000..546af8bb085 --- /dev/null +++ b/src/symtab2gb/symtab2gb_parse_options.h @@ -0,0 +1,32 @@ +/******************************************************************\ + +Module: symtab2gb_parse_options + +Author: Diffblue Ltd. + +\******************************************************************/ + +#ifndef CPROVER_SYMTAB2GB_SYMTAB2GB_PARSE_OPTIONS_H +#define CPROVER_SYMTAB2GB_SYMTAB2GB_PARSE_OPTIONS_H + +#include + +#define SYMTAB2GB_OUT_FILE_OPT "out" + +// clang-format off + +#define SYMTAB2GB_OPTIONS \ + "(" SYMTAB2GB_OUT_FILE_OPT "):" \ +// end options + +// clang-format on + +class symtab2gb_parse_optionst : public parse_options_baset +{ +public: + symtab2gb_parse_optionst(int argc, const char *argv[]); + void help() override; + int doit() override; +}; + +#endif // CPROVER_SYMTAB2GB_SYMTAB2GB_PARSE_OPTIONS_H