Как вызвать функцию проверки абстрактных типов Splint?

Question

Я хочу использовать тутор для обнаружения неявных приведений между typedef с с тем же базовым типом, например, в следующем коде:

typedef int counter; 
typedef int delta; 

static int func(int a, int b, int c) 
{ 
    return a + b + c; 
} 

int main(void) 
{ 
    int a = 5; 
    counter b = a; 
    delta c = (int) 8; 
    return func(a, b, c); 
} 

Похоже, что я могу использовать Splint для этого, но он не дает любые предупреждения. Даже аннотирование как typedef s, так и abstract не вызывает его.

Как получить шину для проверки типа «сильный», как это?

Answer 1

Поскольку вы используете типы в том же файле, в котором они объявлены, Splint предполагает, что файл имеет доступ к абстрактному типу. Вы должны сказать Splint, что файл не имеет доступа к внутренним элементам абстрактного типа, используя @ noaccess @. Например, вы можете сделать

typedef /*@abstract@*/ int counter; /*@noaccess counter@*/ 
typedef /*@abstract@*/ int delta; /*@noaccess delta@*/ 

int main(void) 
{ 
    int a = 5; 
    counter /*@unused@*/ b = a; 
    delta /*@unused@*/ c = (int) 8; 
    return 0; 
} 

Обратите внимание, что вы получите предупреждение не только при назначении б, но и с, даже с актерами.