Skip to content

Commit 40983dd

Browse files
Make property identifiers in output of --show-properties consistent
The same property given as argument to --property had a different name when displayed with --show-properties after using --full-slice in the same invocation of goto-instrument. Property identifiers should at least be consistent w.r.t. input arguments and log file output in the same invocation of a tool. However, the consistency ends as soon as a goto binary is stored and used (where they are relabelled). This could be fixed by storing property identifiers and preventing them from being touched after loading a goto binary.
1 parent a9b4514 commit 40983dd

File tree

1 file changed

+0
-3
lines changed

1 file changed

+0
-3
lines changed

src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1417,9 +1417,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
14171417
full_slicer(goto_functions, ns);
14181418
}
14191419

1420-
// label the assertions
1421-
label_properties(goto_functions);
1422-
14231420
// recalculate numbers, etc.
14241421
goto_functions.update();
14251422
}

0 commit comments

Comments
 (0)