Loading...

Searching...

No Matches

cpp_template_parameter.h

Go to the documentation of this file.

1/*******************************************************************\

2

3Module:

4

5Author: Daniel Kroening, kroening@cs.cmu.edu

6

7\*******************************************************************/

8

9

10#ifndef CPROVER_CPP_CPP_TEMPLATE_PARAMETER_H

11#define CPROVER_CPP_CPP_TEMPLATE_PARAMETER_H

12

13#include <util/expr.h>

14

15// A data structure for expressions of the form

16// <typename T, int x, ...>

17// Not to be confused with template arguments!

18

19 struct template_parametert:public exprt

20{

21public:

22 template_parametert():exprt(ID_template_parameter)

23 {

24 }

25

26 #if 0

27 bool get_is_type() const

28{

29 return get_bool(ID_is_type);

30 }

31

32 void set_is_type(bool value)

33 {

34 set(ID_is_type, value);

35 }

36

37 irep_idt get_identifier() const

38{

39 return get(ID_identifier);

40 }

41

42 void set_identifier(const irep_idt &identifier)

43 {

44 return set(ID_identifier, identifier);

45 }

46 #endif

47

48 exprt &default_argument()

49 {

50 return static_cast<exprt &>(add(ID_C_default_value));

51 }

52

53 const exprt &default_argument() const

54{

55 return static_cast<const exprt &>(find(ID_C_default_value));

56 }

57

58 bool has_default_argument() const

59{

60 return find(ID_C_default_value).is_not_nil();

61 }

62};

63

65 struct template_parameter_symbol_typet : public typet

66{

67public:

68 explicit template_parameter_symbol_typet(const irep_idt &identifier)

69 : typet(ID_template_parameter_symbol_type)

70 {

71 set_identifier(identifier);

72 }

73

74 void set_identifier(const irep_idt &identifier)

75 {

76 set(ID_identifier, identifier);

77 }

78

79 const irep_idt &get_identifier() const

80{

81 return get(ID_identifier);

82 }

83};

84

93inline const template_parameter_symbol_typet &

94 to_template_parameter_symbol_type(const typet &type)

95{

96 PRECONDITION(type.id() == ID_template_parameter_symbol_type);

97 return static_cast<const template_parameter_symbol_typet &>(type);

98}

99

101inline template_parameter_symbol_typet &

102 to_template_parameter_symbol_type(typet &type)

103{

104 PRECONDITION(type.id() == ID_template_parameter_symbol_type);

105 return static_cast<template_parameter_symbol_typet &>(type);

106}

107

108#endif // CPROVER_CPP_CPP_TEMPLATE_PARAMETER_H

ait

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

Definition ai.h:566

dstringt

dstringt has one field, an unsigned integer no which is an index into a static table of strings.

Definition dstring.h:38

exprt

Base class for all expressions.

Definition expr.h:57

irept::get_bool

bool get_bool(const irep_idt &name) const

Definition irep.cpp:57

irept::find

const irept & find(const irep_idt &name) const

Definition irep.cpp:93

irept::get

const irep_idt & get(const irep_idt &name) const

Definition irep.cpp:44

irept::set

void set(const irep_idt &name, const irep_idt &value)

Definition irep.h:412

irept::id

const irep_idt & id() const

Definition irep.h:388

irept::add

irept & add(const irep_idt &name)

Definition irep.cpp:103

typet

The type of an expression, extends irept.

Definition type.h:29

to_template_parameter_symbol_type

const template_parameter_symbol_typet & to_template_parameter_symbol_type(const typet &type)

Cast a typet to a template_parameter_symbol_typet.

Definition cpp_template_parameter.h:94

expr.h

PRECONDITION

#define PRECONDITION(CONDITION)

Definition invariant.h:463

template_parameter_symbol_typet

a template parameter symbol that is a type

Definition cpp_template_parameter.h:66

template_parameter_symbol_typet::template_parameter_symbol_typet

template_parameter_symbol_typet(const irep_idt &identifier)

Definition cpp_template_parameter.h:68

template_parameter_symbol_typet::get_identifier

const irep_idt & get_identifier() const

Definition cpp_template_parameter.h:79

template_parameter_symbol_typet::set_identifier

void set_identifier(const irep_idt &identifier)

Definition cpp_template_parameter.h:74

template_parametert

Definition cpp_template_parameter.h:20

template_parametert::default_argument

exprt & default_argument()

Definition cpp_template_parameter.h:48

template_parametert::default_argument

const exprt & default_argument() const

Definition cpp_template_parameter.h:53

template_parametert::template_parametert

template_parametert()

Definition cpp_template_parameter.h:22

template_parametert::has_default_argument

bool has_default_argument() const

Definition cpp_template_parameter.h:58

CBMC: /home/runner/work/cbmc/cbmc/src/cpp/cpp_template_parameter.h Source File