CBMC
Loading...
Searching...
No Matches
irep_ids.def
Go to the documentation of this file.
1
4
5IREP_ID_TWO(empty_string, )
6IREP_ID_ONE(let)
7IREP_ID_ONE(let_binding)
8IREP_ID_ONE(nil)
9IREP_ID_ONE(type)
10IREP_ID_ONE(bool)
11IREP_ID_ONE(c_bitint)
12IREP_ID_ONE(c_bool)
13IREP_ID_ONE(c_signed_bitint)
14IREP_ID_ONE(c_typeof_unqual)
15IREP_ID_ONE(c_unsigned_bitint)
16IREP_ID_ONE(proper_bool)
17IREP_ID_ONE(signedbv)
18IREP_ID_ONE(unsignedbv)
19IREP_ID_ONE(verilog_signedbv)
20IREP_ID_ONE(verilog_unsignedbv)
21IREP_ID_ONE(floatbv)
22IREP_ID_ONE(fixedbv)
23IREP_ID_ONE(x86_extended)
24IREP_ID_TWO(C_source_location, #source_location)
25IREP_ID_TWO(C_end_location, #end_location)
26IREP_ID_TWO(C_is_padding, #is_padding)
27IREP_ID_ONE(C_do_not_dump)
28IREP_ID_ONE(file)
29IREP_ID_ONE(line)
30IREP_ID_ONE(column)
31IREP_ID_ONE(comment)
32IREP_ID_ONE(property_class)
33IREP_ID_ONE(property_fatal)
34IREP_ID_ONE(property_id)
35IREP_ID_ONE(function)
36IREP_ID_ONE(mathematical_function)
37IREP_ID_ONE(code)
38IREP_ID_ONE(typecast)
39IREP_ID_ONE(static_cast)
40IREP_ID_ONE(dynamic_cast)
41IREP_ID_ONE(const_cast)
42IREP_ID_ONE(reinterpret_cast)
43IREP_ID_ONE(index)
44IREP_ID_ONE(ptrmember)
45IREP_ID_ONE(member)
46IREP_ID_ONE(member_name)
47IREP_ID_TWO(C_member_name, #member_name)
48IREP_ID_TWO(equal, =)
49IREP_ID_TWO(implies, =>)
50IREP_ID_ONE(and)
51IREP_ID_ONE(nand)
52IREP_ID_ONE(or)
53IREP_ID_ONE(nor)
54IREP_ID_ONE(xor)
55IREP_ID_ONE(xnor)
56IREP_ID_ONE(not)
57IREP_ID_ONE(bitand)
58IREP_ID_ONE(bitor)
59IREP_ID_ONE(bitnot)
60IREP_ID_ONE(bitxor)
61IREP_ID_ONE(bitnand)
62IREP_ID_ONE(bitnor)
63IREP_ID_ONE(bitxnor)
64IREP_ID_ONE(notequal)
65IREP_ID_ONE(if)
66IREP_ID_ONE(symbol)
67IREP_ID_ONE(nondet_symbol)
68IREP_ID_ONE(predicate_symbol)
69IREP_ID_ONE(predicate_next_symbol)
70IREP_ID_ONE(nondet_bool)
71IREP_ID_ONE(empty)
72IREP_ID_ONE(side_effect)
73IREP_ID_ONE(statement)
74IREP_ID_ONE(statement_expression)
75IREP_ID_ONE(value)
76IREP_ID_ONE(constant)
77IREP_ID_ONE(block)
78IREP_ID_ONE(decl)
79IREP_ID_ONE(dead)
80IREP_ID_ONE(assign)
81IREP_ID_ONE(assign_div)
82IREP_ID_TWO(assign_mult, assign*)
83IREP_ID_TWO(assign_plus, assign+)
84IREP_ID_TWO(assign_minus, assign-)
85IREP_ID_ONE(assign_mod)
86IREP_ID_ONE(assign_shl)
87IREP_ID_ONE(assign_shr)
88IREP_ID_ONE(assign_ashr)
89IREP_ID_ONE(assign_lshr)
90IREP_ID_ONE(assign_bitand)
91IREP_ID_ONE(assign_bitxor)
92IREP_ID_ONE(assign_bitor)
93IREP_ID_ONE(assume)
94IREP_ID_ONE(assert)
95IREP_ID_ONE(assertion)
96IREP_ID_ONE(precondition)
97IREP_ID_ONE(postcondition)
98IREP_ID_ONE(precondition_instance)
99IREP_ID_ONE(goto)
100IREP_ID_ONE(gcc_computed_goto)
101IREP_ID_ONE(ifthenelse)
102IREP_ID_ONE(label)
103IREP_ID_ONE(break)
104IREP_ID_ONE(continue)
105IREP_ID_ONE(function_call)
106IREP_ID_ONE(return)
107IREP_ID_ONE(skip)
108IREP_ID_ONE(arguments)
109IREP_ID_ONE(array)
110IREP_ID_TWO(C_index_type, #index_type)
111IREP_ID_ONE(size)
112IREP_ID_ONE(frontend_pointer)
113IREP_ID_ONE(pointer)
114IREP_ID_ONE(block_pointer)
115IREP_ID_ONE(switch)
116IREP_ID_ONE(switch_case)
117IREP_ID_ONE(gcc_switch_case_range)
118IREP_ID_ONE(for)
119IREP_ID_ONE(while)
120IREP_ID_ONE(dowhile)
121IREP_ID_ONE(int)
122IREP_ID_ONE(integer)
123IREP_ID_ONE(natural)
124IREP_ID_ONE(real)
125IREP_ID_ONE(rational)
126IREP_ID_ONE(complex)
127IREP_ID_ONE(signed)
128IREP_ID_ONE(unsigned)
129IREP_ID_ONE(asm)
130IREP_ID_ONE(gcc_asm_input)
131IREP_ID_ONE(gcc_asm_output)
132IREP_ID_ONE(gcc_asm_clobbered_register)
133IREP_ID_ONE(incomplete)
134IREP_ID_ONE(incomplete_class)
135IREP_ID_TWO(C_incomplete, #incomplete)
136IREP_ID_ONE(identifier)
137IREP_ID_ONE(name)
138IREP_ID_ONE(inner_name)
139IREP_ID_ONE(cpp_name)
140IREP_ID_ONE(component_cpp_name)
141IREP_ID_TWO(C_id_class, #id_class)
142IREP_ID_ONE(declaration)
143IREP_ID_ONE(declaration_list)
144IREP_ID_ONE(declarator)
145IREP_ID_ONE(struct)
146IREP_ID_ONE(c_bit_field)
147IREP_ID_ONE(union)
148IREP_ID_ONE(class)
149IREP_ID_ONE(merged_type)
150IREP_ID_ONE(range)
151IREP_ID_ONE(from)
152IREP_ID_ONE(to)
153IREP_ID_ONE(module)
154IREP_ID_ONE(parameter)
155IREP_ID_ONE(component_name)
156IREP_ID_ONE(component_number)
157IREP_ID_ONE(tag)
158IREP_ID_ONE(default)
159IREP_ID_TWO(C_default_value, #default_value)
160IREP_ID_ONE(base_name)
161IREP_ID_TWO(C_base_name, #base_name)
162IREP_ID_ONE(string)
163IREP_ID_ONE(regex)
164IREP_ID_ONE(is_cstring)
165IREP_ID_TWO(C_string_constant, #string_constant)
166IREP_ID_ONE(string_constant)
167IREP_ID_ONE(cstrlen)
168IREP_ID_ONE(is_sentinel_dll)
169IREP_ID_ONE(width)
170IREP_ID_ONE(components)
171IREP_ID_ONE(bv)
172IREP_ID_ONE(f)
173IREP_ID_ONE(with)
174IREP_ID_ONE(trans)
175IREP_ID_ONE(throw)
176IREP_ID_ONE(try_catch)
177IREP_ID_ONE(noexcept)
178IREP_ID_ONE(CPROVER_throw)
179IREP_ID_ONE(CPROVER_try_catch)
180IREP_ID_ONE(CPROVER_try_finally)
181IREP_ID_ONE(protection)
182IREP_ID_ONE(private)
183IREP_ID_ONE(public)
184IREP_ID_ONE(protected)
185IREP_ID_ONE(virtual)
186IREP_ID_ONE(volatile)
187IREP_ID_ONE(const)
188IREP_ID_ONE(constexpr)
189IREP_ID_ONE(inline)
190IREP_ID_ONE(forall)
191IREP_ID_ONE(exists)
192IREP_ID_ONE(repeat)
193IREP_ID_ONE(extractbit)
194IREP_ID_ONE(extractbits)
195IREP_ID_ONE(update_bit)
196IREP_ID_ONE(update_bits)
197IREP_ID_ONE(zero_extend)
198IREP_ID_TWO(C_reference, #reference)
199IREP_ID_TWO(C_rvalue_reference, #rvalue_reference)
200IREP_ID_ONE(true)
201IREP_ID_ONE(false)
202IREP_ID_ONE(address_of)
203IREP_ID_ONE(object_address)
204IREP_ID_ONE(field_address)
205IREP_ID_ONE(element_address)
206IREP_ID_ONE(dereference)
207IREP_ID_TWO(C_lvalue, #lvalue)
208IREP_ID_TWO(C_base, #base)
209IREP_ID_ONE(destination)
210IREP_ID_ONE(main)
211IREP_ID_ONE(expression)
212IREP_ID_ONE(allocate)
213IREP_ID_ONE(reallocate)
214IREP_ID_TWO(C_cxx_alloc_type, #cxx_alloc_type)
215IREP_ID_ONE(cpp_new)
216IREP_ID_ONE(cpp_delete)
217IREP_ID_TWO(cpp_new_array, cpp_new[])
218IREP_ID_TWO(cpp_delete_array, cpp_delete[])
219IREP_ID_ONE(java_new)
220IREP_ID_ONE(java_new_array)
221IREP_ID_ONE(java_new_array_data)
222IREP_ID_ONE(java_string_literal)
223IREP_ID_ONE(printf)
224IREP_ID_ONE(input)
225IREP_ID_ONE(output)
226IREP_ID_ONE(nondet)
227IREP_ID_ONE(NULL)
228IREP_ID_ONE(nullptr)
229IREP_ID_ONE(c_enum)
230IREP_ID_ONE(enum_underlying_type)
231IREP_ID_ONE(enumeration)
232IREP_ID_ONE(elements)
233IREP_ID_ONE(unknown)
234IREP_ID_ONE(uninitialized)
235IREP_ID_ONE(invalid)
236IREP_ID_TWO(C_invalid_object, #invalid_object)
237IREP_ID_ONE(pointer_offset)
238IREP_ID_ONE(pointer_object)
239IREP_ID_ONE(is_invalid_pointer)
240IREP_ID_ONE(ieee_float_equal)
241IREP_ID_ONE(ieee_float_notequal)
242IREP_ID_ONE(isnan)
243IREP_ID_ONE(lambda)
244IREP_ID_ONE(named_term)
245IREP_ID_ONE(array_comprehension)
246IREP_ID_ONE(array_of)
247IREP_ID_ONE(array_equal)
248IREP_ID_ONE(array_set)
249IREP_ID_ONE(array_copy)
250IREP_ID_ONE(array_list)
251IREP_ID_ONE(euclidean_mod)
252IREP_ID_ONE(mod)
253IREP_ID_ONE(shr)
254IREP_ID_ONE(ashr)
255IREP_ID_ONE(lshr)
256IREP_ID_ONE(shl)
257IREP_ID_ONE(rol)
258IREP_ID_ONE(ror)
259IREP_ID_ONE(comma)
260IREP_ID_ONE(concatenation)
261IREP_ID_ONE(infinity)
262IREP_ID_ONE(return_type)
263IREP_ID_ONE(typedef)
264IREP_ID_ONE(typedef_type)
265IREP_ID_TWO(C_typedef, #typedef)
266IREP_ID_ONE(extern)
267IREP_ID_ONE(static)
268IREP_ID_ONE(auto)
269IREP_ID_ONE(register)
270IREP_ID_ONE(thread_local)
271IREP_ID_ONE(thread)
272IREP_ID_TWO(C_thread_local, #thread_local)
273IREP_ID_TWO(C_static_lifetime, #static_lifetime)
274IREP_ID_ONE(mutable)
275IREP_ID_ONE(void)
276IREP_ID_ONE(int8)
277IREP_ID_ONE(int16)
278IREP_ID_ONE(int32)
279IREP_ID_ONE(int64)
280IREP_ID_ONE(ptr32)
281IREP_ID_ONE(ptr64)
282IREP_ID_ONE(char)
283IREP_ID_ONE(short)
284IREP_ID_ONE(long)
285IREP_ID_ONE(float)
286IREP_ID_ONE(double)
287IREP_ID_ONE(byte)
288IREP_ID_ONE(boolean)
289IREP_ID_ONE(long_double)
290IREP_ID_ONE(signed_char)
291IREP_ID_ONE(unsigned_char)
292IREP_ID_ONE(signed_int)
293IREP_ID_ONE(unsigned_int)
294IREP_ID_ONE(signed_long_int)
295IREP_ID_ONE(unsigned_long_int)
296IREP_ID_ONE(signed_short_int)
297IREP_ID_ONE(unsigned_short_int)
298IREP_ID_ONE(signed_long_long_int)
299IREP_ID_ONE(unsigned_long_long_int)
300IREP_ID_ONE(signed_int128)
301IREP_ID_ONE(unsigned_int128)
302IREP_ID_TWO(C_inlined, #inlined)
303IREP_ID_ONE(hide)
304IREP_ID_ONE(abs)
305IREP_ID_ONE(sign)
306IREP_ID_ONE(access)
307IREP_ID_TWO(C_access, #access)
308IREP_ID_ONE(postincrement)
309IREP_ID_ONE(postdecrement)
310IREP_ID_ONE(preincrement)
311IREP_ID_ONE(predecrement)
312IREP_ID_ONE(integer_bits)
313IREP_ID_ONE(KnR)
314IREP_ID_TWO(C_KnR, #KnR)
315IREP_ID_ONE(constraint_select_one)
316IREP_ID_ONE(cond)
317IREP_ID_ONE(isfinite)
318IREP_ID_ONE(isinf)
319IREP_ID_ONE(isnormal)
320IREP_ID_ONE(alignof)
321IREP_ID_ONE(clang_builtin_convertvector)
322IREP_ID_ONE(gcc_builtin_va_arg)
323IREP_ID_ONE(gcc_builtin_types_compatible_p)
324IREP_ID_ONE(gcc_builtin_has_attribute)
325IREP_ID_ONE(va_start)
326IREP_ID_ONE(gcc_float16)
327IREP_ID_ONE(gcc_float32)
328IREP_ID_ONE(gcc_float32x)
329IREP_ID_ONE(gcc_float64)
330IREP_ID_ONE(gcc_float64x)
331IREP_ID_ONE(gcc_float80)
332IREP_ID_ONE(gcc_float128)
333IREP_ID_ONE(gcc_float128x)
334IREP_ID_ONE(gcc_int128)
335IREP_ID_ONE(gcc_decimal32)
336IREP_ID_ONE(gcc_decimal64)
337IREP_ID_ONE(gcc_decimal128)
338IREP_ID_ONE(builtin_offsetof)
339IREP_ID_ONE(0)
340IREP_ID_ONE(1)
341IREP_ID_ONE(sizeof)
342IREP_ID_ONE(type_arg)
343IREP_ID_ONE(expr_arg)
344IREP_ID_ONE(expression_list)
345IREP_ID_ONE(initializer_list)
346IREP_ID_ONE(gcc_conditional_expression)
347IREP_ID_ONE(gcc_local_label)
348IREP_ID_ONE(gcc)
349IREP_ID_ONE(msc)
350IREP_ID_ONE(typeof)
351IREP_ID_ONE(ellipsis)
352IREP_ID_ONE(flavor)
353IREP_ID_TWO(ge, >=)
354IREP_ID_TWO(le, <=)
355IREP_ID_TWO(gt, >)
356IREP_ID_TWO(lt, <)
357IREP_ID_TWO(plus, +)
358IREP_ID_TWO(minus, -)
359IREP_ID_TWO(unary_minus, unary-)
360IREP_ID_TWO(unary_plus, unary+)
361IREP_ID_TWO(mult, *)
362IREP_ID_TWO(div, /)
363IREP_ID_TWO(power, **)
364IREP_ID_ONE(factorial_power)
365IREP_ID_TWO(C_pretty_name, #pretty_name)
366IREP_ID_TWO(C_class, #class)
367IREP_ID_TWO(C_field, #field)
368IREP_ID_TWO(C_interface, #interface)
369IREP_ID_ONE(designated_initializer)
370IREP_ID_ONE(designator)
371IREP_ID_ONE(member_designator)
372IREP_ID_ONE(index_designator)
373IREP_ID_TWO(C_constant, #constant)
374IREP_ID_TWO(C_volatile, #volatile)
375IREP_ID_TWO(C_restricted, #restricted)
376IREP_ID_TWO(C_identifier, #identifier)
377IREP_ID_TWO(C_implicit, #implicit)
378IREP_ID_TWO(C_ptr32, #ptr32)
379IREP_ID_TWO(C_ptr64, #ptr64)
380IREP_ID_TWO(C_atomic, #atomic)
381IREP_ID_ONE(restrict)
382IREP_ID_ONE(byte_extract_big_endian)
383IREP_ID_ONE(byte_extract_little_endian)
384IREP_ID_ONE(byte_update_big_endian)
385IREP_ID_ONE(byte_update_little_endian)
386IREP_ID_ONE(replication)
387IREP_ID_ONE(cprover_atomic)
388IREP_ID_ONE(atomic)
389IREP_ID_ONE(atomic_type_specifier)
390IREP_ID_ONE(atomic_begin)
391IREP_ID_ONE(atomic_end)
392IREP_ID_ONE(start_thread)
393IREP_ID_ONE(end_thread)
394IREP_ID_ONE(coverage_criterion)
395IREP_ID_ONE(initializer)
396IREP_ID_ONE(anonymous)
397IREP_ID_TWO(C_is_anonymous, #is_anonymous)
398IREP_ID_ONE(is_enum_constant)
399IREP_ID_ONE(is_inline)
400IREP_ID_ONE(is_extern)
401IREP_ID_ONE(is_synchronized)
402IREP_ID_ONE(is_native_method)
403IREP_ID_ONE(is_varargs_method)
404IREP_ID_ONE(is_global)
405IREP_ID_ONE(is_thread_local)
406IREP_ID_ONE(is_parameter)
407IREP_ID_ONE(is_member)
408IREP_ID_ONE(is_type)
409IREP_ID_ONE(is_register)
410IREP_ID_ONE(is_typedef)
411IREP_ID_ONE(is_static)
412IREP_ID_ONE(is_template)
413IREP_ID_ONE(is_static_assert)
414IREP_ID_ONE(is_virtual)
415IREP_ID_TWO(C_is_virtual, #is_virtual)
416IREP_ID_ONE(literal)
417IREP_ID_ONE(literal_vector)
418IREP_ID_ONE(literals)
419IREP_ID_ONE(member_initializers)
420IREP_ID_ONE(member_initializer)
421IREP_ID_ONE(method_qualifier)
422IREP_ID_ONE(methods)
423IREP_ID_ONE(static_members)
424IREP_ID_ONE(constructor)
425IREP_ID_ONE(destructor)
426IREP_ID_ONE(bases)
427IREP_ID_ONE(base)
428IREP_ID_ONE(from_base)
429IREP_ID_ONE(operator)
430IREP_ID_ONE(template)
431IREP_ID_ONE(template_class_instance)
432IREP_ID_ONE(template_function_instance)
433IREP_ID_ONE(template_type)
434IREP_ID_ONE(template_args)
435IREP_ID_ONE(template_parameter)
436IREP_ID_ONE(template_parameter_symbol_type)
437IREP_ID_ONE(template_parameters)
438IREP_ID_TWO(C_template, #template)
439IREP_ID_TWO(C_template_arguments, #template_arguments)
440IREP_ID_TWO(C_template_case, #template_case)
441IREP_ID_ONE(typename)
442IREP_ID_ONE(C)
443IREP_ID_ONE(cpp)
444IREP_ID_ONE(java)
445IREP_ID_ONE(decl_block)
446IREP_ID_ONE(decl_type)
447IREP_ID_ONE(parameters)
448IREP_ID_ONE(wchar_t)
449IREP_ID_ONE(char16_t)
450IREP_ID_ONE(char32_t)
451IREP_ID_ONE(size_t)
452IREP_ID_ONE(ssize_t)
453IREP_ID_ONE(mode)
454IREP_ID_ONE(this)
455IREP_ID_TWO(C_this, #this)
456IREP_ID_ONE(reduction_and)
457IREP_ID_ONE(reduction_or)
458IREP_ID_ONE(reduction_nand)
459IREP_ID_ONE(reduction_nor)
460IREP_ID_ONE(reduction_xor)
461IREP_ID_ONE(reduction_xnor)
462IREP_ID_ONE(body)
463IREP_ID_ONE(temporary_object)
464IREP_ID_TWO(overflow_plus, overflow-+)
465IREP_ID_TWO(overflow_minus, overflow--)
466IREP_ID_TWO(overflow_mult, overflow-*)
467IREP_ID_TWO(overflow_unary_minus, overflow-unary-)
468IREP_ID_ONE(object_descriptor)
469IREP_ID_ONE(is_dynamic_object)
470IREP_ID_ONE(dynamic_object)
471IREP_ID_TWO(C_dynamic, #dynamic)
472IREP_ID_ONE(pointer_in_range)
473IREP_ID_ONE(object_size)
474IREP_ID_ONE(separate)
475IREP_ID_ONE(live_object)
476IREP_ID_ONE(writeable_object)
477IREP_ID_ONE(integer_address)
478IREP_ID_ONE(integer_address_object)
479IREP_ID_TWO(null_object, NULL-object)
480IREP_ID_ONE(static_object)
481IREP_ID_ONE(stack_object)
482IREP_ID_TWO(C_is_failed_symbol, #is_failed_symbol)
483IREP_ID_TWO(C_failed_symbol, #failed_symbol)
484IREP_ID_ONE(friend)
485IREP_ID_TWO(C_friends, #friends)
486IREP_ID_ONE(explicit)
487IREP_ID_ONE(storage_spec)
488IREP_ID_ONE(member_spec)
489IREP_ID_ONE(msc_declspec)
490IREP_ID_ONE(packed)
491IREP_ID_TWO(C_packed, #packed)
492IREP_ID_ONE(transparent_union)
493IREP_ID_TWO(C_transparent_union, #transparent_union)
494IREP_ID_ONE(aligned)
495IREP_ID_TWO(C_alignment, #alignment)
496IREP_ID_ONE(frontend_vector)
497IREP_ID_ONE(vector)
498IREP_ID_ONE(abstract)
499IREP_ID_ONE(function_application)
500IREP_ID_ONE(cpp_declarator)
501IREP_ID_ONE(cpp_linkage_spec)
502IREP_ID_ONE(cpp_namespace_spec)
503IREP_ID_ONE(cpp_storage_spec)
504IREP_ID_ONE(cpp_using)
505IREP_ID_ONE(cpp_declaration)
506IREP_ID_ONE(cpp_static_assert)
507IREP_ID_ONE(cpp_member_spec)
508IREP_ID_TWO(C_c_type, #c_type)
509IREP_ID_TWO(C_c_bitint_width, #c_bitint_width)
510IREP_ID_ONE(namespace)
511IREP_ID_ONE(linkage)
512IREP_ID_ONE(decltype)
513IREP_ID_TWO(C_tag_only_declaration, #tag_only_declaration)
514IREP_ID_ONE(struct_tag)
515IREP_ID_ONE(union_tag)
516IREP_ID_ONE(c_enum_tag)
517IREP_ID_ONE(verilog_case_equality)
518IREP_ID_ONE(verilog_case_inequality)
519IREP_ID_ONE(user_specified_predicate)
520IREP_ID_ONE(user_specified_parameter_predicates)
521IREP_ID_ONE(user_specified_return_predicates)
522IREP_ID_ONE(unassigned)
523IREP_ID_ONE(new_object)
524IREP_ID_ONE(complex_real)
525IREP_ID_ONE(complex_imag)
526IREP_ID_ONE(imag)
527IREP_ID_ONE(msc_try_except)
528IREP_ID_ONE(msc_try_finally)
529IREP_ID_ONE(msc_leave)
530IREP_ID_ONE(msc_uuidof)
531IREP_ID_ONE(msc_if_exists)
532IREP_ID_ONE(msc_if_not_exists)
533IREP_ID_ONE(msc_underlying_type)
534IREP_ID_ONE(msc_based)
535IREP_ID_ONE(alias)
536IREP_ID_ONE(ptr_object)
537IREP_ID_TWO(C_c_sizeof_type, #c_sizeof_type)
538IREP_ID_ONE(array_update)
539IREP_ID_ONE(update)
540IREP_ID_ONE(static_assert)
541IREP_ID_ONE(gcc_attribute_mode)
542IREP_ID_TWO(built_in, <built-in>)
543IREP_ID_ONE(exception_list)
544IREP_ID_ONE(exception_id)
545IREP_ID_ONE(predicate_passive_symbol)
546IREP_ID_ONE(cw_va_arg_typeof)
547IREP_ID_ONE(fence)
548IREP_ID_ONE(sync)
549IREP_ID_ONE(lwsync)
550IREP_ID_ONE(isync)
551IREP_ID_ONE(WRfence)
552IREP_ID_ONE(RRfence)
553IREP_ID_ONE(RWfence)
554IREP_ID_ONE(WWfence)
555IREP_ID_ONE(RRcumul)
556IREP_ID_ONE(RWcumul)
557IREP_ID_ONE(WWcumul)
558IREP_ID_ONE(WRcumul)
559IREP_ID_ONE(generic_selection)
560IREP_ID_ONE(generic_associations)
561IREP_ID_ONE(generic_association)
562IREP_ID_ONE(floatbv_plus)
563IREP_ID_ONE(floatbv_minus)
564IREP_ID_ONE(floatbv_mult)
565IREP_ID_ONE(floatbv_div)
566IREP_ID_ONE(floatbv_mod)
567IREP_ID_ONE(floatbv_rem)
568IREP_ID_ONE(floatbv_fma)
569IREP_ID_ONE(floatbv_typecast)
570IREP_ID_ONE(floatbv_round_to_integral)
571IREP_ID_ONE(compound_literal)
572IREP_ID_ONE(custom_bv)
573IREP_ID_ONE(custom_unsignedbv)
574IREP_ID_ONE(custom_signedbv)
575IREP_ID_ONE(custom_fixedbv)
576IREP_ID_ONE(custom_floatbv)
577IREP_ID_TWO(C_SSA_symbol, #SSA_symbol)
578IREP_ID_ONE(L0)
579IREP_ID_ONE(L1)
580IREP_ID_ONE(L2)
581IREP_ID_ONE(L1_object_identifier)
582IREP_ID_ONE(already_typechecked)
583IREP_ID_TWO(C_va_arg_type, #va_arg_type)
584IREP_ID_ONE(smt2_symbol)
585IREP_ID_ONE(onehot)
586IREP_ID_ONE(onehot0)
587IREP_ID_ONE(popcount)
588IREP_ID_ONE(function_type)
589IREP_ID_ONE(nodiscard)
590IREP_ID_TWO(C_nodiscard, #nodiscard)
591IREP_ID_ONE(noreturn)
592IREP_ID_TWO(C_noreturn, #noreturn)
593IREP_ID_ONE(weak)
594IREP_ID_ONE(is_weak)
595IREP_ID_ONE(used)
596IREP_ID_ONE(is_used)
597IREP_ID_TWO(C_spec_loop_invariant, #spec_loop_invariant)
598IREP_ID_TWO(C_spec_decreases, #spec_decreases)
599IREP_ID_TWO(C_spec_requires, #spec_requires)
600IREP_ID_TWO(C_spec_ensures, #spec_ensures)
601IREP_ID_TWO(C_spec_assigns, #spec_assigns)
602IREP_ID_TWO(C_spec_frees, #spec_frees)
603IREP_ID_ONE(target_list)
604IREP_ID_ONE(conditional_target_group)
605IREP_ID_ONE(virtual_function)
606IREP_ID_TWO(element_type, element_type)
607IREP_ID_ONE(working_directory)
608IREP_ID_ONE(section)
609IREP_ID_ONE(bswap)
610IREP_ID_ONE(java_bytecode_index)
611IREP_ID_ONE(java_instanceof)
612IREP_ID_ONE(java_super_method_call)
613IREP_ID_ONE(java_enum_static_unwind)
614IREP_ID_ONE(push_catch)
615IREP_ID_ONE(pop_catch)
616IREP_ID_ONE(exception_landingpad)
617IREP_ID_ONE(length_upper_bound)
618IREP_ID_ONE(cprover_associate_array_to_pointer_func)
619IREP_ID_ONE(cprover_associate_length_to_array_func)
620IREP_ID_ONE(cprover_char_literal_func)
621IREP_ID_ONE(cprover_string_literal_func)
622IREP_ID_ONE(cprover_string_char_at_func)
623IREP_ID_ONE(cprover_string_char_set_func)
624IREP_ID_ONE(cprover_string_code_point_at_func)
625IREP_ID_ONE(cprover_string_code_point_before_func)
626IREP_ID_ONE(cprover_string_code_point_count_func)
627IREP_ID_ONE(cprover_string_offset_by_code_point_func)
628IREP_ID_ONE(cprover_string_compare_to_func)
629IREP_ID_ONE(cprover_string_concat_func)
630IREP_ID_ONE(cprover_string_concat_char_func)
631IREP_ID_ONE(cprover_string_concat_code_point_func)
632IREP_ID_ONE(cprover_string_constrain_characters_func)
633IREP_ID_ONE(cprover_string_contains_func)
634IREP_ID_ONE(cprover_string_copy_func)
635IREP_ID_ONE(cprover_string_delete_func)
636IREP_ID_ONE(cprover_string_delete_char_at_func)
637IREP_ID_ONE(cprover_string_equal_func)
638IREP_ID_ONE(cprover_string_equals_ignore_case_func)
639IREP_ID_ONE(cprover_string_empty_string_func)
640IREP_ID_ONE(cprover_string_endswith_func)
641IREP_ID_ONE(cprover_string_format_func)
642IREP_ID_ONE(cprover_string_index_of_func)
643IREP_ID_ONE(cprover_string_insert_func)
644IREP_ID_ONE(cprover_string_is_prefix_func)
645IREP_ID_ONE(cprover_string_is_suffix_func)
646IREP_ID_ONE(cprover_string_is_empty_func)
647IREP_ID_ONE(cprover_string_last_index_of_func)
648IREP_ID_ONE(cprover_string_length_func)
649IREP_ID_ONE(cprover_string_of_int_func)
650IREP_ID_ONE(cprover_string_of_int_hex_func)
651IREP_ID_ONE(cprover_string_of_long_func)
652IREP_ID_ONE(cprover_string_of_float_func)
653IREP_ID_ONE(cprover_string_of_float_scientific_notation_func)
654IREP_ID_ONE(cprover_string_of_double_func)
655IREP_ID_ONE(cprover_string_parse_int_func)
656IREP_ID_ONE(cprover_string_is_valid_int_func)
657IREP_ID_ONE(cprover_string_is_valid_long_func)
658IREP_ID_ONE(cprover_string_replace_func)
659IREP_ID_ONE(cprover_string_set_length_func)
660IREP_ID_ONE(cprover_string_startswith_func)
661IREP_ID_ONE(cprover_string_substring_func)
662IREP_ID_ONE(cprover_string_to_lower_case_func)
663IREP_ID_ONE(cprover_string_to_upper_case_func)
664IREP_ID_ONE(cprover_string_trim_func)
665// Regex operators for the SMT-LIB theory-of-strings back-end. A front-end
666// (e.g. Strata) emits these over SMT-LIB-native String/RegLan operands; they
667// lower directly to the SMT-LIB regex operators in smt2_conv. They have no
668// SAT string-solver (src/solvers/strings) implementation and must therefore
669// only be used with the SMT-LIB back-end.
670IREP_ID_ONE(cprover_string_to_regex_func)
671IREP_ID_ONE(cprover_string_in_regex_func)
672IREP_ID_ONE(cprover_regex_range_func)
673IREP_ID_ONE(cprover_regex_concat_func)
674IREP_ID_ONE(cprover_regex_star_func)
675IREP_ID_ONE(cprover_regex_plus_func)
676IREP_ID_ONE(cprover_regex_opt_func)
677IREP_ID_ONE(cprover_regex_loop_func)
678IREP_ID_ONE(cprover_regex_union_func)
679IREP_ID_ONE(cprover_regex_inter_func)
680IREP_ID_ONE(cprover_regex_comp_func)
681IREP_ID_ONE(cprover_regex_diff_func)
682IREP_ID_ONE(cprover_regex_all_func)
683IREP_ID_ONE(cprover_regex_allchar_func)
684IREP_ID_ONE(cprover_regex_none_func)
685IREP_ID_ONE(skip_initialize)
686IREP_ID_ONE(basic_block_source_lines)
687IREP_ID_ONE(is_nondet_nullable)
688IREP_ID_ONE(array_replace)
689IREP_ID_ONE(switch_case_number)
690IREP_ID_ONE(java_array_access)
691IREP_ID_ONE(java_member_access)
692IREP_ID_TWO(C_java_generic_parameter, #java_generic_parameter)
693IREP_ID_TWO(C_java_generics_class_type, #java_generics_class_type)
694IREP_ID_TWO(C_java_implicitly_generic_class_type, #java_implicitly_generic_class_type)
695IREP_ID_TWO(C_java_generic_symbol, #java_generic_symbol)
696IREP_ID_ONE(generic_types)
697IREP_ID_TWO(implicit_generic_types, #implicit_generic_types)
698IREP_ID_ONE(type_variables)
699IREP_ID_ONE(handle_type)
700IREP_ID_ONE(java_lambda_method_handle)
701IREP_ID_TWO(java_lambda_method_handle_index, lambda_method_handle_index)
702IREP_ID_TWO(java_lambda_method_handles, lambda_method_handles)
703IREP_ID_ONE(havoc_object)
704IREP_ID_TWO(overflow_shl, overflow-shl)
705IREP_ID_TWO(C_no_initialization_required, #no_initialization_required)
706IREP_ID_TWO(C_no_nondet_initialization, #no_nondet_initialization)
707IREP_ID_TWO(overlay_class, java::org.cprover.OverlayClassImplementation)
708IREP_ID_TWO(overlay_method, java::org.cprover.OverlayMethodImplementation)
709IREP_ID_TWO(ignored_method, java::org.cprover.IgnoredMethodImplementation)
710IREP_ID_ONE(is_annotation)
711IREP_ID_TWO(C_annotations, #annotations)
712IREP_ID_ONE(final)
713IREP_ID_ONE(bits_per_byte)
714IREP_ID_TWO(C_abstract, #abstract)
715IREP_ID_ONE(synthetic)
716IREP_ID_ONE(interface)
717IREP_ID_TWO(C_must_not_throw, #must_not_throw)
718IREP_ID_ONE(is_inner_class)
719IREP_ID_ONE(is_anonymous)
720IREP_ID_ONE(outer_class)
721IREP_ID_ONE(is_bridge_method)
722IREP_ID_TWO(C_is_operator, #is_operator)
723IREP_ID_TWO(C_not_accessible, #not_accessible)
724IREP_ID_TWO(C_override_constantness, #override_constantness)
725IREP_ID_TWO(C_bound, #bound)
726IREP_ID_TWO(C_is_static, #is_static)
727IREP_ID_TWO(C_call_by_value, #call_by_value)
728IREP_ID_TWO(C_virtual_name, #virtual_name)
729IREP_ID_TWO(C_unnamed_object, #unnamed_object)
730IREP_ID_TWO(C_temporary_avoided, #temporary_avoided)
731IREP_ID_TWO(C_qualifier, #qualifier)
732IREP_ID_TWO(C_array_ini, #array_ini)
733IREP_ID_ONE(r_ok)
734IREP_ID_ONE(w_ok)
735IREP_ID_ONE(rw_ok)
736IREP_ID_ONE(old)
737IREP_ID_ONE(loop_entry)
738IREP_ID_ONE(super_class)
739IREP_ID_ONE(exceptions_thrown_list)
740IREP_ID_TWO(C_java_method_type, #java_method_type)
741IREP_ID_ONE(compiled)
742IREP_ID_ONE(partial_specialization_args)
743IREP_ID_ONE(specialization_of)
744IREP_ID_ONE(init_args)
745IREP_ID_ONE(ambiguous)
746IREP_ID_ONE(specialization_template_args)
747IREP_ID_ONE(full_template_args)
748IREP_ID_ONE(instantiated_with)
749IREP_ID_ONE(template_methods)
750IREP_ID_ONE(cpp_not_typechecked)
751IREP_ID_ONE(noaccess)
752IREP_ID_ONE(is_operator)
753IREP_ID_ONE(is_cast_operator)
754IREP_ID_ONE(is_explicit)
755IREP_ID_ONE(is_mutable)
756IREP_ID_ONE(virtual_name)
757IREP_ID_ONE(is_pure_virtual)
758IREP_ID_ONE(is_vtptr)
759IREP_ID_ONE(prefix)
760IREP_ID_ONE(cv)
761IREP_ID_ONE(cpp_dummy_destructor)
762IREP_ID_ONE(cast_expression)
763IREP_ID_ONE(pod_constructor)
764IREP_ID_ONE(template_decls)
765IREP_ID_ONE(throw_decl)
766IREP_ID_ONE(typeid)
767IREP_ID_TWO(C_quoted, #quoted)
768IREP_ID_ONE(to_member)
769IREP_ID_ONE(pointer_to_member)
770IREP_ID_ONE(tuple)
771IREP_ID_ONE(function_body)
772IREP_ID_ONE(get_may)
773IREP_ID_ONE(set_may)
774IREP_ID_ONE(clear_may)
775IREP_ID_ONE(get_must)
776IREP_ID_ONE(set_must)
777IREP_ID_ONE(clear_must)
778IREP_ID_ONE(pragma)
779IREP_ID_ONE(__atomic_add_fetch)
780IREP_ID_ONE(__atomic_and_fetch)
781IREP_ID_ONE(__atomic_compare_exchange)
782IREP_ID_ONE(__atomic_compare_exchange_n)
783IREP_ID_ONE(__atomic_exchange)
784IREP_ID_ONE(__atomic_exchange_n)
785IREP_ID_ONE(__atomic_fetch_add)
786IREP_ID_ONE(__atomic_fetch_and)
787IREP_ID_ONE(__atomic_fetch_nand)
788IREP_ID_ONE(__atomic_fetch_or)
789IREP_ID_ONE(__atomic_fetch_sub)
790IREP_ID_ONE(__atomic_fetch_xor)
791IREP_ID_ONE(__atomic_load)
792IREP_ID_ONE(__atomic_load_n)
793IREP_ID_ONE(__atomic_nand_fetch)
794IREP_ID_ONE(__atomic_or_fetch)
795IREP_ID_ONE(__atomic_store)
796IREP_ID_ONE(__atomic_store_n)
797IREP_ID_ONE(__atomic_sub_fetch)
798IREP_ID_ONE(__atomic_xor_fetch)
799IREP_ID_ONE(__sync_add_and_fetch)
800IREP_ID_ONE(__sync_and_and_fetch)
801IREP_ID_ONE(__sync_bool_compare_and_swap)
802IREP_ID_ONE(__sync_fetch_and_add)
803IREP_ID_ONE(__sync_fetch_and_and)
804IREP_ID_ONE(__sync_fetch_and_nand)
805IREP_ID_ONE(__sync_fetch_and_or)
806IREP_ID_ONE(__sync_fetch_and_sub)
807IREP_ID_ONE(__sync_fetch_and_xor)
808IREP_ID_ONE(__sync_lock_release)
809IREP_ID_ONE(__sync_lock_test_and_set)
810IREP_ID_ONE(__sync_nand_and_fetch)
811IREP_ID_ONE(__sync_or_and_fetch)
812IREP_ID_ONE(__sync_sub_and_fetch)
813IREP_ID_ONE(__sync_val_compare_and_swap)
814IREP_ID_ONE(__sync_xor_and_fetch)
815IREP_ID_TWO(statement_list, Statement List)
816IREP_ID_ONE(statement_list_type)
817IREP_ID_ONE(statement_list_function)
818IREP_ID_ONE(statement_list_function_block)
819IREP_ID_TWO(statement_list_main_function, Main)
820IREP_ID_ONE(statement_list_data_block)
821IREP_ID_ONE(statement_list_version)
822IREP_ID_ONE(statement_list_var_input)
823IREP_ID_ONE(statement_list_var_inout)
824IREP_ID_ONE(statement_list_var_output)
825IREP_ID_ONE(statement_list_var_constant)
826IREP_ID_ONE(statement_list_var_temp)
827IREP_ID_ONE(statement_list_var_static)
828IREP_ID_ONE(statement_list_return)
829IREP_ID_TWO(statement_list_return_value_id, Ret_Val)
830IREP_ID_ONE(statement_list_var_entry)
831IREP_ID_ONE(statement_list_var_decls)
832IREP_ID_ONE(statement_list_network)
833IREP_ID_ONE(statement_list_networks)
834IREP_ID_ONE(statement_list_title)
835IREP_ID_ONE(statement_list_identifier)
836IREP_ID_ONE(statement_list_load)
837IREP_ID_ONE(statement_list_transfer)
838IREP_ID_ONE(statement_list_call)
839IREP_ID_ONE(statement_list_nop)
840IREP_ID_ONE(statement_list_const_add)
841IREP_ID_ONE(statement_list_accu_int_add)
842IREP_ID_ONE(statement_list_accu_int_sub)
843IREP_ID_ONE(statement_list_accu_int_mul)
844IREP_ID_ONE(statement_list_accu_int_div)
845IREP_ID_ONE(statement_list_accu_int_eq)
846IREP_ID_ONE(statement_list_accu_int_neq)
847IREP_ID_ONE(statement_list_accu_int_gt)
848IREP_ID_ONE(statement_list_accu_int_lt)
849IREP_ID_ONE(statement_list_accu_int_gte)
850IREP_ID_ONE(statement_list_accu_int_lte)
851IREP_ID_ONE(statement_list_accu_real_add)
852IREP_ID_ONE(statement_list_accu_real_sub)
853IREP_ID_ONE(statement_list_accu_real_mul)
854IREP_ID_ONE(statement_list_accu_real_div)
855IREP_ID_ONE(statement_list_accu_real_eq)
856IREP_ID_ONE(statement_list_accu_real_neq)
857IREP_ID_ONE(statement_list_accu_real_gt)
858IREP_ID_ONE(statement_list_accu_real_lt)
859IREP_ID_ONE(statement_list_accu_real_gte)
860IREP_ID_ONE(statement_list_accu_real_lte)
861IREP_ID_ONE(statement_list_accu_dint_add)
862IREP_ID_ONE(statement_list_accu_dint_sub)
863IREP_ID_ONE(statement_list_accu_dint_mul)
864IREP_ID_ONE(statement_list_accu_dint_div)
865IREP_ID_ONE(statement_list_accu_dint_eq)
866IREP_ID_ONE(statement_list_accu_dint_neq)
867IREP_ID_ONE(statement_list_accu_dint_gt)
868IREP_ID_ONE(statement_list_accu_dint_lt)
869IREP_ID_ONE(statement_list_accu_dint_gte)
870IREP_ID_ONE(statement_list_accu_dint_lte)
871IREP_ID_ONE(statement_list_and)
872IREP_ID_ONE(statement_list_and_not)
873IREP_ID_ONE(statement_list_or)
874IREP_ID_ONE(statement_list_or_not)
875IREP_ID_ONE(statement_list_xor)
876IREP_ID_ONE(statement_list_xor_not)
877IREP_ID_ONE(statement_list_and_nested)
878IREP_ID_ONE(statement_list_and_not_nested)
879IREP_ID_ONE(statement_list_or_nested)
880IREP_ID_ONE(statement_list_or_not_nested)
881IREP_ID_ONE(statement_list_xor_nested)
882IREP_ID_ONE(statement_list_xor_not_nested)
883IREP_ID_ONE(statement_list_nesting_closed)
884IREP_ID_ONE(statement_list_assign)
885IREP_ID_ONE(statement_list_set_rlo)
886IREP_ID_ONE(statement_list_clr_rlo)
887IREP_ID_ONE(statement_list_set)
888IREP_ID_ONE(statement_list_reset)
889IREP_ID_ONE(statement_list_not)
890IREP_ID_ONE(statement_list_jump_unconditional)
891IREP_ID_ONE(statement_list_jump_conditional)
892IREP_ID_ONE(statement_list_jump_conditional_not)
893IREP_ID_ONE(statement_list_instruction)
894IREP_ID_ONE(statement_list_instructions)
895IREP_ID_ONE(max_value)
896IREP_ID_ONE(min_value)
897IREP_ID_ONE(constant_interval)
898IREP_ID_TWO(C_bounds_check, #bounds_check)
899IREP_ID_ONE(count_leading_zeros)
900IREP_ID_TWO(vector_equal, vector-=)
901IREP_ID_TWO(vector_notequal, vector-!=)
902IREP_ID_TWO(vector_ge, vector->=)
903IREP_ID_TWO(vector_le, vector-<=)
904IREP_ID_TWO(vector_gt, vector->)
905IREP_ID_TWO(vector_lt, vector-<)
906IREP_ID_ONE(shuffle_vector)
907IREP_ID_ONE(count_trailing_zeros)
908IREP_ID_ONE(find_first_set)
909IREP_ID_ONE(empty_union)
910IREP_ID_ONE(bitreverse)
911IREP_ID_ONE(saturating_minus)
912IREP_ID_ONE(saturating_plus)
913IREP_ID_ONE(annotated_pointer_constant)
914IREP_ID_TWO(C_flexible_array_member, #flexible_array_member)
915IREP_ID_ONE(state)
916IREP_ID_ONE(initial_state)
917IREP_ID_ONE(evaluate)
918IREP_ID_ONE(allocate_state)
919IREP_ID_ONE(reallocate_state)
920IREP_ID_ONE(deallocate_state)
921IREP_ID_ONE(update_state)
922IREP_ID_ONE(enter_scope_state)
923IREP_ID_ONE(exit_scope_state)
924IREP_ID_ONE(state_r_ok)
925IREP_ID_ONE(state_w_ok)
926IREP_ID_ONE(state_rw_ok)
927IREP_ID_ONE(state_type_compatible)
928IREP_ID_ONE(state_cstrlen)
929IREP_ID_ONE(state_is_cstring)
930IREP_ID_ONE(state_is_dynamic_object)
931IREP_ID_ONE(state_is_sentinel_dll)
932IREP_ID_ONE(state_live_object)
933IREP_ID_ONE(state_writeable_object)
934IREP_ID_ONE(state_object_size)
935IREP_ID_TWO(overflow_result_plus, overflow_result-+)
936IREP_ID_TWO(overflow_result_minus, overflow_result--)
937IREP_ID_TWO(overflow_result_mult, overflow_result-*)
938IREP_ID_TWO(overflow_result_shl, overflow_result-shl)
939IREP_ID_TWO(overflow_result_unary_minus, overflow_result-unary-)
940IREP_ID_ONE(field_sensitive_ssa)
941IREP_ID_ONE(checked_assigns)
942IREP_ID_ONE(enum_is_in_range)
943IREP_ID_ONE(prophecy_rw_ok)
944IREP_ID_ONE(prophecy_r_ok)
945IREP_ID_ONE(prophecy_w_ok)
946IREP_ID_ONE(prophecy_pointer_in_range)
947IREP_ID_ONE(bit_cast)
948
949// Projects depending on this code base that wish to extend the list of
950// available ids should provide a file local_irep_ids.def in their source tree
951// and add -D'LOCAL_IREP_IDS=<project/local_irep_ids.def>' to their compiler
952// command line.
953#ifdef LOCAL_IREP_IDS
954#include LOCAL_IREP_IDS
955#endif
956
957#undef IREP_ID_ONE
958#undef IREP_ID_TWO
is_failed_symbol
bool is_failed_symbol(const exprt &expr)
Return true if, and only if, expr is the result of failed dereferencing.
Definition add_failed_symbols.h:38
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition arith_tools.cpp:219
is_operator
static bool is_operator(const ctokent &t)
Definition ctoken.h:78
main
int main(int argc, char *argv[])
Definition file_converter.cpp:19
implicit
static bool implicit(goto_programt::const_targett target)
Definition full_slicer.cpp:234
dereference
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets, message_handlert &message_handler)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
Definition goto_program_dereference.cpp:278
IREP_ID_TWO
#define IREP_ID_TWO(id, str)
Definition irep_ids.cpp:31
IREP_ID_ONE
#define IREP_ID_ONE(id)
Definition irep_ids.cpp:30
idt::id_class
@ id_class
Definition irep_ids.cpp:181
to_member
static member_exprt to_member(const exprt &pointer, const fieldref_exprt &field_reference, const namespacet &ns)
Build a member exprt for accessing a specific field that may come from a base class.
Definition java_bytecode_convert_method.cpp:656
isnan
int isnan(double d)
Definition math.c:163
isinf
int isinf(double d)
Definition math.c:119
isnormal
int isnormal(double d)
Definition math.c:207
isfinite
int isfinite(double d)
Definition math.c:101
restrict
mini_bddt restrict(const mini_bddt &u, unsigned var, const bool value)
Definition miniBDD.cpp:571
exists
mini_bddt exists(const mini_bddt &u, const unsigned var)
Definition miniBDD.cpp:576
alignment
mp_integer alignment(const typet &type, const namespacet &ns)
Definition padding.cpp:23
pointer_offset
exprt pointer_offset(const exprt &pointer)
Definition pointer_predicates.cpp:38
integer_address
exprt integer_address(const exprt &pointer)
Definition pointer_predicates.cpp:65
object_size
exprt object_size(const exprt &pointer)
Definition pointer_predicates.cpp:33
null_object
exprt null_object(const exprt &pointer)
Definition pointer_predicates.cpp:59
pointer_object
exprt pointer_object(const exprt &p)
Definition pointer_predicates.cpp:23
postcondition
void postcondition(const namespacet &ns, const value_sett &value_set, const symex_target_equationt &equation, const goto_symex_statet &s, exprt &dest)
Definition postcondition.cpp:51
precondition
void precondition(const namespacet &ns, value_setst &value_sets, const goto_programt::const_targett target, const symex_target_equationt &equation, const goto_symex_statet &s, exprt &dest, message_handlert &message_handler)
Definition precondition.cpp:57
comment
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition race_check.cpp:108
L2
@ L2
Definition renamed.h:26
L0
@ L0
Definition renamed.h:23
L1
@ L1
Definition renamed.h:24
printf
int printf(const char *format,...)
Definition stdio.c:1470
abs
int abs(int i)
Definition stdlib.c:10
floatbv_mult
exprt floatbv_mult(const exprt &f, const exprt &g)
Multiplication of expressions representing floating points.
Definition string_constraint_generator_float.cpp:105