1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
Finished checking --- no warnings
impabstract.c: (in function f)
impabstract.c:11:7: Left operand of < is abstract type (mint): m < 2
An abstraction barrier is broken. If necessary, use /*@access <type>@*/ to
allow access to an abstract type. (Use -abstract to inhibit warning)
impabstract.c:13:14: Return value type mint does not match declared type int: m
Underlying types match, but mint is an abstract type that is not accessible
here.
Finished checking --- 2 code warnings, as expected
impabstract.c:2:28: Mutable abstract type cint declared without pointer
indirection: int (violates assignment semantics)
LCL semantics requires that a mutable type exhibits sharing semantics. In
order for objects to be shared a indirection is necessary in the
representation. A mutable type may be represented by a pointer or an abstract
mutable type. Handles into static data are fine, too, but will generate this
error message unless it is suppressed. (Use -mutrep to inhibit warning)
impabstract.c:2:28: Datatype cint inconsistently declared as concrete type
A function, variable or constant is redefined with a different type. (Use
-incondefs to inhibit warning)
impabstract.lcl:2:1: Specification of cint
impabstract.c: (in function f)
impabstract.c:6:7: Left operand of > is abstract type (cint): c > 3
An abstraction barrier is broken. If necessary, use /*@access <type>@*/ to
allow access to an abstract type. (Use -abstract to inhibit warning)
impabstract.c:8:14: Return value type cint does not match declared type int: c
Underlying types match, but cint is an abstract type that is not accessible
here.
Finished checking --- 4 code warnings, as expected
|
