string_format_builtin_function.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Built-in function for String.format
 
Author: Romain Brenguier, Joel Allred
 
\*******************************************************************/
 
 
#ifndef CPROVER_SOLVERS_STRINGS_STRING_FORMAT_BUILTIN_FUNCTION_H
#define CPROVER_SOLVERS_STRINGS_STRING_FORMAT_BUILTIN_FUNCTION_H
 
#include "string_builtin_function.h"
 
class format_specifiert;
 
class string_format_builtin_functiont final : public string_builtin_functiont
{
public:
  array_string_exprt result;
  optionalt<std::string> format_string;
  std::vector<array_string_exprt> inputs;
 
  string_format_builtin_functiont(
    const exprt &return_code,
    const std::vector<exprt> &fun_args,
    array_poolt &array_pool);
 
  optionalt<array_string_exprt> string_result() const override
  {
    return result;
  }
 
  std::vector<array_string_exprt> string_arguments() const override
  {
    return inputs;
  }
 
  optionalt<exprt>
  eval(const std::function<exprt(const exprt &)> &get_value) const override;
 
  std::string name() const override
  {
    return "format";
  }
 
  string_constraintst constraints(
    string_constraint_generatort &generator,
    message_handlert &message_handler) const override;
 
  exprt length_constraint() const override;
 
  bool maybe_testing_function() const override
  {
    return false;
  }
};
 
exprt length_of_decimal_int(
  const exprt &integer,
  const typet &length_type,
  const unsigned long base);
 
exprt length_for_format_specifier(
  const format_specifiert &fs,
  const array_string_exprt &arg,
  const typet &index_type,
  array_poolt &array_pool);
 
#endif // CPROVER_SOLVERS_STRINGS_STRING_FORMAT_BUILTIN_FUNCTION_H