address review comments

src/goto-instrument/contracts/dynamic-frames/dfcc.cpp

@@ -92,14 +92,14 @@ parse_function_contract_pair(const irep_idt &cli_flag)
   else if(split.size() == 2)
   {
     auto function_name = split[0];
-    if(function_name.size() == 0)
+    if(function_name.empty())
     {
       throw invalid_function_contract_pair_exceptiont{
         "couldn't find function name before '/' in '" + cli_flag_str + "'",
         correct_format_message};
     }
     auto contract_name = split[1];
-    if(contract_name.size() == 0)
+    if(contract_name.empty())
     {
       throw invalid_function_contract_pair_exceptiont{
         "couldn't find contract name after '/' in '" + cli_flag_str + "'",

src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp

@@ -49,10 +49,11 @@ void dfcc_contract_clauses_codegent::gen_spec_assigns_instructions(
 {
   for(const auto &expr : assigns_clause)
   {
-    if(can_cast_expr<conditional_target_group_exprt>(expr))
+    if(
+      auto target_group =
+        expr_try_dynamic_cast<conditional_target_group_exprt>(expr))
     {
-      encode_assignable_target_group(
-        language_mode, to_conditional_target_group_expr(expr), dest);
+      encode_assignable_target_group(language_mode, *target_group, dest);
     }
     else
     {
@@ -75,10 +76,11 @@ void dfcc_contract_clauses_codegent::gen_spec_frees_instructions(
 {
   for(const auto &expr : frees_clause)
   {
-    if(can_cast_expr<conditional_target_group_exprt>(expr))
+    if(
+      auto target_group =
+        expr_try_dynamic_cast<conditional_target_group_exprt>(expr))
     {
-      encode_freeable_target_group(
-        language_mode, to_conditional_target_group_expr(expr), dest);
+      encode_freeable_target_group(language_mode, *target_group, dest);
     }
     else
     {
@@ -279,10 +281,9 @@ void dfcc_contract_clauses_codegent::inline_and_check_warnings(
   }
 
   INVARIANT(
-    recursive_call.size() == 0,
-    "recursive calls found when inlining goto program");
+    recursive_call.empty(), "recursive calls found when inlining goto program");
 
   INVARIANT(
-    not_enough_arguments.size() == 0,
+    not_enough_arguments.empty(),
     "not enough arguments when inlining goto program");
 }

src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp

@@ -162,9 +162,9 @@ void dfcc_spec_functionst::generate_havoc_instructions(
       if(ins_it->call_function().id() != ID_symbol)
       {
         throw invalid_source_file_exceptiont(
-          "Function pointer call '" +
+          "Function pointer calls are not supported in assigns clauses: '" +
             from_expr(ns, function_id, ins_it->call_function()) +
-            "' in function '" + id2string(function_id) + "' is not supported",
+            "' called in function '" + id2string(function_id) + "'",
           ins_it->source_location());
       }
 
@@ -265,21 +265,25 @@ void dfcc_spec_functionst::to_spec_assigns_function(
       .symbol_expr();
 
   to_spec_assigns_instructions(
-    write_set_to_fill, goto_function.body, nof_targets);
+    write_set_to_fill,
+    utils.get_function_symbol(function_id).mode,
+    goto_function.body,
+    nof_targets);
 
   goto_model.goto_functions.update();
 
   // instrument for side-effects checking
   std::set<irep_idt> function_pointer_contracts;
   instrument.instrument_function(function_id, function_pointer_contracts);
   INVARIANT(
-    function_pointer_contracts.size() == 0,
+    function_pointer_contracts.empty(),
     "discovered function pointer contracts unexpectedly");
   utils.set_hide(function_id, true);
 }
 
 void dfcc_spec_functionst::to_spec_assigns_instructions(
   const exprt &write_set_to_fill,
+  const irep_idt &language_mode,
   goto_programt &program,
   std::size_t &nof_targets)
 {
@@ -295,9 +299,9 @@ void dfcc_spec_functionst::to_spec_assigns_instructions(
       if(ins_it->call_function().id() != ID_symbol)
       {
         throw invalid_source_file_exceptiont(
-          "Function pointer call '" +
-            from_expr(ns, "", ins_it->call_function()) +
-            "' are supported in assigns clauses",
+          "Function pointer calls are not supported in assigns clauses '" +
+            from_expr_using_mode(ns, language_mode, ins_it->call_function()) +
+            "'",
           ins_it->source_location());
       }
 
@@ -350,22 +354,26 @@ void dfcc_spec_functionst::to_spec_frees_function(
       .symbol_expr();
 
   to_spec_frees_instructions(
-    write_set_to_fill, goto_function.body, nof_targets);
+    write_set_to_fill,
+    utils.get_function_symbol(function_id).mode,
+    goto_function.body,
+    nof_targets);
 
   goto_model.goto_functions.update();
 
   // instrument for side-effects checking
   std::set<irep_idt> function_pointer_contracts;
   instrument.instrument_function(function_id, function_pointer_contracts);
   INVARIANT(
-    function_pointer_contracts.size() == 0,
+    function_pointer_contracts.empty(),
     "discovered function pointer contracts unexpectedly");
 
   utils.set_hide(function_id, true);
 }
 
 void dfcc_spec_functionst::to_spec_frees_instructions(
   const exprt &write_set_to_fill,
+  const irep_idt &language_mode,
   goto_programt &program,
   std::size_t &nof_targets)
 {
@@ -378,9 +386,9 @@ void dfcc_spec_functionst::to_spec_frees_instructions(
       if(ins_it->call_function().id() != ID_symbol)
       {
         throw invalid_source_file_exceptiont(
-          "Function pointer call '" +
-            from_expr(ns, "", ins_it->call_function()) +
-            "' are not supported in frees clauses",
+          "Function pointer calls are not supported in frees clauses: '" +
+            from_expr_using_mode(ns, language_mode, ins_it->call_function()) +
+            "'",
           ins_it->source_location());
       }
 

src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h

@@ -152,11 +152,13 @@ class dfcc_spec_functionst
   /// `__CPROVER_object_from`, `__CPROVER_object_upto`.
   ///
   /// \param[in] write_set_to_fill write set to populate.
+  /// \param[in] language_mode used to format expressions.
   /// \param[inout] program function to transform in place
   /// \param[out] nof_targets receives the estimated size of the write set
   ///
   void to_spec_assigns_instructions(
     const exprt &write_set_to_fill,
+    const irep_idt &language_mode,
     goto_programt &program,
     std::size_t &nof_targets);
 
@@ -201,11 +203,13 @@ class dfcc_spec_functionst
   /// freeable targets: `__CPROVER_freeable`.
   ///
   /// \param[in] write_set_to_fill write set to populate.
+  /// \param[in] language_mode used to format expressions.
   /// \param[inout] program function to transform in place
   /// \param[out] nof_targets receives the estimated size of the write set
   ///
   void to_spec_frees_instructions(
     const exprt &write_set_to_fill,
+    const irep_idt &language_mode,
     goto_programt &program,
     std::size_t &nof_targets);
 

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

@@ -30,14 +30,6 @@ Author: Remi Delmas, delmasrd@amazon.com
 #include "dfcc_lift_memory_predicates.h"
 #include "dfcc_utils.h"
 
-/// Lift a c++ bool to an exprt
-static exprt to_bool_expr(bool v)
-{
-  if(v)
-    return true_exprt();
-  return false_exprt();
-}
-
 /// Generate the contract write set
 const symbol_exprt create_contract_write_set(
   dfcc_utilst &utils,
@@ -312,8 +304,8 @@ void dfcc_wrapper_programt::encode_requires_write_set()
     address_of_write_set,
     from_integer(0, size_type()),
     from_integer(0, size_type()),
-    to_bool_expr(check_mode),
-    to_bool_expr(!check_mode),
+    make_boolean_expr(check_mode),
+    make_boolean_expr(!check_mode),
     false_exprt(),
     false_exprt(),
     true_exprt(),
@@ -387,8 +379,8 @@ void dfcc_wrapper_programt::encode_ensures_write_set()
     from_integer(0, size_type()),
     false_exprt(),
     false_exprt(),
-    to_bool_expr(!check_mode),
-    to_bool_expr(check_mode),
+    make_boolean_expr(!check_mode),
+    make_boolean_expr(check_mode),
     true_exprt(),
     true_exprt(),
     wrapper_sl);