CBMC
nondet_bool.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Nondeterministic boolean helper
4 
5 Author: Chris Smowton, chris@smowton.net
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_UTIL_NONDET_BOOL_H
13 #define CPROVER_UTIL_NONDET_BOOL_H
14 
15 #include "std_expr.h"
16 
20 inline exprt
21 get_nondet_bool(const typet &type, const source_locationt &source_location)
22 {
23  // We force this to 0 and 1 and won't consider
24  // other values.
25  return typecast_exprt(
26  side_effect_expr_nondett(bool_typet(), source_location), type);
27 }
28 
29 #endif // CPROVER_UTIL_NONDET_BOOL_H
typet
The type of an expression, extends irept.
Definition: type.h:28
exprt
Base class for all expressions.
Definition: expr.h:55
bool_typet
The Boolean type.
Definition: std_types.h:35
source_locationt
Definition: source_location.h:18
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1519
get_nondet_bool
exprt get_nondet_bool(const typet &type, const source_locationt &source_location)
Definition: nondet_bool.h:21
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2016
std_expr.h