CBMC
does_remove_constt Class Reference

#include <does_remove_const.h>

+ Collaboration diagram for does_remove_constt:

Public Member Functions

 does_remove_constt (const goto_programt &)
 A naive analysis to look for casts that remove const-ness from pointers. More...
 
std::pair< bool, source_locationtoperator() () const
 A naive analysis to look for casts that remove const-ness from pointers. More...
 

Private Member Functions

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 const qualification. More...
 
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. More...
 
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 const-correctness. More...
 

Private Attributes

const goto_programtgoto_program
 

Friends

class does_remove_const_testt
 

Detailed Description

Definition at line 21 of file does_remove_const.h.

Constructor & Destructor Documentation

◆ does_remove_constt()

does_remove_constt::does_remove_constt ( const goto_programt goto_program)
explicit

A naive analysis to look for casts that remove const-ness from pointers.

Parameters
goto_programthe goto program to check

Definition at line 20 of file does_remove_const.cpp.

Member Function Documentation

◆ does_expr_lose_const()

bool does_remove_constt::does_expr_lose_const ( const exprt expr) const
private

Search the expression tree to look for any children that have the same base type, but a less strict const qualification.

If one is found, we return true.

Parameters
exprThe expression to check
Returns
Returns true if somewhere in the passed expression tree the const- ness is lost.

Definition at line 61 of file does_remove_const.cpp.

◆ does_type_preserve_const_correctness()

bool does_remove_constt::does_type_preserve_const_correctness ( const typet target_type,
const typet source_type 
) const
private

A recursive check that handles when assigning a source value to a target, is the assignment a loss of const-correctness.

For primitive types, it always returns true since these are copied

For pointers we requires that if in the source it's value couldn't be modified, then it still can't be modified in the target

target_type | source_type || result

const int | int -> true int | const int -> true const int | const int -> true int | int -> true

int * | int * const -> true int * | const int * -> false const int * | int * -> true const int * | const int * -> true int * const | int * -> true

See unit/analyses/does_type_preserve_const_correcness for comprehensive list

Parameters
target_typethe resulting type
source_typethe starting type
Returns
Returns true if a value of type source_type could be assigned into a a value of target_type without losing const-correctness

Definition at line 114 of file does_remove_const.cpp.

◆ is_type_at_least_as_const_as()

bool does_remove_constt::is_type_at_least_as_const_as ( const typet type_more_const,
const typet type_compare 
) const
private

A simple check to check the type_more_const is at least as const as type compare.

This only checks the exact type, use is_pointer_at_least_as_constant_as for dealing with nested types

type_more_const | type_compare || result

const int | int -> true int | const int -> false const int | const int -> true int | int -> true int * | int * const -> false int * | const int * -> true const int * | int * -> true int * const | int * -> true

See unit/analyses/is_type_as_least_as_const_as for comprehensive list

Parameters
type_more_constthe type we are expecting to be at least as const qualified
type_comparethe type we are comparing against which may be less const qualified
Returns
Returns true if type_more_const is at least as const as type_compare

Definition at line 158 of file does_remove_const.cpp.

◆ operator()()

std::pair< bool, source_locationt > does_remove_constt::operator() ( ) const

A naive analysis to look for casts that remove const-ness from pointers.

Returns
Returns true if the program contains a const-removing cast

Definition at line 26 of file does_remove_const.cpp.

Friends And Related Function Documentation

◆ does_remove_const_testt

friend class does_remove_const_testt
friend

Definition at line 38 of file does_remove_const.h.

Member Data Documentation

◆ goto_program

const goto_programt& does_remove_constt::goto_program
private

Definition at line 36 of file does_remove_const.h.


The documentation for this class was generated from the following files: