ANSI-C Language Type Checking. More...

#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/cprover_prefix.h>
#include <util/pointer_expr.h>
#include <util/std_types.h>
#include <util/string_constant.h>
#include <util/symbol_table_base.h>
#include <goto-programs/goto_instruction_code.h>
#include "c_expr.h"
#include "c_typecheck_base.h"
#include <atomic>

Include dependency graph for c_typecheck_gcc_polymorphic_builtins.cpp:

Go to the source code of this file.

Functions
static symbol_exprt	typecheck_sync_with_pointer_parameter (const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)

static symbol_exprt	typecheck_sync_compare_swap (const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)

static symbol_exprt	typecheck_sync_lock_release (const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)

static symbol_exprt	typecheck_atomic_load_n (const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)

static symbol_exprt	typecheck_atomic_store_n (const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)

static symbol_exprt	typecheck_atomic_exchange_n (const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)

static symbol_exprt	typecheck_atomic_load_store (const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)

static symbol_exprt	typecheck_atomic_exchange (const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)

static symbol_exprt	typecheck_atomic_compare_exchange (const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)

static symbol_exprt	typecheck_atomic_op_fetch (const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)

static symbol_exprt	typecheck_atomic_fetch_op (const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)

static symbolt	result_symbol (const irep_idt &identifier, const typet &type, const source_locationt &source_location, symbol_table_baset &symbol_table)

static void	instantiate_atomic_fetch_op (const irep_idt &identifier, const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, symbol_table_baset &symbol_table, code_blockt &block)

static void	instantiate_atomic_op_fetch (const irep_idt &identifier, const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, symbol_table_baset &symbol_table, code_blockt &block)

static void	instantiate_sync_fetch (const irep_idt &identifier, const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)

static void	instantiate_sync_bool_compare_and_swap (const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)

static void	instantiate_sync_val_compare_and_swap (const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, symbol_table_baset &symbol_table, code_blockt &block)

static void	instantiate_sync_lock_test_and_set (const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, symbol_table_baset &symbol_table, code_blockt &block)

static void	instantiate_sync_lock_release (const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)

static void	instantiate_atomic_load (const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)

static void	instantiate_atomic_load_n (const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, symbol_table_baset &symbol_table, code_blockt &block)

static void	instantiate_atomic_store (const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)

static void	instantiate_atomic_store_n (const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)

static void	instantiate_atomic_exchange (const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)

static void	instantiate_atomic_exchange_n (const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, symbol_table_baset &symbol_table, code_blockt &block)

static void	instantiate_atomic_compare_exchange (const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, symbol_table_baset &symbol_table, code_blockt &block)

static void	instantiate_atomic_compare_exchange_n (const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)

Detailed Description

ANSI-C Language Type Checking.

Definition in file c_typecheck_gcc_polymorphic_builtins.cpp.

Function Documentation

◆ instantiate_atomic_compare_exchange()

static void instantiate_atomic_compare_exchange	(	const irep_idt &	identifier_with_type,
		const code_typet &	code_type,
		const source_locationt &	source_location,
		const std::vector< symbol_exprt > &	parameter_exprs,
		symbol_table_baset &	symbol_table,
		code_blockt &	block
	)

static

Definition at line 1137 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ instantiate_atomic_compare_exchange_n()

static void instantiate_atomic_compare_exchange_n	(	const irep_idt &	identifier_with_type,
		const code_typet &	code_type,
		const source_locationt &	source_location,
		const std::vector< symbol_exprt > &	parameter_exprs,
		code_blockt &	block
	)

static

Definition at line 1215 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ instantiate_atomic_exchange()

static void instantiate_atomic_exchange	(	const irep_idt &	identifier_with_type,
		const code_typet &	code_type,
		const source_locationt &	source_location,
		const std::vector< symbol_exprt > &	parameter_exprs,
		code_blockt &	block
	)

static

Definition at line 1070 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ instantiate_atomic_exchange_n()

static void instantiate_atomic_exchange_n	(	const irep_idt &	identifier_with_type,
		const code_typet &	code_type,
		const source_locationt &	source_location,
		const std::vector< symbol_exprt > &	parameter_exprs,
		symbol_table_baset &	symbol_table,
		code_blockt &	block
	)

static

