cprover
c_typecheck_gcc_polymorphic_builtins.cpp File Reference

ANSI-C Language Type Checking. More...

#include "c_typecheck_base.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/cprover_prefix.h>
#include <util/std_types.h>
#include <util/string_constant.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_tablet &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_tablet &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_tablet &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_tablet &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_tablet &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_tablet &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_tablet &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_tablet &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_tablet symbol_table,
code_blockt block 
)
static

Definition at line 1118 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 1190 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 1053 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_tablet symbol_table,
code_blockt block 
)
static

Definition at line 1088 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_tablet symbol_table,
code_blockt block 
)
static

Definition at line 618 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 940 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_tablet symbol_table,
code_blockt block 
)
static

Definition at line 973 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_tablet symbol_table,
code_blockt block 
)
static

Definition at line 680 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 1000 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 1033 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 767 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 743 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 900 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_tablet symbol_table,
code_blockt block 
)
static

Definition at line 844 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_tablet symbol_table,
code_blockt block 
)
static

Definition at line 794 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_tablet symbol_table 
)
static

Definition at line 597 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 342 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 289 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 208 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 444 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 137 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 244 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 407 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 172 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 59 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 102 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 22 of file c_typecheck_gcc_polymorphic_builtins.cpp.