CBMC
does_remove_const.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Analyses
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
10 
11 #ifndef CPROVER_ANALYSES_DOES_REMOVE_CONST_H
12 #define CPROVER_ANALYSES_DOES_REMOVE_CONST_H
13 
14 #include <utility>
15 
16 class goto_programt;
17 class exprt;
18 class source_locationt;
19 class typet;
20 
22 {
23 public:
24  explicit does_remove_constt(const goto_programt &);
25  std::pair<bool, source_locationt> operator()() const;
26 
27 private:
28  bool does_expr_lose_const(const exprt &expr) const;
29 
31  const typet &type_more_const, const typet &type_compare) const;
32 
34  const typet *target_type, const typet *source_type) const;
35 
37 
39 };
40 
41 #endif // CPROVER_ANALYSES_DOES_REMOVE_CONST_H
bool is_type_at_least_as_const_as(const typet &type_more_const, const typet &type_compare) const
A simple check to check the type_more_const is at least as const as type compare.
friend class does_remove_const_testt
bool does_type_preserve_const_correctness(const typet *target_type, const typet *source_type) const
A recursive check that handles when assigning a source value to a target, is the assignment a loss of...
does_remove_constt(const goto_programt &)
A naive analysis to look for casts that remove const-ness from pointers.
std::pair< bool, source_locationt > operator()() const
A naive analysis to look for casts that remove const-ness from pointers.
const goto_programt & goto_program
bool does_expr_lose_const(const exprt &expr) const
Search the expression tree to look for any children that have the same base type, but a less strict c...
Base class for all expressions.
Definition: expr.h:56
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
The type of an expression, extends irept.
Definition: type.h:29