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

17 jsont ai_domain_baset::output_json(const ai_baset &ai, const namespacet &ns)

18 const

19{

20 std::ostringstream out;

21 output(out, ai, ns);

22 json_stringt json(out.str());

23 return std::move(json);

24}

26 xmlt ai_domain_baset::output_xml(const ai_baset &ai, const namespacet &ns) const

27{

28 std::ostringstream out;

29 output(out, ai, ns);

30 xmlt xml("abstract_state");

31 xml.data = out.str();

32 return xml;

33}

43 bool ai_domain_baset::ai_simplify_lhs(exprt &condition, const namespacet &ns)

44 const

45{

46 // Care must be taken here to give something that is still writable

47 if(condition.id() == ID_index)

48 {

49 index_exprt ie = to_index_expr(condition);

50 bool no_simplification = ai_simplify(ie.index(), ns);

51 if(!no_simplification)

52 condition = simplify_expr(std::move(ie), ns);

53

54 return no_simplification;

55 }

56 else if(condition.id() == ID_dereference)

57 {

58 dereference_exprt de = to_dereference_expr(condition);

59 bool no_simplification = ai_simplify(de.pointer(), ns);

60 if(!no_simplification)

61 condition = simplify_expr(std::move(de), ns); // So *(&x) -> x

62

63 return no_simplification;

64 }

65 else if(condition.id() == ID_member)

66 {

67 member_exprt me = to_member_expr(condition);

68 // Since simplify_ai_lhs is required to return an addressable object

69 // (so remains a valid left hand side), to simplify

70 // `(something_simplifiable).b` we require that `something_simplifiable`

71 // must also be addressable

72 bool no_simplification = ai_simplify_lhs(me.compound(), ns);

73 if(!no_simplification)

74 condition = simplify_expr(std::move(me), ns);

75

76 return no_simplification;

77 }

78 else

79 return true;

80}

ai_domain.h

Abstract Interpretation Domain.

ai_baset

This is the basic interface of the abstract interpreter with default implementations of the core func...

Definition ai.h:117

ai_domain_baset::output_xml

virtual xmlt output_xml(const ai_baset &ai, const namespacet &ns) const

Definition ai_domain.cpp:26

ai_domain_baset::output_json

virtual jsont output_json(const ai_baset &ai, const namespacet &ns) const

Definition ai_domain.cpp:17

ai_domain_baset::ai_simplify_lhs

virtual bool ai_simplify_lhs(exprt &condition, const namespacet &ns) const

Simplifies the expression but keeps it as an l-value.

Definition ai_domain.cpp:43

ai_domain_baset::output

virtual void output(std::ostream &, const ai_baset &, const namespacet &) const

Definition ai_domain.h:104

ai_domain_baset::ai_simplify

virtual bool ai_simplify(exprt &condition, const namespacet &) const

also add

Definition ai_domain.h:149

ait

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

Definition ai.h:566

dereference_exprt

Operator to dereference a pointer.

Definition pointer_expr.h:834

exprt

Base class for all expressions.

Definition expr.h:57

index_exprt

Array index operator.

Definition std_expr.h:1431

irept::id

const irep_idt & id() const

Definition irep.h:388

json_stringt

Definition json.h:270

jsont

Definition json.h:27

member_exprt

Extract member of struct or union.

Definition std_expr.h:2866

namespacet

A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...

Definition namespace.h:91

xmlt

Definition xml.h:21

xmlt::data

std::string data

Definition xml.h:39

pointer_expr.h

API to expression classes for Pointers.

to_dereference_expr

const dereference_exprt & to_dereference_expr(const exprt &expr)

Cast an exprt to a dereference_exprt.

Definition pointer_expr.h:890

json

static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)

Definition properties.cpp:120

xml

xmlt xml(const irep_idt &property_id, const property_infot &property_info)

Definition properties.cpp:110

simplify_expr

exprt simplify_expr(exprt src, const namespacet &ns)

Definition simplify_expr.cpp:3412

simplify_expr.h

to_index_expr

const index_exprt & to_index_expr(const exprt &expr)

Cast an exprt to an index_exprt.

Definition std_expr.h:1494

to_member_expr

const member_exprt & to_member_expr(const exprt &expr)

Cast an exprt to a member_exprt.

Definition std_expr.h:2953