CBMC
havoc_utils.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Utilities for building havoc code for expressions.
4 
5 Author: Saswat Padhi, saspadhi@amazon.com
6 
7 Date: July 2021
8 
9 \*******************************************************************/
10 
13 
14 #include "havoc_utils.h"
15 
16 #include <util/pointer_expr.h>
17 #include <util/std_code.h>
18 
20 
22  const source_locationt location,
23  goto_programt &dest)
24 {
25  for(const auto &expr : assigns)
26  append_havoc_code_for_expr(location, expr, dest);
27 }
28 
30  const source_locationt location,
31  const exprt &expr,
32  goto_programt &dest)
33 {
34  if(expr.id() == ID_index || expr.id() == ID_dereference)
35  {
36  address_of_exprt address_of_expr(expr);
37  if(!is_constant(address_of_expr))
38  {
39  append_object_havoc_code_for_expr(location, address_of_expr, dest);
40  return;
41  }
42  }
43  append_scalar_havoc_code_for_expr(location, expr, dest);
44 }
45 
47  const source_locationt location,
48  const exprt &expr,
49  goto_programt &dest) const
50 {
51  codet havoc(ID_havoc_object);
52  havoc.add_source_location() = location;
53  havoc.add_to_operands(expr);
54  dest.add(goto_programt::make_other(havoc, location));
55 }
56 
58  const source_locationt location,
59  const exprt &expr,
60  goto_programt &dest) const
61 {
62  side_effect_expr_nondett rhs(expr.type(), location);
64  code_assignt{expr, std::move(rhs), location}, location));
65 }
Operator to return the address of an object.
Definition: pointer_expr.h:540
A goto_instruction_codet representing an assignment in the program.
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
Base class for all expressions.
Definition: expr.h:56
source_locationt & add_source_location()
Definition: expr.h:236
typet & type()
Return the type of the expression.
Definition: expr.h:84
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:170
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_other(const goto_instruction_codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:957
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:739
virtual void append_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest)
Append goto instructions to havoc a single expression expr
Definition: havoc_utils.cpp:29
const havoc_utils_can_forward_propagatet is_constant
Definition: havoc_utils.h:108
virtual void append_object_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const
Append goto instructions to havoc the underlying object of expr
Definition: havoc_utils.cpp:46
const assignst & assigns
Definition: havoc_utils.h:107
void append_full_havoc_code(const source_locationt location, goto_programt &dest)
Append goto instructions to havoc the full assigns set.
Definition: havoc_utils.cpp:21
virtual void append_scalar_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const
Append goto instructions to havoc the value of expr
Definition: havoc_utils.cpp:57
const irep_idt & id() const
Definition: irep.h:388
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
Concrete Goto Program.
Utilities for building havoc code for expressions.
API to expression classes for Pointers.