Skip to content

Commit 9bf6ad4

Browse files
committed
Split dynamic objects right after they are created
There must be no code between creating dynamic objects (replace malloc) and splitting them into instances since if the code in between changes numbering of GOTO nodes, the split objects may have a different location number than the original objects (which contain also a concrete object). This may cause some trouble later, especially with the zones domain, when it would add differences between fields of objects that can never be allocated at the same time (have contradictory allocation guards). Such template rows would make the invariant incomputable, yielding false negative results.
1 parent 029dece commit 9bf6ad4

File tree

1 file changed

+1
-2
lines changed

1 file changed

+1
-2
lines changed

src/2ls/2ls_parse_options.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1113,6 +1113,7 @@ bool twols_parse_optionst::process_goto_program(
11131113
// Replace malloc
11141114
dynamic_objects=util_make_unique<dynamic_objectst>(goto_model);
11151115
dynamic_objects->replace_malloc(options.get_bool_option("pointer-check"));
1116+
dynamic_objects->generate_instances(options);
11161117

11171118
// Allow recording of mallocs and memory leaks
11181119
if(options.get_bool_option("pointer-check"))
@@ -1137,8 +1138,6 @@ bool twols_parse_optionst::process_goto_program(
11371138
inline_main(goto_model);
11381139
}
11391140

1140-
dynamic_objects->generate_instances(options);
1141-
11421141
if(!cmdline.isset("independent-properties"))
11431142
{
11441143
add_assumptions_after_assertions(goto_model);

0 commit comments

Comments
 (0)