Definition at line 1106 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ instantiate_atomic_fetch_op()

static void instantiate_atomic_fetch_op	(	const irep_idt &	identifier,
		const irep_idt &	identifier_with_type,
		const code_typet &	code_type,
		const source_locationt &	source_location,
		const std::vector< symbol_exprt > &	parameter_exprs,
		symbol_table_baset &	symbol_table,
		code_blockt &	block
	)

static

Definition at line 628 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ instantiate_atomic_load()

static void instantiate_atomic_load	(	const irep_idt &	identifier_with_type,
		const code_typet &	code_type,
		const source_locationt &	source_location,
		const std::vector< symbol_exprt > &	parameter_exprs,
		code_blockt &	block
	)

static

Definition at line 953 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ instantiate_atomic_load_n()

static void instantiate_atomic_load_n	(	const irep_idt &	identifier_with_type,
		const code_typet &	code_type,
		const source_locationt &	source_location,
		const std::vector< symbol_exprt > &	parameter_exprs,
		symbol_table_baset &	symbol_table,
		code_blockt &	block
	)

static

Definition at line 987 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ instantiate_atomic_op_fetch()

static void instantiate_atomic_op_fetch	(	const irep_idt &	identifier,
		const irep_idt &	identifier_with_type,
		const code_typet &	code_type,
		const source_locationt &	source_location,
		const std::vector< symbol_exprt > &	parameter_exprs,
		symbol_table_baset &	symbol_table,
		code_blockt &	block
	)

static

Definition at line 691 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ instantiate_atomic_store()

static void instantiate_atomic_store	(	const irep_idt &	identifier_with_type,
		const code_typet &	code_type,
		const source_locationt &	source_location,
		const std::vector< symbol_exprt > &	parameter_exprs,
		code_blockt &	block
	)

static

Definition at line 1015 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ instantiate_atomic_store_n()

static void instantiate_atomic_store_n	(	const irep_idt &	identifier_with_type,
		const code_typet &	code_type,
		const source_locationt &	source_location,
		const std::vector< symbol_exprt > &	parameter_exprs,
		code_blockt &	block
	)

static

Definition at line 1049 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ instantiate_sync_bool_compare_and_swap()

static void instantiate_sync_bool_compare_and_swap	(	const irep_idt &	identifier_with_type,
		const code_typet &	code_type,
		const source_locationt &	source_location,
		const std::vector< symbol_exprt > &	parameter_exprs,
		code_blockt &	block
	)

static

Definition at line 779 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ instantiate_sync_fetch()

static void instantiate_sync_fetch	(	const irep_idt &	identifier,
		const irep_idt &	identifier_with_type,
		const code_typet &	code_type,
		const source_locationt &	source_location,
		const std::vector< symbol_exprt > &	parameter_exprs,
		code_blockt &	block
	)

static

Definition at line 755 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ instantiate_sync_lock_release()

static void instantiate_sync_lock_release	(	const irep_idt &	identifier_with_type,
		const code_typet &	code_type,
		const source_locationt &	source_location,
		const std::vector< symbol_exprt > &	parameter_exprs,
		code_blockt &	block
	)

static

Definition at line 913 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ instantiate_sync_lock_test_and_set()

static void instantiate_sync_lock_test_and_set	(	const irep_idt &	identifier_with_type,
		const code_typet &	code_type,
		const source_locationt &	source_location,
		const std::vector< symbol_exprt > &	parameter_exprs,
		symbol_table_baset &	symbol_table,
		code_blockt &	block
	)

static

Definition at line 857 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ instantiate_sync_val_compare_and_swap()

static void instantiate_sync_val_compare_and_swap	(	const irep_idt &	identifier_with_type,
		const code_typet &	code_type,
		const source_locationt &	source_location,
		const std::vector< symbol_exprt > &	parameter_exprs,
		symbol_table_baset &	symbol_table,
		code_blockt &	block
	)

static

Definition at line 807 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ result_symbol()

static symbolt result_symbol	(	const irep_idt &	identifier,
		const typet &	type,
		const source_locationt &	source_location,
		symbol_table_baset &	symbol_table
	)

static

Definition at line 610 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ typecheck_atomic_compare_exchange()

