From 7eaf1579bb8c41336ddbddb3781c5a5fc47be724 Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Mon, 18 Mar 2019 13:08:51 +0000 Subject: [PATCH 1/4] Havoc global variables in memory snapshot harness Basically just grabs a list of var-names from command line and calls recursive initialize on them instead of assigning their value. --- .../memory_snapshot_harness_generator.cpp | 24 +++++++++++++++---- .../memory_snapshot_harness_generator.h | 13 +++++++--- 2 files changed, 30 insertions(+), 7 deletions(-) diff --git a/src/goto-harness/memory_snapshot_harness_generator.cpp b/src/goto-harness/memory_snapshot_harness_generator.cpp index 47c23c2a318..d4451d044cc 100644 --- a/src/goto-harness/memory_snapshot_harness_generator.cpp +++ b/src/goto-harness/memory_snapshot_harness_generator.cpp @@ -24,6 +24,7 @@ Author: Daniel Poetzl #include #include "goto_harness_generator_factory.h" +#include "recursive_initialization.h" void memory_snapshot_harness_generatort::handle_option( const std::string &option, @@ -56,6 +57,10 @@ void memory_snapshot_harness_generatort::handle_option( location_number = optionalt(safe_string2unsigned(start.back())); } } + else if(option == "havoc-variables") + { + variables_to_havoc.insert(values.begin(), values.end()); + } else { throw invalid_command_line_argument_exceptiont( @@ -196,17 +201,27 @@ void memory_snapshot_harness_generatort::add_init_section( } code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals( - const symbol_tablet &snapshot) const + const symbol_tablet &snapshot, + goto_modelt &goto_model) const { + recursive_initializationt recursive_initialization{ + recursive_initialization_configt{}, goto_model}; + code_blockt code; for(const auto &pair : snapshot) { const symbolt &symbol = pair.second; - if(!symbol.is_static_lifetime) continue; - code.add(code_assignt{symbol.symbol_expr(), symbol.value}); + if(variables_to_havoc.count(symbol.base_name) == 0) + { + code.add(code_assignt{symbol.symbol_expr(), symbol.value}); + } + else + { + recursive_initialization.initialize(symbol.symbol_expr(), 0, {}, code); + } } return code; } @@ -312,7 +327,8 @@ void memory_snapshot_harness_generatort::generate( add_init_section(goto_model); - code_blockt harness_function_body = add_assignments_to_globals(snapshot); + code_blockt harness_function_body = + add_assignments_to_globals(snapshot, goto_model); add_call_with_nondet_arguments( *called_function_symbol, harness_function_body); diff --git a/src/goto-harness/memory_snapshot_harness_generator.h b/src/goto-harness/memory_snapshot_harness_generator.h index fac5f6484e9..1e8a324d9fa 100644 --- a/src/goto-harness/memory_snapshot_harness_generator.h +++ b/src/goto-harness/memory_snapshot_harness_generator.h @@ -19,9 +19,12 @@ Author: Daniel Poetzl #include #include +// clang-format off #define MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS \ "(memory-snapshot):" \ - "(initial-location):" // MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS + "(initial-location):" \ + "(havoc-variables):" // MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS +// clang-format on // clang-format off #define MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP \ @@ -31,6 +34,8 @@ Author: Daniel Poetzl "--initial-location ]>\n" \ " use given function and location number as " \ "entry\n point\n" \ + "--havoc-variables vars initialise variables from vars to\n" \ + " non-deterministic values" \ // MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP // clang-format on @@ -61,8 +66,9 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort void add_init_section(goto_modelt &goto_model) const; - code_blockt add_assignments_to_globals(const symbol_tablet &snapshot) const; - + code_blockt add_assignments_to_globals( + const symbol_tablet &snapshot, + goto_modelt &goto_model) const; void add_call_with_nondet_arguments( const symbolt &called_function_symbol, code_blockt &code) const; @@ -75,6 +81,7 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort irep_idt entry_function_name; optionalt location_number; + std::unordered_set variables_to_havoc; message_handlert &message_handler; }; From 6ca35c2fcb9cff1200b308295f03138384f147f1 Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Mon, 18 Mar 2019 13:09:26 +0000 Subject: [PATCH 2/4] Add documentation to memory snapshot harness Code level documentation for the class methods. --- .../memory_snapshot_harness_generator.h | 69 +++++++++++++++++++ 1 file changed, 69 insertions(+) diff --git a/src/goto-harness/memory_snapshot_harness_generator.h b/src/goto-harness/memory_snapshot_harness_generator.h index 1e8a324d9fa..1568932d1a6 100644 --- a/src/goto-harness/memory_snapshot_harness_generator.h +++ b/src/goto-harness/memory_snapshot_harness_generator.h @@ -51,28 +51,97 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort { } + /// The main function of this harness, consists of the following: + /// 1. Load memory table from the snapshot. + /// 2. Add initial section to the user-specified initial location. + /// 3. Assign global variables their snapshot values (via the harness + /// function). + /// 4. Insert call of the initial location (with nondet values) into the + /// harness function. + /// 5. Build symbol for the harness functions. + /// 6. Insert harness function into \p goto_model. + /// \param goto_model: goto model to be modified + /// \param harness_function_name: name of the resulting harness function void generate(goto_modelt &goto_model, const irep_idt &harness_function_name) override; protected: + /// Collect the memory-snapshot specific cmdline options (one at a time) + /// \param option: memory-snapshot | initial-location | havoc-variables + /// \param values: list of arguments related to a given option void handle_option( const std::string &option, const std::list &values) override; + /// Check that user options make sense: + /// On their own, e.g. location number cannot be specified without a function. + /// In relation to the input program, e.g. function name must be known via + /// the symbol table. + /// \param goto_model: the model containing the symbol table, goto functions, + /// etc. void validate_options(const goto_modelt &goto_model) override; + /// Parse the snapshot JSON file and initialise the symbol table + /// \param file: the snapshot JSON file + /// \param snapshot: the resulting symbol table built from the snapshot void get_memory_snapshot(const std::string &file, symbol_tablet &snapshot) const; + /// Modify the entry-point function to start from the user-specified initial + /// location. + /// Turn this: + /// + /// int foo() { + /// ..first_part.. + /// i: //location_number=i + /// ..second_part.. + /// } + /// + /// Into this: + /// + /// func_init_done; + /// __CPROVER_initialize() { + /// ... + /// func_init_done = false; + /// } + /// int foo() { + /// if (func_init_done) goto 1; + /// func_init_done = true; + /// goto i; + /// 1: ; + /// ..first_part.. + /// i: //location_number=i + /// ..second_part.. + /// } + /// + /// \param goto_model: Model where the modification takes place void add_init_section(goto_modelt &goto_model) const; + /// For each global symbol in the \p snapshot symbol table either: + /// 1) add \ref code_assignt assigning a value from the \p snapshot to the + /// symbol + /// or + /// 2) recursively initialise the symbol to a non-deterministic value of the + /// right type + /// \param snapshot: snapshot to load the symbols and their values from + /// \param goto_model: model to initialise the havoc-ing + /// \return the block of code where the assignments are added code_blockt add_assignments_to_globals( const symbol_tablet &snapshot, goto_modelt &goto_model) const; + + /// Create as many non-deterministic arguments as there are arguments of the + /// \p called_function_symbol and add a function call with those arguments + /// \param called_function_symbol: the function to be called + /// \param code: the block of code where the function call is added void add_call_with_nondet_arguments( const symbolt &called_function_symbol, code_blockt &code) const; + /// Insert the \p function into the symbol table (and the goto functions map) + /// of the \p goto_model + /// \param goto_model: goto model where the insertion is to take place + /// \param function: symbol of the function to be inserted void insert_harness_function_into_goto_model( goto_modelt &goto_model, const symbolt &function) const; From fce288d0e947daf5e3b18f4f47902156a62be0b1 Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Mon, 18 Mar 2019 13:09:38 +0000 Subject: [PATCH 3/4] Add cprover manual entry Covering memory-snapshot harness, but not the memory analyzer. --- doc/cprover-manual/goto-harness.md | 104 ++++++++++++++++++++++++++++- 1 file changed, 102 insertions(+), 2 deletions(-) diff --git a/doc/cprover-manual/goto-harness.md b/doc/cprover-manual/goto-harness.md index 4bdf0b37194..f7ae8fb5032 100644 --- a/doc/cprover-manual/goto-harness.md +++ b/doc/cprover-manual/goto-harness.md @@ -13,9 +13,10 @@ having to manually construct an appropriate environment. We have two types of harnesses we can generate for now: -* The `memory-snapshot` harness. TODO: Daniel can document this. * The `function-call` harness, which automatically synthesises an environment without having any information about the program state. +* The `memory-snapshot` harness, which loads an existing program state (in form +of a JSON file) and selectively _havoc-ing_ some variables. It is used similarly to how `goto-instrument` is used by modifying an existing GOTO binary, as produced by `goto-cc`. @@ -309,4 +310,103 @@ main.c function function ** 0 of 1 failed (1 iterations) VERIFICATION SUCCESSFUL -``` \ No newline at end of file +``` + +### The memory snapshot harness + +The `function-call` harness is used in situations in which we want the analysed +function to work in arbitrary environment. If we want to analyse a function +starting from a _real_ program state, we can call the `memory-snapshot` harness +instead. + +Furthermore, the program state of interest may be taken at a particular location +within a function. In that case we do not want the harness to instrument the +whole function but rather to allow starting the execution from a specific +initial location (specified via `--initial-location func[:]`). Note that the +initial location does not have to be the first instruction of a function: we can +also specify the _location number_ `n` to set the initial location inside our +function. The _location numbers_ do not have to coincide with the lines of the +program code. To find the _location number_ run CBMC with +`--show-goto-functions`. Most commonly, the _location number_ is the instruction +of the break-point used to extract the program state for the memory snapshot. + +Say we want to check the assertion in the following code: + +```C +// main.c +#include + +unsigned int x; +unsigned int y; + +unsigned int nondet_int() { + unsigned int z; + return z; +} + +void checkpoint() {} + +unsigned int complex_function_which_returns_one() { + unsigned int i = 0; + while(++i < 1000001) { + if(nondet_int() && ((i & 1) == 1)) + break; + } + return i & 1; +} + +void fill_array(unsigned int* arr, unsigned int size) { + for (unsigned int i = 0; i < size; i++) + arr[i]=nondet_int(); +} + +unsigned int array_sum(unsigned int* arr, unsigned int size) { + unsigned int sum = 0; + for (unsigned int i = 0; i < size; i++) + sum += arr[i]; + return sum; +} + +const unsigned int array_size = 100000; + +int main() { + x = complex_function_which_returns_one(); + unsigned int large_array[array_size]; + fill_array(large_array, array_size); + y = array_sum(large_array, array_size); + checkpoint(); + assert(y + 2 > x); + return 0; +} +``` + +But are not particularly interested in analysing the complex function, since we +trust that its implementation is correct. Hence we run the above program +stopping after the assignments to `x` and `x` and storing the program state, +e.g. using the `memory-analyzer`, in a JSON file `snapshot.json`. Then run the +harness and verify the assertion with: + +``` +$ goto-cc -o main.gb main.c +$ goto-harness \ + --harness-function-name harness \ + --harness-type initialise-with-memory-snapshot \ + --memory-snapshot snapshot.json \ + --initial-location checkpoint \ + --havoc-variables x \ + main.gb main-mod.gb +$ cbmc --function harness main-mod.gb +``` + +This will result in: + +``` +[...] + +** Results: +main.c function main +[main.assertion.1] line 42 assertion y + 2 > x: SUCCESS + +** 0 of 1 failed (1 iterations) +VERIFICATION SUCCESSFUL +``` From ceaafdfd1a3cfcf90657fbf908c363bf6126968e Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Mon, 18 Mar 2019 13:23:05 +0000 Subject: [PATCH 4/4] Add regression tests For global int, global struct, multiple snapshot-ed symbols, multiple havoc-ed symbols. --- .../goto-harness/havoc-global-int-01/main.c | 8 + .../havoc-global-int-01/test.desc | 8 + .../goto-harness/havoc-global-int-02/main.c | 53 +++ .../havoc-global-int-02/test.desc | 9 + .../goto-harness/havoc-global-struct/main.c | 21 ++ .../havoc-global-struct/test.desc | 8 + .../global-int-x-y-snapshot.json | 212 +++++++++++ .../global-struct-snapshot.json | 357 ++++++++++++++++++ 8 files changed, 676 insertions(+) create mode 100644 regression/goto-harness/havoc-global-int-01/main.c create mode 100644 regression/goto-harness/havoc-global-int-01/test.desc create mode 100644 regression/goto-harness/havoc-global-int-02/main.c create mode 100644 regression/goto-harness/havoc-global-int-02/test.desc create mode 100644 regression/goto-harness/havoc-global-struct/main.c create mode 100644 regression/goto-harness/havoc-global-struct/test.desc create mode 100644 regression/goto-harness/load-snapshot-json-snapshots/global-int-x-y-snapshot.json create mode 100644 regression/goto-harness/load-snapshot-json-snapshots/global-struct-snapshot.json diff --git a/regression/goto-harness/havoc-global-int-01/main.c b/regression/goto-harness/havoc-global-int-01/main.c new file mode 100644 index 00000000000..429359bc030 --- /dev/null +++ b/regression/goto-harness/havoc-global-int-01/main.c @@ -0,0 +1,8 @@ +int x = 1; + +int main() +{ + assert(x == 1); + + return 0; +} diff --git a/regression/goto-harness/havoc-global-int-01/test.desc b/regression/goto-harness/havoc-global-int-01/test.desc new file mode 100644 index 00000000000..621decdd139 --- /dev/null +++ b/regression/goto-harness/havoc-global-int-01/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-location main:0 --havoc-variables x +^EXIT=10$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion x == 1: FAILURE +-- +^warning: ignoring diff --git a/regression/goto-harness/havoc-global-int-02/main.c b/regression/goto-harness/havoc-global-int-02/main.c new file mode 100644 index 00000000000..747f3435368 --- /dev/null +++ b/regression/goto-harness/havoc-global-int-02/main.c @@ -0,0 +1,53 @@ +#include + +unsigned int x; +unsigned int y; + +unsigned int nondet_int() +{ + unsigned int z; + return z; +} + +void checkpoint() +{ +} + +unsigned int complex_function_which_returns_one() +{ + unsigned int i = 0; + while(++i < 1000001) + { + if(nondet_int() && ((i & 1) == 1)) + break; + } + return i & 1; +} + +void fill_array(unsigned int *arr, unsigned int size) +{ + for(unsigned int i = 0; i < size; i++) + arr[i] = nondet_int(); +} + +unsigned int array_sum(unsigned int *arr, unsigned int size) +{ + unsigned int sum = 0; + for(unsigned int i = 0; i < size; i++) + sum += arr[i]; + return sum; +} + +const unsigned int array_size = 100000; + +int main() +{ + x = complex_function_which_returns_one(); + unsigned int large_array[array_size]; + fill_array(large_array, array_size); + y = array_sum(large_array, array_size); + checkpoint(); + assert(y + 2 > y); //y is nondet -- may overflow + assert(0); + return 0; +} diff --git a/regression/goto-harness/havoc-global-int-02/test.desc b/regression/goto-harness/havoc-global-int-02/test.desc new file mode 100644 index 00000000000..a1243f319fc --- /dev/null +++ b/regression/goto-harness/havoc-global-int-02/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-y-snapshot.json --initial-location main:9 --havoc-variables y +^\[main.assertion.1\] line \d+ assertion y \+ 2 > y: FAILURE$ +^\[main.assertion.2\] line \d+ assertion 0: FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/goto-harness/havoc-global-struct/main.c b/regression/goto-harness/havoc-global-struct/main.c new file mode 100644 index 00000000000..30af7e78645 --- /dev/null +++ b/regression/goto-harness/havoc-global-struct/main.c @@ -0,0 +1,21 @@ +#include + +struct simple_str +{ + int i; + int j; +} simple; + +void checkpoint() +{ +} + +int main() +{ + simple.i = 1; + simple.j = 2; + + checkpoint(); + assert(simple.j > simple.i); + return 0; +} diff --git a/regression/goto-harness/havoc-global-struct/test.desc b/regression/goto-harness/havoc-global-struct/test.desc new file mode 100644 index 00000000000..4d85c4c6be7 --- /dev/null +++ b/regression/goto-harness/havoc-global-struct/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-struct-snapshot.json --initial-location main:3 --havoc-variables simple +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.1\] line \d+ assertion simple.j > simple.i: FAILURE$ +-- +^warning: ignoring diff --git a/regression/goto-harness/load-snapshot-json-snapshots/global-int-x-y-snapshot.json b/regression/goto-harness/load-snapshot-json-snapshots/global-int-x-y-snapshot.json new file mode 100644 index 00000000000..b3d9d7936f9 --- /dev/null +++ b/regression/goto-harness/load-snapshot-json-snapshots/global-int-x-y-snapshot.json @@ -0,0 +1,212 @@ + { + "symbolTable": { + "__CPROVER_size_t": { + "baseName": "__CPROVER_size_t", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": true, + "isInput": false, + "isLvalue": false, + "isMacro": true, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": true, + "isType": true, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer" + } + } + }, + "mode": "C", + "module": "main", + "name": "__CPROVER_size_t", + "prettyName": "__CPROVER_size_t", + "prettyType": "__CPROVER_size_t", + "prettyValue": "", + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer" + } + } + }, + "#typedef": { + "id": "__CPROVER_size_t" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "nil" + } + }, + "x": { + "baseName": "x", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "main.c" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer" + } + } + }, + "mode": "C", + "module": "main", + "name": "x", + "prettyName": "x", + "prettyType": "unsigned int", + "prettyValue": "1u", + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "1" + } + } + } + }, + "y": { + "baseName": "y", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "main.c" + }, + "line": { + "id": "4" + }, + "working_directory": { + "id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer" + } + } + }, + "mode": "C", + "module": "main", + "name": "y", + "prettyName": "y", + "prettyType": "unsigned int", + "prettyValue": "0u", + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + } + } + } diff --git a/regression/goto-harness/load-snapshot-json-snapshots/global-struct-snapshot.json b/regression/goto-harness/load-snapshot-json-snapshots/global-struct-snapshot.json new file mode 100644 index 00000000000..0bc285444de --- /dev/null +++ b/regression/goto-harness/load-snapshot-json-snapshots/global-struct-snapshot.json @@ -0,0 +1,357 @@ + { + "symbolTable": { + "__CPROVER_size_t": { + "baseName": "__CPROVER_size_t", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": true, + "isInput": false, + "isLvalue": false, + "isMacro": true, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": true, + "isType": true, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer" + } + } + }, + "mode": "C", + "module": "main", + "name": "__CPROVER_size_t", + "prettyName": "__CPROVER_size_t", + "prettyType": "__CPROVER_size_t", + "prettyValue": "", + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer" + } + } + }, + "#typedef": { + "id": "__CPROVER_size_t" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "nil" + } + }, + "simple": { + "baseName": "simple", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "main.c" + }, + "line": { + "id": "6" + }, + "working_directory": { + "id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer" + } + } + }, + "mode": "C", + "module": "main", + "name": "simple", + "prettyName": "simple", + "prettyType": "struct simple_str", + "prettyValue": "{ .i=1, .j=2 }", + "type": { + "id": "struct_tag", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "main.c" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer" + } + } + }, + "identifier": { + "id": "tag-simple_str" + } + } + }, + "value": { + "id": "struct", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "main.c" + }, + "line": { + "id": "6" + }, + "working_directory": { + "id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer" + } + } + }, + "type": { + "id": "struct_tag", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "main.c" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer" + } + } + }, + "identifier": { + "id": "tag-simple_str" + } + } + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "1" + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "2" + } + } + } + ] + } + }, + "tag-simple_str": { + "baseName": "simple_str", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": false, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": true, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "main.c" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer" + } + } + }, + "mode": "C", + "module": "main", + "name": "tag-simple_str", + "prettyName": "struct simple_str", + "prettyType": "struct simple_str { signed int i; signed int j; }", + "prettyValue": "", + "type": { + "id": "struct", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "main.c" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer" + } + } + }, + "components": { + "id": "", + "sub": [ + { + "id": "", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "main.c" + }, + "line": { + "id": "4" + }, + "working_directory": { + "id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer" + } + } + }, + "name": { + "id": "i" + }, + "pretty_name": { + "id": "i" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + { + "id": "", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "main.c" + }, + "line": { + "id": "5" + }, + "working_directory": { + "id": "/home/diffblue/petr.bauch/code/cbmc/regression/memory-analyzer" + } + } + }, + "name": { + "id": "j" + }, + "pretty_name": { + "id": "j" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + ] + }, + "tag": { + "id": "simple_str" + } + } + }, + "value": { + "id": "nil" + } + } + } + }