CBMC
ssa_expr.cpp File Reference
#include "ssa_expr.h"
#include <sstream>
#include "pointer_expr.h"
+ Include dependency graph for ssa_expr.cpp:

Go to the source code of this file.

Functions

static std::ostream & initialize_ssa_identifier (std::ostream &os, const exprt &expr)
 If expr is: More...
 

Function Documentation

◆ initialize_ssa_identifier()

static std::ostream& initialize_ssa_identifier ( std::ostream &  os,
const exprt expr 
)
static

If expr is:

  • a symbol_exprt "s" add "s" to the stream os
    • a member_exprt, apply recursively and add "..component_name"
    • an index_exprt where the index is a constant, apply recursively on the array and add "[[index]]"
      Returns
      the stream os

Definition at line 22 of file ssa_expr.cpp.