static symbol_exprt typecheck_atomic_compare_exchange	(	const irep_idt &	identifier,
		const exprt::operandst &	arguments,
		const source_locationt &	source_location,
		message_handlert &	message_handler
	)

static

Definition at line 353 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ typecheck_atomic_exchange()

static symbol_exprt typecheck_atomic_exchange	(	const irep_idt &	identifier,
		const exprt::operandst &	arguments,
		const source_locationt &	source_location,
		message_handlert &	message_handler
	)

static

Definition at line 300 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ typecheck_atomic_exchange_n()

static symbol_exprt typecheck_atomic_exchange_n	(	const irep_idt &	identifier,
		const exprt::operandst &	arguments,
		const source_locationt &	source_location,
		message_handlert &	message_handler
	)

static

Definition at line 217 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ typecheck_atomic_fetch_op()

static symbol_exprt typecheck_atomic_fetch_op	(	const irep_idt &	identifier,
		const exprt::operandst &	arguments,
		const source_locationt &	source_location,
		message_handlert &	message_handler
	)

static

Definition at line 456 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ typecheck_atomic_load_n()

static symbol_exprt typecheck_atomic_load_n	(	const irep_idt &	identifier,
		const exprt::operandst &	arguments,
		const source_locationt &	source_location,
		message_handlert &	message_handler
	)

static

Definition at line 144 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ typecheck_atomic_load_store()

static symbol_exprt typecheck_atomic_load_store	(	const irep_idt &	identifier,
		const exprt::operandst &	arguments,
		const source_locationt &	source_location,
		message_handlert &	message_handler
	)

static

Definition at line 255 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ typecheck_atomic_op_fetch()

static symbol_exprt typecheck_atomic_op_fetch	(	const irep_idt &	identifier,
		const exprt::operandst &	arguments,
		const source_locationt &	source_location,
		message_handlert &	message_handler
	)

static

Definition at line 419 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ typecheck_atomic_store_n()

static symbol_exprt typecheck_atomic_store_n	(	const irep_idt &	identifier,
		const exprt::operandst &	arguments,
		const source_locationt &	source_location,
		message_handlert &	message_handler
	)

static

Definition at line 179 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ typecheck_sync_compare_swap()

static symbol_exprt typecheck_sync_compare_swap	(	const irep_idt &	identifier,
		const exprt::operandst &	arguments,
		const source_locationt &	source_location,
		message_handlert &	message_handler
	)

static

Definition at line 66 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ typecheck_sync_lock_release()

static symbol_exprt typecheck_sync_lock_release	(	const irep_idt &	identifier,
		const exprt::operandst &	arguments,
		const source_locationt &	source_location,
		message_handlert &	message_handler
	)

static

Definition at line 109 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ typecheck_sync_with_pointer_parameter()

static symbol_exprt typecheck_sync_with_pointer_parameter	(	const irep_idt &	identifier,
		const exprt::operandst &	arguments,
		const source_locationt &	source_location,
		message_handlert &	message_handler
	)

static

Definition at line 27 of file c_typecheck_gcc_polymorphic_builtins.cpp.

Functions

Detailed Description

Function Documentation

◆ instantiate_atomic_compare_exchange()

◆ instantiate_atomic_compare_exchange_n()

◆ instantiate_atomic_exchange()

◆ instantiate_atomic_exchange_n()

◆ instantiate_atomic_fetch_op()

◆ instantiate_atomic_load()

◆ instantiate_atomic_load_n()

◆ instantiate_atomic_op_fetch()

◆ instantiate_atomic_store()

◆ instantiate_atomic_store_n()

◆ instantiate_sync_bool_compare_and_swap()

◆ instantiate_sync_fetch()

◆ instantiate_sync_lock_release()

◆ instantiate_sync_lock_test_and_set()

◆ instantiate_sync_val_compare_and_swap()

◆ result_symbol()

◆ typecheck_atomic_compare_exchange()

◆ typecheck_atomic_exchange()

◆ typecheck_atomic_exchange_n()

◆ typecheck_atomic_fetch_op()

◆ typecheck_atomic_load_n()

◆ typecheck_atomic_load_store()

◆ typecheck_atomic_op_fetch()

◆ typecheck_atomic_store_n()

◆ typecheck_sync_compare_swap()

◆ typecheck_sync_lock_release()

◆ typecheck_sync_with_pointer_parameter()