Commit efe00459 authored by David Bühler's avatar David Bühler
Browse files

[Eva] Adds a test for the alarm about the creation of invalid pointers.

parent 72781a63
/* run.config*
STDOPT: +"-warn-invalid-pointer -absolute-valid-range=10-30"
STDOPT: +"-no-warn-invalid-pointer -absolute-valid-range=10-30"
*/
#include <__fc_builtin.h>
#include <stdint.h>
/* Tests the emission of \object_pointer alarms when -warn-invalid-pointer
is enabled. The second run should emit no alarm. */
volatile int undet;
/* Simple pointer computations. */
void pointer_computation () {
int x;
int *p = &x;
if (undet)
p--; // Red alarm.
p++; // No alarm.
if (undet)
p++; // Red alarm.
int i = undet;
p += i; // Unknown alarm. [i] should be reduced to {-1, 0}.
int j = undet;
p -= j; // Unknown alarm. [j] should be reduced to {-1, 0, 1}.
p --; // Unknown alarm. [p] should be exactly {&x}.
int array[25];
int *q = undet ? &x : &array[0];
int offset1 = Frama_C_interval(0, 10);
q += offset1; // Unknown alarm. [offset1] should not be reduced.
int offset2 = Frama_C_interval(0, 50);
q += offset2; // Unknown alarm. [offset2] should be reduced to [0..25].
q += 0; // No alarm.
}
/* Increment or decrement pointers in loops. */
void pointer_in_loops () {
int t[128];
int *p = &t[0];
/*@ loop unroll 128; */
for (int i = 0; i < 128; i++) {
*p = i;
p++; // No alarm.
}
if (undet) {
int *q = &t[127];
/*@ loop unroll 128; */
for (int i = 0; i < 128; i++) {
*q = i;
q--; // Alarm in the last iteration: q points to t[-1].
}
Frama_C_show_each_bottom(q); // Should not be reached.
}
}
/* Conversion integer -> pointer. */
void int_conversion () {
int x, *p;
p = (int *)0; // NULL pointer: always ok.
p = (int *) 20; // Inside -absolute-valid-range: no alarms.
if (undet) {
p = (int *) 42; // Outside -absolute-valid-range: red alarm.
}
x = Frama_C_interval(15, 25);
p = (int *) x; // Inside -absolute-valid-range: no alarms.
x = Frama_C_interval(100, 500);
if (undet) {
p = (int *) x; // Outside -absolute-valid-range: red alarm.
}
x = Frama_C_interval(15, 100);
p = (int *) x; // Unknown alarm. [x] should be reduced to [15..31].
p = (int *) undet; // Unknown alarm. [p] should be have value in [0..31].
}
void addrof () {
int a[10], *p;
p = &(a[0]);
p = &(a[10]);
if (undet)
p = &(a[11]); // Invalid alarm
if (undet)
p = &(a[-1]); // Invalid alarm
int offset = undet;
p = &(a[offset]); /* Unknown alarm. [offset] should be reduced to [0..10]. */
}
typedef union {
uintptr_t integer;
int *pointer;
} ptr_union;
/* Creates invalid pointers through an union. */
void union_pointer () {
int *p;
ptr_union u;
u.integer = 0;
p = u.pointer; // No alarm.
if (undet) {
u.integer = 42;
p = u.pointer; // Red alarm.
}
u.integer = undet;
p = u.pointer; // Unknown alarm. [u.integer] should be reduced to [0..31].
}
/* Creates invalid pointers through untyped writes. */
void write_pointer () {
int x;
int *p = 0;
*((uintptr_t *) &p) = &x;
int *q = p; // No alarm.
*((uintptr_t *) &p) = (uintptr_t)p + undet;
q = p; // Unknown alarm.
*((uintptr_t *) &p) = 42;
if (undet) {
q = p; // Red alarm.
}
}
/* Tests the evaluation of the logical predicate \object_pointer when
-warn-invalid-pointer is disabled. */
void object_pointer_predicate () {
int x, array[64];
int *p = &x;
/*@ assert \object_pointer(p); */
if (undet) {
p--;
/*@ assert \object_pointer(p); */
}
p++;
/*@ assert \object_pointer(p); */
if (undet) {
p++;
/*@ assert \object_pointer(p); */
}
p += undet;
/*@ assert \object_pointer(p); */
/*@ assert \object_pointer(p); */
Frama_C_show_each_object_pointer(p);
p = (int *)((uintptr_t)&x + undet);
/*@ assert \object_pointer(p); */
/*@ assert \object_pointer(p); */
Frama_C_show_each_object_pointer_char(p);
int i = Frama_C_interval(0, 20);
p = undet ? &x : &array[i];
/*@ assert \object_pointer(p); */
p += i;
/*@ assert \object_pointer(p); */
p += undet;
/*@ assert \object_pointer(p); */
Frama_C_show_each_object_pointer_array(p);
p = (int *) 0;
/*@ assert \object_pointer(p); */
if (undet)
p = (int *) 20;
/*@ assert \object_pointer(p); */
if (undet)
p = (int *) 50;
/*@ assert \object_pointer(p); */
p = (int *) undet;
/*@ assert \object_pointer(p); */
if (undet) {
p = (int *) 100;
/*@ assert \object_pointer(p); */
}
}
void main () {
pointer_computation ();
pointer_in_loops ();
int_conversion ();
addrof ();
union_pointer ();
write_pointer ();
object_pointer_predicate ();
}
[kernel] Parsing tests/value/invalid_pointer.c (with preprocessing)
[kernel:typing:int-conversion] tests/value/invalid_pointer.c:111: Warning:
Conversion from a pointer to an integer without an explicit cast
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
NULL[rbits 80 to 247] ∈ [--..--]
undet ∈ [--..--]
[eva] computing for function pointer_computation <- main.
Called from tests/value/invalid_pointer.c:171.
[eva:alarm] tests/value/invalid_pointer.c:19: Warning:
invalid pointer creation. assert \object_pointer(p - 1);
[eva:alarm] tests/value/invalid_pointer.c:22: Warning:
invalid pointer creation. assert \object_pointer(p + 1);
[eva:alarm] tests/value/invalid_pointer.c:24: Warning:
invalid pointer creation. assert \object_pointer(p + i);
[eva:alarm] tests/value/invalid_pointer.c:26: Warning:
invalid pointer creation. assert \object_pointer(p - j);
[eva:alarm] tests/value/invalid_pointer.c:27: Warning:
invalid pointer creation. assert \object_pointer(p - 1);
[eva] computing for function Frama_C_interval <- pointer_computation <- main.
Called from tests/value/invalid_pointer.c:30.
[eva] using specification for function Frama_C_interval
[eva] tests/value/invalid_pointer.c:30:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva:alarm] tests/value/invalid_pointer.c:31: Warning:
invalid pointer creation. assert \object_pointer(q + offset1);
[eva] computing for function Frama_C_interval <- pointer_computation <- main.
Called from tests/value/invalid_pointer.c:32.
[eva] tests/value/invalid_pointer.c:32:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva:alarm] tests/value/invalid_pointer.c:33: Warning:
invalid pointer creation. assert \object_pointer(q + offset2);
[eva] Recording results for pointer_computation
[eva] Done for function pointer_computation
[eva] computing for function pointer_in_loops <- main.
Called from tests/value/invalid_pointer.c:172.
[eva] tests/value/invalid_pointer.c:42:
Trace partitioning superposing up to 100 states
[eva:alarm] tests/value/invalid_pointer.c:51: Warning:
invalid pointer creation. assert \object_pointer(q - 1);
[eva] Recording results for pointer_in_loops
[eva] Done for function pointer_in_loops
[eva] computing for function int_conversion <- main.
Called from tests/value/invalid_pointer.c:173.
[eva:alarm] tests/value/invalid_pointer.c:63: Warning:
invalid pointer creation. assert \object_pointer((int *)42);
[eva] computing for function Frama_C_interval <- int_conversion <- main.
Called from tests/value/invalid_pointer.c:65.
[eva] tests/value/invalid_pointer.c:65:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- int_conversion <- main.
Called from tests/value/invalid_pointer.c:67.
[eva] tests/value/invalid_pointer.c:67:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva:alarm] tests/value/invalid_pointer.c:69: Warning:
invalid pointer creation. assert \object_pointer((int *)x);
[eva] computing for function Frama_C_interval <- int_conversion <- main.
Called from tests/value/invalid_pointer.c:71.
[eva] tests/value/invalid_pointer.c:71:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva:alarm] tests/value/invalid_pointer.c:72: Warning:
invalid pointer creation. assert \object_pointer((int *)x);
[eva:alarm] tests/value/invalid_pointer.c:73: Warning:
invalid pointer creation. assert \object_pointer((int *)undet);
[eva] Recording results for int_conversion
[eva] Done for function int_conversion
[eva] computing for function addrof <- main.
Called from tests/value/invalid_pointer.c:174.
[eva:alarm] tests/value/invalid_pointer.c:81: Warning:
invalid pointer creation. assert \object_pointer(&a[11]);
[eva:alarm] tests/value/invalid_pointer.c:83: Warning:
invalid pointer creation. assert \object_pointer(&a[(int)(-1)]);
[eva:alarm] tests/value/invalid_pointer.c:85: Warning:
invalid pointer creation. assert \object_pointer(&a[offset]);
[eva] Recording results for addrof
[eva] Done for function addrof
[eva] computing for function union_pointer <- main.
Called from tests/value/invalid_pointer.c:175.
[eva:alarm] tests/value/invalid_pointer.c:101: Warning:
invalid pointer creation. assert \object_pointer(u.pointer);
[eva:alarm] tests/value/invalid_pointer.c:104: Warning:
invalid pointer creation. assert \object_pointer(u.pointer);
[eva] Recording results for union_pointer
[eva] Done for function union_pointer
[eva] computing for function write_pointer <- main.
Called from tests/value/invalid_pointer.c:176.
[eva:alarm] tests/value/invalid_pointer.c:114: Warning:
invalid pointer creation. assert \object_pointer(p);
[eva:alarm] tests/value/invalid_pointer.c:117: Warning:
invalid pointer creation. assert \object_pointer(p);
[eva] Recording results for write_pointer
[eva] Done for function write_pointer
[eva] computing for function object_pointer_predicate <- main.
Called from tests/value/invalid_pointer.c:177.
[eva] tests/value/invalid_pointer.c:126: assertion got status valid.
[eva:alarm] tests/value/invalid_pointer.c:128: Warning:
invalid pointer creation. assert \object_pointer(p - 1);
[eva] tests/value/invalid_pointer.c:132: assertion got status valid.
[eva:alarm] tests/value/invalid_pointer.c:134: Warning:
invalid pointer creation. assert \object_pointer(p + 1);
[eva:alarm] tests/value/invalid_pointer.c:137: Warning:
invalid pointer creation. assert \object_pointer(p + undet);
[eva] tests/value/invalid_pointer.c:138: assertion got status valid.
[eva] tests/value/invalid_pointer.c:139: assertion got status valid.
[eva] tests/value/invalid_pointer.c:140:
Frama_C_show_each_object_pointer: {{ &x + {0; 4} }}
[eva:alarm] tests/value/invalid_pointer.c:141: Warning:
invalid pointer creation.
assert
\object_pointer((int *)((unsigned int)((unsigned int)(&x) +
(unsigned int)undet)));
[eva] tests/value/invalid_pointer.c:142: assertion got status valid.
[eva] tests/value/invalid_pointer.c:143: assertion got status valid.
[eva] tests/value/invalid_pointer.c:144:
Frama_C_show_each_object_pointer_char: {{ &x + {0; 1; 2; 3; 4} }}
[eva] computing for function Frama_C_interval <- object_pointer_predicate <- main.
Called from tests/value/invalid_pointer.c:145.
[eva] tests/value/invalid_pointer.c:145:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] tests/value/invalid_pointer.c:147: assertion got status valid.
[eva:alarm] tests/value/invalid_pointer.c:148: Warning:
invalid pointer creation. assert \object_pointer(p + i);
[eva] tests/value/invalid_pointer.c:149: assertion got status valid.
[eva:alarm] tests/value/invalid_pointer.c:150: Warning:
invalid pointer creation. assert \object_pointer(p + undet);
[eva] tests/value/invalid_pointer.c:151: assertion got status valid.
[eva] tests/value/invalid_pointer.c:152:
Frama_C_show_each_object_pointer_array:
{{ &x + {0; 4} ; &array + [0..256],0%4 }}
[eva] tests/value/invalid_pointer.c:154: assertion got status valid.
[eva:alarm] tests/value/invalid_pointer.c:157: Warning:
assertion got status unknown.
[eva:alarm] tests/value/invalid_pointer.c:159: Warning:
invalid pointer creation. assert \object_pointer((int *)50);
[eva:alarm] tests/value/invalid_pointer.c:160: Warning:
assertion got status unknown.
[eva:alarm] tests/value/invalid_pointer.c:161: Warning:
invalid pointer creation. assert \object_pointer((int *)undet);
[eva:alarm] tests/value/invalid_pointer.c:162: Warning:
assertion got status unknown.
[eva:alarm] tests/value/invalid_pointer.c:164: Warning:
invalid pointer creation. assert \object_pointer((int *)100);
[eva] Recording results for object_pointer_predicate
[eva] Done for function object_pointer_predicate
[eva] Recording results for main
[eva] done for function main
[eva] tests/value/invalid_pointer.c:19:
assertion 'Eva,pointer_value' got final status invalid.
[eva] tests/value/invalid_pointer.c:22:
assertion 'Eva,pointer_value' got final status invalid.
[eva] tests/value/invalid_pointer.c:63:
assertion 'Eva,pointer_value' got final status invalid.
[eva] tests/value/invalid_pointer.c:69:
assertion 'Eva,pointer_value' got final status invalid.
[eva] tests/value/invalid_pointer.c:81:
assertion 'Eva,pointer_value' got final status invalid.
[eva] tests/value/invalid_pointer.c:83:
assertion 'Eva,pointer_value' got final status invalid.
[eva] tests/value/invalid_pointer.c:101:
assertion 'Eva,pointer_value' got final status invalid.
[eva] tests/value/invalid_pointer.c:117:
assertion 'Eva,pointer_value' got final status invalid.
[eva] tests/value/invalid_pointer.c:128:
assertion 'Eva,pointer_value' got final status invalid.
[eva] tests/value/invalid_pointer.c:134:
assertion 'Eva,pointer_value' got final status invalid.
[eva] tests/value/invalid_pointer.c:159:
assertion 'Eva,pointer_value' got final status invalid.
[eva] tests/value/invalid_pointer.c:164:
assertion 'Eva,pointer_value' got final status invalid.
[scope:rm_asserts] removing 2 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function addrof:
p ∈ {{ &a + [0..40],0%4 }}
offset ∈ [--..--]
[eva:final-states] Values at end of function int_conversion:
Frama_C_entropy_source ∈ [--..--]
x ∈ [15..31]
p ∈ [0..31]
[eva:final-states] Values at end of function object_pointer_predicate:
Frama_C_entropy_source ∈ [--..--]
p ∈ [0..31]
i ∈ [0..20]
[eva:final-states] Values at end of function pointer_computation:
Frama_C_entropy_source ∈ [--..--]
p ∈ {{ &x }}
i ∈ {-1; 0}
j ∈ {-1; 0; 1}
q ∈ {{ &x + {0; 4} ; &array + [0..100],0%4 }}
offset1 ∈ [0..10]
offset2 ∈ [0..25]
[eva:final-states] Values at end of function pointer_in_loops:
t[0] ∈ {0}
[1] ∈ {1}
[2] ∈ {2}
[3] ∈ {3}
[4] ∈ {4}
[5] ∈ {5}
[6] ∈ {6}
[7] ∈ {7}
[8] ∈ {8}
[9] ∈ {9}
[10] ∈ {10}
[11] ∈ {11}
[12] ∈ {12}
[13] ∈ {13}
[14] ∈ {14}
[15] ∈ {15}
[16] ∈ {16}
[17] ∈ {17}
[18] ∈ {18}
[19] ∈ {19}
[20] ∈ {20}
[21] ∈ {21}
[22] ∈ {22}
[23] ∈ {23}
[24] ∈ {24}
[25] ∈ {25}
[26] ∈ {26}
[27] ∈ {27}
[28] ∈ {28}
[29] ∈ {29}
[30] ∈ {30}
[31] ∈ {31}
[32] ∈ {32}
[33] ∈ {33}
[34] ∈ {34}
[35] ∈ {35}
[36] ∈ {36}
[37] ∈ {37}
[38] ∈ {38}
[39] ∈ {39}
[40] ∈ {40}
[41] ∈ {41}
[42] ∈ {42}
[43] ∈ {43}
[44] ∈ {44}
[45] ∈ {45}
[46] ∈ {46}
[47] ∈ {47}
[48] ∈ {48}
[49] ∈ {49}
[50] ∈ {50}
[51] ∈ {51}
[52] ∈ {52}
[53] ∈ {53}
[54] ∈ {54}
[55] ∈ {55}
[56] ∈ {56}
[57] ∈ {57}
[58] ∈ {58}
[59] ∈ {59}
[60] ∈ {60}
[61] ∈ {61}
[62] ∈ {62}
[63] ∈ {63}
[64] ∈ {64}
[65] ∈ {65}
[66] ∈ {66}
[67] ∈ {67}
[68] ∈ {68}
[69] ∈ {69}
[70] ∈ {70}
[71] ∈ {71}
[72] ∈ {72}
[73] ∈ {73}
[74] ∈ {74}
[75] ∈ {75}
[76] ∈ {76}
[77] ∈ {77}
[78] ∈ {78}
[79] ∈ {79}
[80] ∈ {80}
[81] ∈ {81}
[82] ∈ {82}
[83] ∈ {83}
[84] ∈ {84}
[85] ∈ {85}
[86] ∈ {86}
[87] ∈ {87}
[88] ∈ {88}
[89] ∈ {89}
[90] ∈ {90}
[91] ∈ {91}
[92] ∈ {92}
[93] ∈ {93}
[94] ∈ {94}
[95] ∈ {95}
[96] ∈ {96}
[97] ∈ {97}
[98] ∈ {98}
[99] ∈ {99}
[100] ∈ {100}
[101] ∈ {101}
[102] ∈ {102}
[103] ∈ {103}
[104] ∈ {104}
[105] ∈ {105}
[106] ∈ {106}
[107] ∈ {107}
[108] ∈ {108}
[109] ∈ {109}
[110] ∈ {110}
[111] ∈ {111}
[112] ∈ {112}
[113] ∈ {113}
[114] ∈ {114}
[115] ∈ {115}
[116] ∈ {116}
[117] ∈ {117}
[118] ∈ {118}
[119] ∈ {119}
[120] ∈ {120}
[121] ∈ {121}
[122] ∈ {122}
[123] ∈ {123}
[124] ∈ {124}
[125] ∈ {125}
[126] ∈ {126}
[127] ∈ {127}
p ∈ {{ &t[128] }}
[eva:final-states] Values at end of function union_pointer:
p ∈ [0..31]
u{.integer; .pointer} ∈ [0..31]
[eva:final-states] Values at end of function write_pointer:
p ∈ {42}
q ∈ {{ &x + {0; 1; 2; 3; 4} }}
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
[from] Computing for function addrof
[from] Done for function addrof
[from] Computing for function int_conversion
[from] Computing for function Frama_C_interval <-int_conversion
[from] Done for function Frama_C_interval
[from] Done for function int_conversion
[from] Computing for function object_pointer_predicate
[from] Done for function object_pointer_predicate
[from] Computing for function pointer_computation
[from] Done for function pointer_computation
[from] Computing for function pointer_in_loops
[from] Done for function pointer_in_loops
[from] Computing for function union_pointer
[from] Done for function union_pointer
[from] Computing for function write_pointer
[from] Done for function write_pointer
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function Frama_C_interval:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
\result FROM Frama_C_entropy_source; min; max
[from] Function addrof:
NO EFFECTS
[from] Function int_conversion:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function object_pointer_predicate:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function pointer_computation:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function pointer_in_loops:
NO EFFECTS
[from] Function union_pointer:
NO EFFECTS
[from] Function write_pointer:
NO EFFECTS
[from] Function main:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function addrof:
p; offset
[inout] Inputs for function addrof:
undet
[inout] Out (internal) for function int_conversion:
Frama_C_entropy_source; x; p
[inout] Inputs for function int_conversion:
Frama_C_entropy_source; undet
[inout] Out (internal) for function object_pointer_predicate:
Frama_C_entropy_source; p; i
[inout] Inputs for function object_pointer_predicate:
Frama_C_entropy_source; undet
[inout] Out (internal) for function pointer_computation:
Frama_C_entropy_source; p; i; j; q; tmp; offset1; offset2
[inout] Inputs for function pointer_computation:
Frama_C_entropy_source; undet
[inout] Out (internal) for function pointer_in_loops:
t[0..127]; p; i; q; i_0
[inout] Inputs for function pointer_in_loops:
undet
[inout] Out (internal) for function union_pointer:
p; u
[inout] Inputs for function union_pointer:
undet
[inout] Out (internal) for function write_pointer:
p; q
[inout] Inputs for function write_pointer:
undet
[inout] Out (internal) for function main:
Frama_C_entropy_source
[inout] Inputs for function main:
Frama_C_entropy_source; undet
[kernel] Parsing tests/value/invalid_pointer.c (with preprocessing)
[kernel:typing:int-conversion] tests/value/invalid_pointer.c:111: Warning:
Conversion from a pointer to an integer without an explicit cast
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
NULL[rbits 80 to 247] ∈ [--..--]
undet ∈ [--..--]
[eva] computing for function pointer_computation <- main.
Called from tests/value/invalid_pointer.c:171.
[eva] computing for function Frama_C_interval <- pointer_computation <- main.
Called from tests/value/invalid_pointer.c:30.
[eva] using specification for function Frama_C_interval
[eva] tests/value/invalid_pointer.c:30:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- pointer_computation <- main.
Called from tests/value/invalid_pointer.c:32.
[eva] tests/value/invalid_pointer.c:32:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] Recording results for pointer_computation
[eva] Done for function pointer_computation
[eva] computing for function pointer_in_loops <- main.
Called from tests/value/invalid_pointer.c:172.
[eva] tests/value/invalid_pointer.c:42:
Trace partitioning superposing up to 100 states
[eva] tests/value/invalid_pointer.c:53:
Frama_C_show_each_bottom: {{ &t + {-4} }}
[eva] Recording results for pointer_in_loops
[eva] Done for function pointer_in_loops
[eva] computing for function int_conversion <- main.
Called from tests/value/invalid_pointer.c:173.
[eva] computing for function Frama_C_interval <- int_conversion <- main.
Called from tests/value/invalid_pointer.c:65.
[eva] tests/value/invalid_pointer.c:65:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- int_conversion <- main.