cbmc/expr__initializer_8h_source.html

/*******************************************************************\


Module: Expression Initialization


Author: Daniel Kroening, kroening@kroening.com


\*******************************************************************/


#ifndef CPROVER_UTIL_EXPR_INITIALIZER_H

#define CPROVER_UTIL_EXPR_INITIALIZER_H


#include <optional>


class exprt;

class namespacet;

class source_locationt;

class typet;


std::optional<exprt>

zero_initializer(const typet &, const source_locationt &, const namespacet &);


std::optional<exprt> nondet_initializer(

  const typet &type,

  const source_locationt &source_location,

  const namespacet &ns);


std::optional<exprt> expr_initializer(

  const typet &type,

  const source_locationt &source_location,

  const namespacet &ns,

  const exprt &init_byte_expr);


exprt duplicate_per_byte(

  const exprt &init_byte_expr,

  const typet &output_type,

  const namespacet &ns);


#endif // CPROVER_UTIL_EXPR_INITIALIZER_H

ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562

exprt
Base class for all expressions.
Definition expr.h:56

namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91

source_locationt
Definition source_location.h:20

typet
The type of an expression, extends irept.
Definition type.h:29

typet::source_location
const source_locationt & source_location() const
Definition type.h:72

duplicate_per_byte
exprt duplicate_per_byte(const exprt &init_byte_expr, const typet &output_type, const namespacet &ns)
Builds an expression of the given output type with each of its bytes initialized to the given initial...
Definition expr_initializer.cpp:381

expr_initializer
std::optional< exprt > expr_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, const exprt &init_byte_expr)
Create a value for type type, with all subtype bytes initialized to the given value.
Definition expr_initializer.cpp:340

zero_initializer
std::optional< exprt > zero_initializer(const typet &, const source_locationt &, const namespacet &)
Create the equivalent of zero for type type.
Definition expr_initializer.cpp:308

nondet_initializer
std::optional< exprt > nondet_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create a non-deterministic value for type type, with all subtypes independently expanded as non-deter...
Definition expr_initializer.cpp:324