|
# 1 "/home/druidos/development/work/ldv-tools/install/kernel-rules/models/resource/dma-mapping.aspect"
|
|
# 1 "<built-in>"
|
|
# 1 "<command-line>"
|
|
# 1 "/home/druidos/development/work/ldv-tools/install/ri/ri.aspect" 1
|
|
# 1 "<command-line>" 2
|
|
# 1 "/home/druidos/development/work/ldv-tools/install/kernel-rules/models/resource/dma-mapping.aspect"
|
|
before: file("$this")
|
|
{
|
|
#include <linux/types.h>
|
|
#include <linux/dma-direction.h>
|
|
|
|
extern dma_addr_t ldv_dma_map_page(struct device *dev, struct page *page, size_t offset, size_t size, enum dma_data_direction dir);
|
|
extern dma_addr_t ldv_dma_map_single(struct device *dev, void *cpu_addr, size_t size, enum dma_data_direction dir);
|
|
extern dma_addr_t ldv_dma_map_single_attrs(struct device *dev, void *ptr, size_t size, enum dma_data_direction dir, struct dma_attrs *attrs);
|
|
extern int ldv_dma_mapping_error(struct device *dev, dma_addr_t dma_addr);
|
|
}
|
|
|
|
around: call(static inline dma_addr_t dma_map_page(struct device *dev, struct page *page, size_t offset, size_t size, enum dma_data_direction dir))
|
|
{
|
|
return ldv_dma_map_page($arg1, $arg2, $arg3, $arg4, $arg5);
|
|
}
|
|
|
|
around: call(dma_addr_t dma_map_single(struct device *dev, void *cpu_addr, size_t size, enum dma_data_direction dir))
|
|
{
|
|
return ldv_dma_map_single($arg1, $arg2, $arg3, $arg4);
|
|
}
|
|
|
|
around: call(static inline int dma_mapping_error(struct device *dev, dma_addr_t dma_addr))
|
|
{
|
|
return ldv_dma_mapping_error($arg1, $arg2);
|
|
}
|
|
|
|
around: call(static inline dma_addr_t dma_map_single_attrs(struct device *dev, void *ptr, size_t size, enum dma_data_direction dir, struct dma_attrs *attrs))
|
|
{
|
|
return ldv_dma_map_single_attrs($arg1, $arg2, $arg3, $arg4, $arg5);
|
|
}
|
|
|
|
new: file("$env<LDV_COMMON_MODEL>")
|
|
{
|
|
#include <linux/types.h>
|
|
#include <linux/dma-direction.h>
|
|
#include <verifier/rcv.h>
|
|
#include <verifier/set.h>
|
|
#include <verifier/map.h>
|
|
|
|
Set LDV_DMA_MAP_CALLS;
|
|
|
|
/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_dma_map_page') maps page */
|
|
dma_addr_t ldv_dma_map_page(struct device *dev, struct page *page, size_t offset, size_t size, enum dma_data_direction dir) {
|
|
dma_addr_t nonedetermined;
|
|
|
|
nonedetermined = ldv_undef_ptr();
|
|
|
|
/* LDV_COMMENT_ASSERT Check that previos dma_mapping call was checked*/
|
|
ldv_assert(ldv_set_is_empty(LDV_DMA_MAP_CALLS));
|
|
|
|
ldv_set_add(LDV_DMA_MAP_CALLS, nonedetermined);
|
|
|
|
return nonedetermined;
|
|
}
|
|
|
|
/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_dma_mapping_error') unmaps page */
|
|
int ldv_dma_mapping_error(struct device *dev, dma_addr_t dma_addr) {
|
|
|
|
/* LDV_COMMENT_ASSERT No dma_mapping calls to verify */
|
|
ldv_assert(ldv_set_contains(LDV_DMA_MAP_CALLS, dma_addr));
|
|
ldv_set_remove(LDV_DMA_MAP_CALLS, dma_addr);
|
|
|
|
int nonedetermined;
|
|
|
|
nonedetermined = ldv_undef_int();
|
|
|
|
return nonedetermined;
|
|
}
|
|
|
|
|
|
|
|
/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_dma_map_single') maps pci_dma */
|
|
dma_addr_t ldv_dma_map_single(struct device *dev, void *cpu_addr, size_t size, enum dma_data_direction dir) {
|
|
dma_addr_t nonedetermined;
|
|
|
|
nonedetermined = ldv_undef_ptr();
|
|
|
|
/* LDV_COMMENT_ASSERT Check that previos dma_mapping call was checked*/
|
|
ldv_assert(ldv_set_is_empty(LDV_DMA_MAP_CALLS));
|
|
|
|
ldv_set_add(LDV_DMA_MAP_CALLS, nonedetermined);
|
|
|
|
return nonedetermined;
|
|
}
|
|
|
|
/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_dma_map_single_attrs') maps pci_dma */
|
|
dma_addr_t ldv_dma_map_single_attrs(struct device *dev, void *ptr, size_t size, enum dma_data_direction dir, struct dma_attrs *attrs) {
|
|
dma_addr_t nonedetermined;
|
|
|
|
nonedetermined = ldv_undef_ptr();
|
|
|
|
/* LDV_COMMENT_ASSERT Check that previos dma_mapping call was checked*/
|
|
ldv_assert(ldv_set_is_empty(LDV_DMA_MAP_CALLS));
|
|
|
|
ldv_set_add(LDV_DMA_MAP_CALLS, nonedetermined);
|
|
|
|
return nonedetermined;
|
|
}
|
|
|
|
/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_initialize') Initialize all module reference counters at the beginning */
|
|
void ldv_initialize(void) {
|
|
/* LDV_COMMENT_CHANGE_STATE All module reference counters have some initial value at the beginning */
|
|
ldv_set_init(LDV_DMA_MAP_CALLS);
|
|
}
|
|
|
|
/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_check_final_state') Check that all module reference counters have their initial values at the end */
|
|
void ldv_check_final_state(void) {
|
|
/* LDV_COMMENT_ASSERT All incremented module reference counters should be decremented before module unloading*/
|
|
ldv_assert(ldv_set_is_empty(LDV_DMA_MAP_CALLS));
|
|
}
|
|
|
|
}
|