CBMC: /home/runner/work/cbmc/cbmc/src/analyses/does_remove_const.cpp Source File

20 does_remove_constt::does_remove_constt(const goto_programt &goto_program)

21 : goto_program(goto_program)

22{}

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

27{

28 for(const goto_programt::instructiont &instruction :

29 goto_program.instructions)

30 {

31 if(!instruction.is_assign())

32 {

33 continue;

34 }

35

36 const typet &rhs_type = instruction.assign_rhs().type();

37 const typet &lhs_type = instruction.assign_lhs().type();

38

39 // Compare the types recursively for a point where the rhs is more

40 // const that the lhs

41 if(!does_type_preserve_const_correctness(&lhs_type, &rhs_type))

42 {

43 return {true, instruction.source_location()};

44 }

45

46 if(does_expr_lose_const(instruction.assign_rhs()))

47 {

48 return {true, instruction.assign_rhs().find_source_location()};

49 }

50 }

51

52 return {false, source_locationt()};

53}

61 bool does_remove_constt::does_expr_lose_const(const exprt &expr) const

62{

63 const typet &root_type=expr.type();

64

65 // Look in each child that has the same type as the root

66 for(const exprt &op : expr.operands())

67 {

68 const typet &op_type=op.type();

69 if(op_type == root_type)

70 {

71 // Is this child more const-qualified than the root

72 if(!does_type_preserve_const_correctness(&root_type, &op_type))

73 {

74 return true;

75 }

76 }

77

78 // Recursively check the children of this child

79 if(does_expr_lose_const(op))

80 {

81 return true;

82 }

83 }

84 return false;

85}

114 bool does_remove_constt::does_type_preserve_const_correctness(

115 const typet *target_type, const typet *source_type) const

116{

117 while(target_type->id()==ID_pointer)

118 {

119 PRECONDITION(source_type->id() == ID_pointer);

120

121 const auto &target_pointer_type = to_pointer_type(*target_type);

122 const auto &source_pointer_type = to_pointer_type(*source_type);

123

124 bool direct_subtypes_at_least_as_const = is_type_at_least_as_const_as(

125 target_pointer_type.base_type(), source_pointer_type.base_type());

126 // We have a pointer to something, but the thing it is pointing to can't be

127 // modified normally, but can through this pointer

128 if(!direct_subtypes_at_least_as_const)

129 return false;

130 // Check the subtypes if they are pointers

131 target_type = &target_pointer_type.base_type();

132 source_type = &source_pointer_type.base_type();

133 }

134 return true;

135}

158 bool does_remove_constt::is_type_at_least_as_const_as(

159 const typet &type_more_const, const typet &type_compare) const

160{

161 return !type_compare.get_bool(ID_C_constant) ||

162 type_more_const.get_bool(ID_C_constant);

163}

ait

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

Definition ai.h:566

does_remove_constt::is_type_at_least_as_const_as

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.

Definition does_remove_const.cpp:158

does_remove_constt::does_type_preserve_const_correctness

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...

Definition does_remove_const.cpp:114

does_remove_constt::does_remove_constt

does_remove_constt(const goto_programt &)

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

Definition does_remove_const.cpp:20

does_remove_constt::operator()

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

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

Definition does_remove_const.cpp:26

does_remove_constt::goto_program

const goto_programt & goto_program

Definition does_remove_const.h:36

does_remove_constt::does_expr_lose_const

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...

Definition does_remove_const.cpp:61

exprt

Base class for all expressions.

Definition expr.h:57

exprt::type

typet & type()

Return the type of the expression.

Definition expr.h:85

exprt::operands

operandst & operands()

Definition expr.h:95

goto_programt::instructiont

This class represents an instruction in the GOTO intermediate representation.

Definition goto_program.h:180

goto_programt

A generic container class for the GOTO intermediate representation of one function.

Definition goto_program.h:72

irept::id

const irep_idt & id() const

Definition irep.h:388

source_locationt

Definition source_location.h:20

typet

The type of an expression, extends irept.

Definition type.h:29

does_remove_const.h

Analyses.

goto_program.h

Concrete Goto Program.

pointer_expr.h

API to expression classes for Pointers.

to_pointer_type

const pointer_typet & to_pointer_type(const typet &type)

Cast a typet to a pointer_typet.

Definition pointer_expr.h:93

PRECONDITION

#define PRECONDITION(CONDITION)

Definition invariant.h:463