@@ -1029,38 +1029,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
1029
1029
// all checks supported by goto_check
1030
1030
PARSE_OPTIONS_GOTO_CHECK (cmdline, options);
1031
1031
1032
- // unwind loops
1033
- if (cmdline.isset (" unwind" ))
1034
- {
1035
- log.status () << " Unwinding loops" << messaget::eom;
1036
- options.set_option (" unwind" , cmdline.get_value (" unwind" ));
1037
- }
1038
-
1039
- {
1040
- parse_function_pointer_restriction_options_from_cmdline (cmdline, options);
1041
-
1042
- if (
1043
- options.is_set (RESTRICT_FUNCTION_POINTER_OPT) ||
1044
- options.is_set (RESTRICT_FUNCTION_POINTER_BY_NAME_OPT) ||
1045
- options.is_set (RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT))
1046
- {
1047
- label_function_pointer_call_sites (goto_model);
1048
-
1049
- restrict_function_pointers (ui_message_handler, goto_model, options);
1050
- }
1051
- }
1052
-
1053
- // skip over selected loops
1054
- if (cmdline.isset (" skip-loops" ))
1055
- {
1056
- log.status () << " Adding gotos to skip loops" << messaget::eom;
1057
- if (skip_loops (
1058
- goto_model, cmdline.get_value (" skip-loops" ), ui_message_handler))
1059
- throw 0 ;
1060
- }
1061
-
1062
- namespacet ns (goto_model.symbol_table );
1063
-
1064
1032
// initialize argv with valid pointers
1065
1033
if (cmdline.isset (" model-argc-argv" ))
1066
1034
{
@@ -1096,6 +1064,10 @@ void goto_instrument_parse_optionst::instrument_goto_program()
1096
1064
std::string (CPROVER_PREFIX) + " CUSTOM_BITVECTOR_ANALYSIS" );
1097
1065
}
1098
1066
1067
+ // remove inline assembler as that may yield further library function calls
1068
+ // that need to be resolved
1069
+ remove_asm (goto_model);
1070
+
1099
1071
// add the library
1100
1072
log.status () << " Adding CPROVER library (" << config.ansi_c .arch << " )"
1101
1073
<< messaget::eom;
@@ -1104,6 +1076,31 @@ void goto_instrument_parse_optionst::instrument_goto_program()
1104
1076
link_to_library (goto_model, ui_message_handler, cprover_c_library_factory);
1105
1077
}
1106
1078
1079
+ {
1080
+ parse_function_pointer_restriction_options_from_cmdline (cmdline, options);
1081
+
1082
+ if (
1083
+ options.is_set (RESTRICT_FUNCTION_POINTER_OPT) ||
1084
+ options.is_set (RESTRICT_FUNCTION_POINTER_BY_NAME_OPT) ||
1085
+ options.is_set (RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT))
1086
+ {
1087
+ label_function_pointer_call_sites (goto_model);
1088
+
1089
+ restrict_function_pointers (ui_message_handler, goto_model, options);
1090
+ }
1091
+ }
1092
+
1093
+ // skip over selected loops
1094
+ if (cmdline.isset (" skip-loops" ))
1095
+ {
1096
+ log.status () << " Adding gotos to skip loops" << messaget::eom;
1097
+ if (skip_loops (
1098
+ goto_model, cmdline.get_value (" skip-loops" ), ui_message_handler))
1099
+ {
1100
+ throw 0 ;
1101
+ }
1102
+ }
1103
+
1107
1104
// now do full inlining, if requested
1108
1105
if (cmdline.isset (" inline" ))
1109
1106
{
@@ -1420,6 +1417,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
1420
1417
do_indirect_call_and_rtti_removal ();
1421
1418
1422
1419
log.status () << " Pointer Analysis" << messaget::eom;
1420
+ const namespacet ns (goto_model.symbol_table );
1423
1421
value_set_analysist value_set_analysis (ns);
1424
1422
value_set_analysis (goto_model.goto_functions );
1425
1423
0 commit comments