@@ -67,31 +67,35 @@ void dfcc_swap_and_wrapt::swap_and_wrap(
6767 std::set<irep_idt> &function_pointer_contracts,
6868 bool allow_recursive_calls)
6969{
70- auto found = cache.find (function_id);
71- if (found != cache.end ())
72- {
73- auto &pair = found->second ;
70+ auto pair = cache.insert ({function_id, {contract_id, contract_mode}});
71+ auto inserted = pair.second ;
7472
73+ if (!inserted)
74+ {
75+ auto old_contract_id = pair.first ->second .first ;
76+ auto old_contract_mode = pair.first ->second .second ;
77+
78+ // different swapp already performed, abort
79+ if (old_contract_id != contract_id || old_contract_mode != contract_mode)
80+ {
81+ auto mode1 = (old_contract_mode == dfcc_contract_modet::REPLACE)
82+ ? " REPLACE"
83+ : " CHECK" ;
84+ auto mode2 =
85+ (contract_mode == dfcc_contract_modet::REPLACE) ? " REPLACE" : " CHECK)" ;
86+
87+ std::ostringstream err_msg;
88+ err_msg << " DFCC: multiple attempts to swap and wrap function '"
89+ << function_id << " ':\n " ;
90+ err_msg << " - with '" << old_contract_id << " ' in mode " << mode1 << " \n " ;
91+ err_msg << " - with '" << contract_id << " ' in mode " << mode2 << " \n " ;
92+ throw invalid_input_exceptiont (err_msg.str ());
93+ }
7594 // same swap already performed
76- if (pair.first == contract_id && pair.second == contract_mode)
77- return ;
78-
79- // already swapped with something else, abort
80- auto mode1 =
81- (pair.second == dfcc_contract_modet::REPLACE) ? " REPLACE" : " CHECK" ;
82- auto mode2 =
83- (contract_mode == dfcc_contract_modet::REPLACE) ? " REPLACE" : " CHECK)" ;
84-
85- std::ostringstream err_msg;
86- err_msg << " DFCC: multiple attempts to swap and wrap function '"
87- << function_id << " ':\n " ;
88- err_msg << " - with '" << pair.first << " ' in mode " << mode1 << " \n " ;
89- err_msg << " - with '" << contract_id << " ' in mode " << mode2 << " \n " ;
90- throw invalid_input_exceptiont (err_msg.str ());
95+ return ;
9196 }
9297
93- cache.insert ({function_id, {contract_id, contract_mode}});
94-
98+ // actually perform the translation
9599 switch (contract_mode)
96100 {
97101 case dfcc_contract_modet::CHECK:
0 commit comments