|
13 | 13 | #include "invariant.h"
|
14 | 14 | #include "std_types.h"
|
15 | 15 | #include "validate.h"
|
16 |
| -#include "validate_code.h" |
17 | 16 |
|
18 | 17 | /// Data structure for representing an arbitrary statement in a program. Every
|
19 | 18 | /// specific type of statement (e.g. block of statements, assignment,
|
@@ -73,51 +72,6 @@ class codet : public exprt
|
73 | 72 | codet &last_statement();
|
74 | 73 | const codet &last_statement() const;
|
75 | 74 |
|
76 |
| - /// Check that the code statement is well-formed (shallow checks only, i.e., |
77 |
| - /// enclosed statements, subexpressions, etc. are not checked) |
78 |
| - /// |
79 |
| - /// Subclasses may override this function to provide specific well-formedness |
80 |
| - /// checks for the corresponding types. |
81 |
| - /// |
82 |
| - /// The validation mode indicates whether well-formedness check failures are |
83 |
| - /// reported via DATA_INVARIANT violations or exceptions. |
84 |
| - static void check(const codet &, const validation_modet) |
85 |
| - { |
86 |
| - } |
87 |
| - |
88 |
| - /// Check that the code statement is well-formed, assuming that all its |
89 |
| - /// enclosed statements, subexpressions, etc. have all ready been checked for |
90 |
| - /// well-formedness. |
91 |
| - /// |
92 |
| - /// Subclasses may override this function to provide specific well-formedness |
93 |
| - /// checks for the corresponding types. |
94 |
| - /// |
95 |
| - /// The validation mode indicates whether well-formedness check failures are |
96 |
| - /// reported via DATA_INVARIANT violations or exceptions. |
97 |
| - static void validate( |
98 |
| - const codet &code, |
99 |
| - const namespacet &, |
100 |
| - const validation_modet vm = validation_modet::INVARIANT) |
101 |
| - { |
102 |
| - check_code(code, vm); |
103 |
| - } |
104 |
| - |
105 |
| - /// Check that the code statement is well-formed (full check, including checks |
106 |
| - /// of all subexpressions) |
107 |
| - /// |
108 |
| - /// Subclasses may override this function to provide specific well-formedness |
109 |
| - /// checks for the corresponding types. |
110 |
| - /// |
111 |
| - /// The validation mode indicates whether well-formedness check failures are |
112 |
| - /// reported via DATA_INVARIANT violations or exceptions. |
113 |
| - static void validate_full( |
114 |
| - const codet &code, |
115 |
| - const namespacet &, |
116 |
| - const validation_modet vm = validation_modet::INVARIANT) |
117 |
| - { |
118 |
| - check_code(code, vm); |
119 |
| - } |
120 |
| - |
121 | 75 | using exprt::op0;
|
122 | 76 | using exprt::op1;
|
123 | 77 | using exprt::op2;
|
|
0 commit comments