cprover
string_refinement_util.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: String solver
4 
5  Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
9 #include <algorithm>
10 #include <numeric>
11 #include <functional>
12 #include <iostream>
13 #include <util/arith_tools.h>
14 #include <util/expr_util.h>
15 #include <util/ssa_expr.h>
16 #include <util/std_expr.h>
17 #include <util/expr_iterator.h>
18 #include <util/graph.h>
19 #include <util/magic.h>
20 #include <util/make_unique.h>
21 #include <unordered_set>
22 #include "string_refinement_util.h"
23 
26 static void for_each_atomic_string(
27  const array_string_exprt &e,
28  const std::function<void(const array_string_exprt &)> f);
29 
30 bool is_char_type(const typet &type)
31 {
32  return type.id() == ID_unsignedbv &&
33  to_unsignedbv_type(type).get_width() <=
35 }
36 
37 bool is_char_array_type(const typet &type, const namespacet &ns)
38 {
39  if(type.id() == ID_symbol)
40  return is_char_array_type(ns.follow(type), ns);
41  return type.id() == ID_array && is_char_type(type.subtype());
42 }
43 
44 bool is_char_pointer_type(const typet &type)
45 {
46  return type.id() == ID_pointer && is_char_type(type.subtype());
47 }
48 
49 bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
50 {
51  return has_subtype(type, is_char_pointer_type, ns);
52 }
53 
54 bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
55 {
56  return has_subexpr(
57  expr, [&](const exprt &e) { return is_char_array_type(e.type(), ns); });
58 }
59 
61 {
62  auto ref = std::ref(static_cast<const exprt &>(expr));
63  while(can_cast_expr<with_exprt>(ref.get()))
64  {
65  const auto &with_expr = expr_dynamic_cast<with_exprt>(ref.get());
66  const auto current_index = numeric_cast_v<std::size_t>(with_expr.where());
67  entries[current_index] = with_expr.new_value();
68  ref = with_expr.old();
69  }
70 
71  // This function only handles 'with' and 'array_of' expressions
72  PRECONDITION(ref.get().id() == ID_array_of);
73  default_value = expr_dynamic_cast<array_of_exprt>(ref.get()).what();
74 }
75 
77 {
78  return std::accumulate(
79  entries.begin(),
80  entries.end(),
82  [&](
83  const exprt if_expr,
84  const std::pair<std::size_t, exprt> &entry) { // NOLINT
85  const exprt entry_index = from_integer(entry.first, index.type());
86  const exprt &then_expr = entry.second;
87  CHECK_RETURN(then_expr.type() == if_expr.type());
88  const equal_exprt index_equal(index, entry_index);
89  return if_exprt(index_equal, then_expr, if_expr, if_expr.type());
90  });
91 }
92 
93 exprt sparse_arrayt::at(const std::size_t index) const
94 {
95  const auto it = entries.find(index);
96  return it != entries.end() ? it->second : default_value;
97 }
98 
100 {
101  return std::accumulate(
102  entries.rbegin(),
103  entries.rend(),
105  [&](
106  const exprt if_expr,
107  const std::pair<std::size_t, exprt> &entry) { // NOLINT
108  const exprt entry_index = from_integer(entry.first, index.type());
109  const exprt &then_expr = entry.second;
110  CHECK_RETURN(then_expr.type() == if_expr.type());
111  const binary_relation_exprt index_small_eq(index, ID_le, entry_index);
112  return if_exprt(index_small_eq, then_expr, if_expr, if_expr.type());
113  });
114 }
115 
117  const array_exprt &expr,
118  const exprt &extra_value)
119  : sparse_arrayt(extra_value)
120 {
121  const auto &operands = expr.operands();
122  exprt last_added = extra_value;
123  for(std::size_t i = 0; i < operands.size(); ++i)
124  {
125  const std::size_t index = operands.size() - 1 - i;
126  if(operands[index].id() != ID_unknown && operands[index] != last_added)
127  {
128  entries[index] = operands[index];
129  last_added = operands[index];
130  }
131  }
132 }
133 
135  const array_list_exprt &expr,
136  const exprt &extra_value)
137  : interval_sparse_arrayt(extra_value)
138 {
139  PRECONDITION(expr.operands().size() % 2 == 0);
140  for(std::size_t i = 0; i < expr.operands().size(); i += 2)
141  {
142  const auto index = numeric_cast<std::size_t>(expr.operands()[i]);
143  INVARIANT(
144  expr.operands()[i + 1].type() == extra_value.type(),
145  "all values in array should have the same type");
146  if(index.has_value() && expr.operands()[i + 1].id() != ID_unknown)
147  entries[*index] = expr.operands()[i + 1];
148  }
149 }
150 
152 interval_sparse_arrayt::of_expr(const exprt &expr, const exprt &extra_value)
153 {
154  if(const auto &array_expr = expr_try_dynamic_cast<array_exprt>(expr))
155  return interval_sparse_arrayt(*array_expr, extra_value);
156  if(const auto &with_expr = expr_try_dynamic_cast<with_exprt>(expr))
157  return interval_sparse_arrayt(*with_expr);
158  if(const auto &array_list = expr_try_dynamic_cast<array_list_exprt>(expr))
159  return interval_sparse_arrayt(*array_list, extra_value);
160  return {};
161 }
162 
163 exprt interval_sparse_arrayt::at(const std::size_t index) const
164 {
165  // First element at or after index
166  const auto it = entries.lower_bound(index);
167  return it != entries.end() ? it->second : default_value;
168 }
169 
171  std::size_t size,
172  const typet &index_type) const
173 {
174  const array_typet array_type(
176  array_exprt array(array_type);
177  array.operands().reserve(size);
178 
179  auto it = entries.begin();
180  for(; it != entries.end() && it->first < size; ++it)
181  array.operands().resize(it->first + 1, it->second);
182 
183  array.operands().resize(
184  size, it == entries.end() ? default_value : it->second);
185  return array;
186 }
187 
188 void equation_symbol_mappingt::add(const std::size_t i, const exprt &expr)
189 {
190  equations_containing[expr].push_back(i);
191  strings_in_equation[i].push_back(expr);
192 }
193 
194 std::vector<exprt>
196 {
197  return strings_in_equation[i];
198 }
199 
200 std::vector<std::size_t>
202 {
203  return equations_containing[expr];
204 }
205 
208 static std::unique_ptr<string_builtin_functiont> to_string_builtin_function(
209  const function_application_exprt &fun_app,
210  const exprt &return_code,
211  array_poolt &array_pool)
212 {
213  const auto name = expr_checked_cast<symbol_exprt>(fun_app.function());
214  const irep_idt &id = is_ssa_expr(name) ? to_ssa_expr(name).get_object_name()
215  : name.get_identifier();
216 
217  if(id == ID_cprover_string_insert_func)
218  return util_make_unique<string_insertion_builtin_functiont>(
219  return_code, fun_app.arguments(), array_pool);
220 
221  if(id == ID_cprover_string_concat_func)
222  return util_make_unique<string_concatenation_builtin_functiont>(
223  return_code, fun_app.arguments(), array_pool);
224 
225  if(id == ID_cprover_string_concat_char_func)
226  return util_make_unique<string_concat_char_builtin_functiont>(
227  return_code, fun_app.arguments(), array_pool);
228 
229  return util_make_unique<string_builtin_function_with_no_evalt>(
230  return_code, fun_app, array_pool);
231 }
232 
235 {
236  auto entry_inserted = node_index_pool.emplace(e, string_nodes.size());
237  if(!entry_inserted.second)
238  return string_nodes[entry_inserted.first->second];
239 
240  string_nodes.emplace_back(e, entry_inserted.first->second);
241  return string_nodes.back();
242 }
243 
244 std::unique_ptr<const string_dependenciest::string_nodet>
246 {
247  const auto &it = node_index_pool.find(e);
248  if(it != node_index_pool.end())
249  return util_make_unique<const string_nodet>(string_nodes.at(it->second));
250  return {};
251 }
252 
254  std::unique_ptr<string_builtin_functiont> &builtin_function)
255 {
256  builtin_function_nodes.emplace_back(
257  std::move(builtin_function), builtin_function_nodes.size());
258  return builtin_function_nodes.back();
259 }
260 
262  const builtin_function_nodet &node) const
263 {
264  return *node.data;
265 }
266 
268  const array_string_exprt &e,
269  const std::function<void(const array_string_exprt &)> f)
270 {
271  if(e.id() != ID_if)
272  return f(e);
273 
274  const auto if_expr = to_if_expr(e);
275  for_each_atomic_string(to_array_string_expr(if_expr.true_case()), f);
276  for_each_atomic_string(to_array_string_expr(if_expr.false_case()), f);
277 }
278 
280  const array_string_exprt &e,
281  const builtin_function_nodet &builtin_function_node)
282 {
283  for_each_atomic_string(e, [&](const array_string_exprt &s) { //NOLINT
284  string_nodet &string_node = get_node(s);
285  string_node.dependencies.push_back(builtin_function_node.index);
286  });
287 }
288 
290 {
291  builtin_function_nodes.clear();
292  string_nodes.clear();
293  node_index_pool.clear();
294  clean_cache();
295 }
296 
298  string_dependenciest &dependencies,
299  const function_application_exprt &fun_app,
300  const string_dependenciest::builtin_function_nodet &builtin_function_node,
301  array_poolt &array_pool)
302 {
303  PRECONDITION(fun_app.arguments()[0].type().id() != ID_pointer);
304  if(
305  fun_app.arguments().size() > 1 &&
306  fun_app.arguments()[1].type().id() == ID_pointer)
307  {
308  // Case where the result is given as a pointer argument
309  const array_string_exprt string =
310  array_pool.find(fun_app.arguments()[1], fun_app.arguments()[0]);
311  dependencies.add_dependency(string, builtin_function_node);
312  }
313 
314  for(const auto &expr : fun_app.arguments())
315  {
316  std::for_each(
317  expr.depth_begin(),
318  expr.depth_end(),
319  [&](const exprt &e) { // NOLINT
321  {
322  const auto string_struct = expr_checked_cast<struct_exprt>(e);
323  const auto string = array_pool.of_argument(string_struct);
324  dependencies.add_dependency(string, builtin_function_node);
325  }
326  });
327  }
328 }
329 
331  const array_string_exprt &s,
332  const std::function<exprt(const exprt &)> &get_value) const
333 {
334  const auto &it = node_index_pool.find(s);
335  if(it == node_index_pool.end())
336  return {};
337 
338  if(eval_string_cache[it->second])
339  return eval_string_cache[it->second];
340 
341  const auto node = string_nodes[it->second];
342  const auto &f = node.result_from;
343  if(f && node.dependencies.size() == 1)
344  {
345  const auto value_opt = builtin_function_nodes[*f].data->eval(get_value);
346  eval_string_cache[it->second] = value_opt;
347  return value_opt;
348  }
349  return {};
350 }
351 
353 {
354  eval_string_cache.resize(string_nodes.size());
355  for(auto &e : eval_string_cache)
356  e.reset();
357 }
358 
359 bool add_node(
360  string_dependenciest &dependencies,
361  const equal_exprt &equation,
362  array_poolt &array_pool)
363 {
364  const auto fun_app =
366  if(!fun_app)
367  return false;
368 
369  auto builtin_function =
370  to_string_builtin_function(*fun_app, equation.lhs(), array_pool);
371 
372  CHECK_RETURN(builtin_function != nullptr);
373  const auto &builtin_function_node = dependencies.make_node(builtin_function);
374  // Warning: `builtin_function` has been emptied and should not be used anymore
375 
376  if(
377  const auto &string_result =
378  dependencies.get_builtin_function(builtin_function_node).string_result())
379  {
380  dependencies.add_dependency(*string_result, builtin_function_node);
381  auto &node = dependencies.get_node(*string_result);
382  node.result_from = builtin_function_node.index;
383 
384  // Ensure all atomic strings in the argument have an associated node
385  for(const auto arg : builtin_function_node.data->string_arguments())
386  {
388  arg, [&](const array_string_exprt &atomic) { // NOLINT
389  (void)dependencies.get_node(atomic);
390  });
391  }
392  }
393  else
395  dependencies, *fun_app, builtin_function_node, array_pool);
396 
397  return true;
398 }
399 
401  const builtin_function_nodet &node,
402  const std::function<void(const string_nodet &)> &f) const
403 {
404  for(const auto &s : node.data->string_arguments())
405  {
406  std::vector<std::reference_wrapper<const exprt>> stack({s});
407  while(!stack.empty())
408  {
409  const auto current = stack.back();
410  stack.pop_back();
411  if(const auto if_expr = expr_try_dynamic_cast<if_exprt>(current.get()))
412  {
413  stack.emplace_back(if_expr->true_case());
414  stack.emplace_back(if_expr->false_case());
415  }
416  else
417  {
418  const auto string_node = node_at(to_array_string_expr(current));
419  INVARIANT(
420  string_node,
421  "dependencies of the node should have been added to the graph at node creation "
422  + current.get().pretty());
423  f(*string_node);
424  }
425  }
426  }
427 }
428 
430  const string_nodet &node,
431  const std::function<void(const builtin_function_nodet &)> &f) const
432 {
433  for(const std::size_t &index : node.dependencies)
434  f(builtin_function_nodes[index]);
435 }
436 
438  const nodet &node,
439  const std::function<void(const nodet &)> &f) const
440 {
441  switch(node.kind)
442  {
443  case nodet::BUILTIN:
446  [&](const string_nodet &n) { return f(nodet(n)); });
447  break;
448 
449  case nodet::STRING:
451  string_nodes[node.index],
452  [&](const builtin_function_nodet &n) { return f(nodet(n)); });
453  break;
454  }
455 }
456 
458  const std::function<void(const nodet &)> &f) const
459 {
460  for(const auto string_node : string_nodes)
461  f(nodet(string_node));
462  for(std::size_t i = 0; i < builtin_function_nodes.size(); ++i)
464 }
465 
466 void string_dependenciest::output_dot(std::ostream &stream) const
467 {
468  const auto for_each =
469  [&](const std::function<void(const nodet &)> &f) { // NOLINT
470  for_each_node(f);
471  };
472  const auto for_each_succ =
473  [&](const nodet &n, const std::function<void(const nodet &)> &f) { // NOLINT
474  for_each_successor(n, f);
475  };
476  const auto node_to_string = [&](const nodet &n) { // NOLINT
477  std::stringstream ostream;
478  if(n.kind == nodet::BUILTIN)
479  ostream << '"' << builtin_function_nodes[n.index].data->name() << '_'
480  << n.index << '"';
481  else
482  ostream << '"' << format(string_nodes[n.index].expr) << '"';
483  return ostream.str();
484  };
485  stream << "digraph dependencies {\n";
486  output_dot_generic<nodet>(stream, for_each, for_each_succ, node_to_string);
487  stream << '}' << std::endl;
488 }
489 
491  string_constraint_generatort &generator)
492 {
493  std::unordered_set<nodet, node_hash> test_dependencies;
494  for(const auto &builtin : builtin_function_nodes)
495  {
496  if(builtin.data->maybe_testing_function())
497  test_dependencies.insert(nodet(builtin));
498  }
499 
501  test_dependencies,
502  [&](
503  const nodet &n,
504  const std::function<void(const nodet &)> &f) { // NOLINT
505  for_each_successor(n, f);
506  });
507 
508  for(const auto &node : builtin_function_nodes)
509  {
510  if(test_dependencies.count(nodet(node)))
511  {
512  const auto &builtin = builtin_function_nodes[node.index];
513  const exprt return_value = builtin.data->add_constraints(generator);
514  generator.add_lemma(equal_exprt(return_value, builtin.data->return_code));
515  }
516  else
517  generator.add_lemma(node.data->length_constraint());
518  }
519 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3426
The type of an expression.
Definition: type.h:22
array_exprt concretize(std::size_t size, const typet &index_type) const
Convert to an array representation, ignores elements at index >= size.
const string_builtin_functiont & get_builtin_function(const builtin_function_nodet &node) const
void add_constraints(string_constraint_generatort &generatort)
For all builtin call on which a test (or an unsupported buitin) result depends, add the corresponding...
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
virtual exprt to_if_expression(const exprt &index) const
Creates an if_expr corresponding to the result of accessing the array at the given index...
application of (mathematical) function
Definition: std_expr.h:4531
builtin_function_nodet & make_node(std::unique_ptr< string_builtin_functiont > &builtin_function)
builtin_function is reset to an empty pointer after the node is created
void clean_cache()
Clean the cache used by eval
bool has_subtype(const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns)
returns true if any of the contained types satisfies pred
Definition: expr_util.cpp:139
Deprecated expression utility functions.
bool can_cast_expr< with_exprt >(const exprt &base)
Definition: std_expr.h:3540
bool add_node(string_dependenciest &dependencies, const equal_exprt &equation, array_poolt &array_pool)
When right hand side of equation is a builtin_function add a "string_builtin_function" node to the gr...
std::unique_ptr< string_builtin_functiont > data
string_nodet & get_node(const array_string_exprt &e)
enum string_dependenciest::nodet::@4 kind
virtual optionalt< array_string_exprt > string_result() const
argumentst & arguments()
Definition: std_expr.h:4564
bool is_char_pointer_type(const typet &type)
For now, any unsigned bitvector type is considered a character.
interval_sparse_arrayt(const with_exprt &expr)
An expression of the form array_of(x) with {i:=a} with {j:=b} is converted to an array arr where for ...
The trinary if-then-else operator.
Definition: std_expr.h:3361
std::unique_ptr< const string_nodet > node_at(const array_string_exprt &e) const
typet & type()
Definition: expr.h:56
exprt to_if_expression(const exprt &index) const override
Creates an if_expr corresponding to the result of accessing the array at the given index...
Magic numbers used throughout the codebase.
auto expr_dynamic_cast(TExpr &base) -> typename detail::expr_dynamic_cast_return_typet< T, TExpr >::type
Cast a reference to a generic exprt to a specific derived class.
Definition: expr_cast.h:165
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
std::vector< builtin_function_nodet > builtin_function_nodes
Set of nodes representing builtin_functions.
Correspondance between arrays and pointers string representations.
Base class for string functions that are built in the solver.
static void for_each_atomic_string(const array_string_exprt &e, const std::function< void(const array_string_exprt &)> f)
Applies f on all strings contained in e that are not if-expressions.
std::unordered_map< array_string_exprt, std::size_t, irep_hash > node_index_pool
Nodes describing dependencies of a string: values of the map correspond to indexes in the vector stri...
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
equality
Definition: std_expr.h:1354
void for_each_successor(const nodet &i, const std::function< void(const nodet &)> &f) const
Applies f on all successors of the node n.
const std::size_t STRING_REFINEMENT_MAX_CHAR_WIDTH
Definition: magic.h:12
const irep_idt & id() const
Definition: irep.h:189
dt * data
Definition: irep.h:326
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:154
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
static void add_dependency_to_string_subexprs(string_dependenciest &dependencies, const function_application_exprt &fun_app, const string_dependenciest::builtin_function_nodet &builtin_function_node, array_poolt &array_pool)
optionalt< exprt > eval(const array_string_exprt &s, const std::function< exprt(const exprt &)> &get_value) const
Attempt to evaluate the given string from the dependencies and valuation of strings on which it depen...
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:125
std::map< exprt, std::vector< std::size_t > > equations_containing
Record index of the equations that contain a given expression.
Represents arrays by the indexes up to which the value remains the same.
nonstd::optional< T > optionalt
Definition: optional.h:35
std::vector< string_nodet > string_nodes
Set of nodes representing strings.
void clear()
Clear the content of the dependency graph.
void add(const std::size_t i, const exprt &expr)
Record the fact that equation i contains expression expr
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
Definition: arith_tools.h:122
API to expression classes.
Represents arrays of the form array_of(x) with {i:=a} with {j:=b} ... by a default value x and a list...
TO_BE_DOCUMENTED.
Definition: namespace.h:74
std::map< std::size_t, exprt > entries
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
array constructor from single element
Definition: std_expr.h:1550
const typet & follow(const typet &) const
Definition: namespace.cpp:55
bitvector_typet index_type()
Definition: c_types.cpp:16
auto expr_checked_cast(TExpr &base) -> typename detail::expr_dynamic_cast_return_typet< T, TExpr >::type
Cast a reference to a generic exprt to a specific derived class.
Definition: expr_cast.h:184
array_string_exprt of_argument(const exprt &arg)
Converts a struct containing a length and pointer to an array.
exprt at(std::size_t index) const override
Get the value at the specified index.
std::vector< optionalt< exprt > > eval_string_cache
std::unordered_map< std::size_t, std::vector< exprt > > strings_in_equation
Record expressions that are contained in the equation with the given index.
Keep track of dependencies between strings.
std::size_t get_width() const
Definition: std_types.h:1129
A builtin function node contains a builtin function call.
symbol_exprt & function()
Definition: std_expr.h:4552
A string node points to builtin_function on which it depends.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1245
bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
A Template Class for Graphs.
static std::unique_ptr< string_builtin_functiont > to_string_builtin_function(const function_application_exprt &fun_app, const exprt &return_code, array_poolt &array_pool)
Construct a string_builtin_functiont object from a function application.
std::vector< exprt > find_expressions(const std::size_t i)
Base class for all expressions.
Definition: expr.h:42
bool is_refined_string_type(const typet &type)
Operator to update elements in structs and arrays.
Definition: std_expr.h:3461
irep_idt get_object_name() const
Definition: ssa_expr.h:46
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:173
std::vector< std::size_t > dependencies
sparse_arrayt(const with_exprt &expr)
Initialize a sparse array from an expression of the form array_of(x) with {i:=a} with {j:=b} ...
arrays with given size
Definition: std_types.h:1004
void add_dependency(const array_string_exprt &e, const builtin_function_nodet &builtin_function)
Add edge from node for e to node for builtin_function if e is a simple array expression.
static optionalt< interval_sparse_arrayt > of_expr(const exprt &expr, const exprt &extra_value)
If the expression is an array_exprt or a with_exprt uses the appropriate constructor, otherwise returns empty optional.
Expression to hold a symbol (variable)
Definition: std_expr.h:90
virtual exprt at(std::size_t index) const
Get the value at the specified index.
const typet & subtype() const
Definition: type.h:33
bool is_char_type(const typet &type)
For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character...
bool is_char_array_type(const typet &type, const namespacet &ns)
Distinguish char array from other types.
operandst & operands()
Definition: expr.h:66
std::vector< std::size_t > find_equations(const exprt &expr)
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
#define stack(x)
Definition: parser.h:144
struct constructor from list of elements
Definition: std_expr.h:1815
void for_each_node(const std::function< void(const nodet &)> &f) const
Applies f on all nodes.
array constructor from list of elements
Definition: std_expr.h:1617
void get_reachable(Container &set, const std::function< void(const typename Container::value_type &, const std::function< void(const typename Container::value_type &)> &)> &for_each_successor)
Add to set, nodes that are reachable from set.
Definition: graph.h:474
void for_each_dependency(const string_nodet &node, const std::function< void(const builtin_function_nodet &)> &f) const
Applies f to each node on which node depends.
array_string_exprt & to_array_string_expr(exprt &expr)
Definition: string_expr.h:162
Array constructor from a list of index-element pairs Operands are index/value pairs, alternating.
Definition: std_expr.h:1662
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition: expr_cast.h:91
void output_dot(std::ostream &stream) const
static format_containert< T > format(const T &o)
Definition: format.h:35