Skip to content
Snippets Groups Projects
Commit a465676c authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[Instantiate] Ignore incomplete types in string functions

parent 6520856e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 141 additions and 30 deletions
src/plugins/instantiate/string/memcmp.ml
+ 2
− 1
View file @ a465676c
......@@ -97,7 +97,8 @@ let well_typed_call _ret = function
| [ s1 ; s2 ; len ] ->
(Cil.isIntegralType (Cil.typeOf len)) &&
(Cil_datatype.Typ.equal (type_from_arg s1) (type_from_arg s2)) &&
(not (Cil.isVoidType (type_from_arg s1)))
(not (Cil.isVoidType (type_from_arg s1))) &&
(Cil.isCompleteType (type_from_arg s1))
| _ -> false
let key_from_call _ret = function
......
src/plugins/instantiate/string/memcpy.ml
+ 2
− 1
View file @ a465676c
......@@ -103,7 +103,8 @@ let well_typed_call _ret = function
| [ dest ; src ; len ] ->
(Cil.isIntegralType (Cil.typeOf len)) &&
(Cil_datatype.Typ.equal (type_from_arg dest) (type_from_arg src)) &&
(not (Cil.isVoidType (type_from_arg dest)))
(not (Cil.isVoidType (type_from_arg dest))) &&
(Cil.isCompleteType (type_from_arg dest))
| _ -> false
let key_from_call _ret = function
......
src/plugins/instantiate/string/memmove.ml
+ 2
− 1
View file @ a465676c
......@@ -97,7 +97,8 @@ let well_typed_call _ret = function
| [ dest ; src ; len ] ->
(Cil.isIntegralType (Cil.typeOf len)) &&
(Cil_datatype.Typ.equal (type_from_arg dest) (type_from_arg src)) &&
(not (Cil.isVoidType (type_from_arg dest)))
(not (Cil.isVoidType (type_from_arg dest))) &&
(Cil.isCompleteType (type_from_arg dest))
| _ -> false
let key_from_call _ret = function
......
src/plugins/instantiate/string/memset.ml
+ 1
− 0
View file @ a465676c
......@@ -197,6 +197,7 @@ let well_typed_call _ret = function
| [ ptr ; _ ; _ ] when any_char_composed_type (type_from_arg ptr) -> true
| [ ptr ; _ ; _ ] when contains_union_type (type_from_arg ptr) -> false
| [ ptr ; _ ; _ ] when Cil.isVoidType (type_from_arg ptr) -> false
| [ ptr ; _ ; _ ] when not (Cil.isCompleteType (type_from_arg ptr)) -> false
| [ _ ; value ; _ ] ->
begin match memset_value value with
| None -> false
......
src/plugins/instantiate/tests/string/memcmp.c
+ 5
− 0
View file @ a465676c
......@@ -29,4 +29,9 @@ int nested(int (*s1)[10], int (*s2)[10], int n){
int with_void(void *s1, void *s2, int n){
return memcmp(s1, s2, 10) ;
}
struct incomplete ;
int with_incomplete(struct incomplete* s1, struct incomplete* s2, int n){
return memcmp(s1, s2, n);
}
\ No newline at end of file
src/plugins/instantiate/tests/string/memcpy.c
+ 6
− 0
View file @ a465676c
......@@ -36,3 +36,9 @@ void with_void(void *src, void *dest, int n){
void *res = memcpy(dest, src, n);
memcpy(src, res, n);
}
struct incomplete ;
void with_incomplete(struct incomplete* src, struct incomplete* dest, int n){
struct incomplete* res = memcpy(dest, src, n);
memcpy(src, res, n);
}
\ No newline at end of file
src/plugins/instantiate/tests/string/memmove.c
+ 6
− 0
View file @ a465676c
......@@ -36,3 +36,9 @@ void with_void(void *src, void *dest, int n){
void *res = memmove(dest, src, n);
memmove(src, res, n);
}
struct incomplete ;
void with_incomplete(struct incomplete *src, struct incomplete *dest, int n){
struct incomplete *res = memmove(dest, src, n);
memmove(src, res, n);
}
src/plugins/instantiate/tests/string/memset_value.c
+ 5
− 0
View file @ a465676c
......@@ -51,3 +51,8 @@ void with_void(void* dest, int value){
void* res = memset(dest, value, 10);
memset(res, value, 10);
}
void with_incomplete(struct incomplete* dest, int value){
struct incomplete * res = memset(dest, value, 10);
memset(res, value, 10);
}
\ No newline at end of file
src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
+ 25
− 6
View file @ a465676c
[kernel] Parsing tests/string/memcmp.c (with preprocessing)
[instantiate] tests/string/memcmp.c:31: Warning: Ignore call: not well typed
[instantiate] tests/string/memcmp.c:36: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
......@@ -9,6 +10,7 @@ struct X {
int y ;
};
typedef int named;
struct incomplete;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_read_s1:
......@@ -150,21 +152,30 @@ int with_void(void *s1, void *s2, int n)
return tmp;
}
int with_incomplete(struct incomplete *s1, struct incomplete *s2, int n)
{
int tmp;
tmp = memcmp((void const *)s1,(void const *)s2,(unsigned int)n);
return tmp;
}
[kernel] Parsing tests/string/result/memcmp.c (with preprocessing)
[kernel] Parsing tests/string/memcmp.c (with preprocessing)
[kernel] tests/string/memcmp.c:10: Warning:
def'n of func integer at tests/string/memcmp.c:10 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:34 (sum 1972); keeping the one at tests/string/result/memcmp.c:34.
def'n of func integer at tests/string/memcmp.c:10 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:35 (sum 1972); keeping the one at tests/string/result/memcmp.c:35.
[kernel] tests/string/memcmp.c:14: Warning:
def'n of func with_named at tests/string/memcmp.c:14 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:41 (sum 1972); keeping the one at tests/string/result/memcmp.c:41.
def'n of func with_named at tests/string/memcmp.c:14 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:42 (sum 1972); keeping the one at tests/string/result/memcmp.c:42.
[kernel] tests/string/memcmp.c:18: Warning:
def'n of func structure at tests/string/memcmp.c:18 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:72 (sum 1972); keeping the one at tests/string/result/memcmp.c:72.
def'n of func structure at tests/string/memcmp.c:18 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:73 (sum 1972); keeping the one at tests/string/result/memcmp.c:73.
[kernel] tests/string/memcmp.c:22: Warning:
def'n of func pointers at tests/string/memcmp.c:22 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:103 (sum 1972); keeping the one at tests/string/result/memcmp.c:103.
def'n of func pointers at tests/string/memcmp.c:22 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:104 (sum 1972); keeping the one at tests/string/result/memcmp.c:104.
[kernel] tests/string/memcmp.c:26: Warning:
def'n of func nested at tests/string/memcmp.c:26 (sum 1087) conflicts with the one at tests/string/result/memcmp.c:137 (sum 1974); keeping the one at tests/string/result/memcmp.c:137.
def'n of func nested at tests/string/memcmp.c:26 (sum 1087) conflicts with the one at tests/string/result/memcmp.c:138 (sum 1974); keeping the one at tests/string/result/memcmp.c:138.
[kernel] tests/string/memcmp.c:30: Warning:
def'n of func with_void at tests/string/memcmp.c:30 (sum 1087) conflicts with the one at tests/string/result/memcmp.c:144 (sum 1974); keeping the one at tests/string/result/memcmp.c:144.
def'n of func with_void at tests/string/memcmp.c:30 (sum 1087) conflicts with the one at tests/string/result/memcmp.c:145 (sum 1974); keeping the one at tests/string/result/memcmp.c:145.
[kernel] tests/string/memcmp.c:35: Warning:
def'n of func with_incomplete at tests/string/memcmp.c:35 (sum 1087) conflicts with the one at tests/string/result/memcmp.c:152 (sum 1974); keeping the one at tests/string/result/memcmp.c:152.
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
......@@ -174,6 +185,7 @@ struct X {
int y ;
};
typedef int named;
struct incomplete;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_read_s1:
......@@ -324,4 +336,11 @@ int with_void(void *s1, void *s2, int n)
return tmp;
}
int with_incomplete(struct incomplete *s1, struct incomplete *s2, int n)
{
int tmp;
tmp = memcmp((void const *)s1,(void const *)s2,(unsigned int)n);
return tmp;
}
src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
+ 28
− 6
View file @ a465676c
[kernel] Parsing tests/string/memcpy.c (with preprocessing)
[instantiate] tests/string/memcpy.c:36: Warning: Ignore call: not well typed
[instantiate] tests/string/memcpy.c:37: Warning: Ignore call: not well typed
[instantiate] tests/string/memcpy.c:42: Warning: Ignore call: not well typed
[instantiate] tests/string/memcpy.c:43: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
......@@ -10,6 +12,7 @@ struct X {
int y ;
};
typedef int named;
struct incomplete;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
......@@ -162,21 +165,31 @@ void with_void(void *src, void *dest, int n)
return;
}
void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
{
struct incomplete *res =
memcpy((void *)dest,(void const *)src,(unsigned int)n);
memcpy((void *)src,(void const *)res,(unsigned int)n);
return;
}
[kernel] Parsing tests/string/result/memcpy.c (with preprocessing)
[kernel] Parsing tests/string/memcpy.c (with preprocessing)
[kernel] tests/string/memcpy.c:10: Warning:
dropping duplicate def'n of func integer at tests/string/memcpy.c:10 in favor of that at tests/string/result/memcpy.c:36
dropping duplicate def'n of func integer at tests/string/memcpy.c:10 in favor of that at tests/string/result/memcpy.c:37
[kernel] tests/string/memcpy.c:15: Warning:
dropping duplicate def'n of func with_named at tests/string/memcpy.c:15 in favor of that at tests/string/result/memcpy.c:43
dropping duplicate def'n of func with_named at tests/string/memcpy.c:15 in favor of that at tests/string/result/memcpy.c:44
[kernel] tests/string/memcpy.c:20: Warning:
dropping duplicate def'n of func structure at tests/string/memcpy.c:20 in favor of that at tests/string/result/memcpy.c:76
dropping duplicate def'n of func structure at tests/string/memcpy.c:20 in favor of that at tests/string/result/memcpy.c:77
[kernel] tests/string/memcpy.c:25: Warning:
dropping duplicate def'n of func pointers at tests/string/memcpy.c:25 in favor of that at tests/string/result/memcpy.c:109
dropping duplicate def'n of func pointers at tests/string/memcpy.c:25 in favor of that at tests/string/result/memcpy.c:110
[kernel] tests/string/memcpy.c:30: Warning:
dropping duplicate def'n of func nested at tests/string/memcpy.c:30 in favor of that at tests/string/result/memcpy.c:147
dropping duplicate def'n of func nested at tests/string/memcpy.c:30 in favor of that at tests/string/result/memcpy.c:148
[kernel] tests/string/memcpy.c:35: Warning:
dropping duplicate def'n of func with_void at tests/string/memcpy.c:35 in favor of that at tests/string/result/memcpy.c:155
dropping duplicate def'n of func with_void at tests/string/memcpy.c:35 in favor of that at tests/string/result/memcpy.c:156
[kernel] tests/string/memcpy.c:41: Warning:
dropping duplicate def'n of func with_incomplete at tests/string/memcpy.c:41 in favor of that at tests/string/result/memcpy.c:163
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
......@@ -186,6 +199,7 @@ struct X {
int y ;
};
typedef int named;
struct incomplete;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
......@@ -349,4 +363,12 @@ void with_void(void *src, void *dest, int n)
return;
}
void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
{
struct incomplete *res =
memcpy((void *)dest,(void const *)src,(unsigned int)n);
memcpy((void *)src,(void const *)res,(unsigned int)n);
return;
}
src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
+ 28
− 6
View file @ a465676c
[kernel] Parsing tests/string/memmove.c (with preprocessing)
[instantiate] tests/string/memmove.c:36: Warning: Ignore call: not well typed
[instantiate] tests/string/memmove.c:37: Warning: Ignore call: not well typed
[instantiate] tests/string/memmove.c:42: Warning: Ignore call: not well typed
[instantiate] tests/string/memmove.c:43: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
......@@ -10,6 +12,7 @@ struct X {
int y ;
};
typedef int named;
struct incomplete;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
......@@ -146,21 +149,31 @@ void with_void(void *src, void *dest, int n)
return;
}
void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
{
struct incomplete *res =
memmove((void *)dest,(void const *)src,(unsigned int)n);
memmove((void *)src,(void const *)res,(unsigned int)n);
return;
}
[kernel] Parsing tests/string/result/memmove.c (with preprocessing)
[kernel] Parsing tests/string/memmove.c (with preprocessing)
[kernel] tests/string/memmove.c:10: Warning:
dropping duplicate def'n of func integer at tests/string/memmove.c:10 in favor of that at tests/string/result/memmove.c:32
dropping duplicate def'n of func integer at tests/string/memmove.c:10 in favor of that at tests/string/result/memmove.c:33
[kernel] tests/string/memmove.c:15: Warning:
dropping duplicate def'n of func with_named at tests/string/memmove.c:15 in favor of that at tests/string/result/memmove.c:39
dropping duplicate def'n of func with_named at tests/string/memmove.c:15 in favor of that at tests/string/result/memmove.c:40
[kernel] tests/string/memmove.c:20: Warning:
dropping duplicate def'n of func structure at tests/string/memmove.c:20 in favor of that at tests/string/result/memmove.c:68
dropping duplicate def'n of func structure at tests/string/memmove.c:20 in favor of that at tests/string/result/memmove.c:69
[kernel] tests/string/memmove.c:25: Warning:
dropping duplicate def'n of func pointers at tests/string/memmove.c:25 in favor of that at tests/string/result/memmove.c:97
dropping duplicate def'n of func pointers at tests/string/memmove.c:25 in favor of that at tests/string/result/memmove.c:98
[kernel] tests/string/memmove.c:30: Warning:
dropping duplicate def'n of func nested at tests/string/memmove.c:30 in favor of that at tests/string/result/memmove.c:131
dropping duplicate def'n of func nested at tests/string/memmove.c:30 in favor of that at tests/string/result/memmove.c:132
[kernel] tests/string/memmove.c:35: Warning:
dropping duplicate def'n of func with_void at tests/string/memmove.c:35 in favor of that at tests/string/result/memmove.c:139
dropping duplicate def'n of func with_void at tests/string/memmove.c:35 in favor of that at tests/string/result/memmove.c:140
[kernel] tests/string/memmove.c:41: Warning:
dropping duplicate def'n of func with_incomplete at tests/string/memmove.c:41 in favor of that at tests/string/result/memmove.c:147
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
......@@ -170,6 +183,7 @@ struct X {
int y ;
};
typedef int named;
struct incomplete;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
......@@ -317,4 +331,12 @@ void with_void(void *src, void *dest, int n)
return;
}
void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
{
struct incomplete *res =
memmove((void *)dest,(void const *)src,(unsigned int)n);
memmove((void *)src,(void const *)res,(unsigned int)n);
return;
}
src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
+ 31
− 9
View file @ a465676c
......@@ -23,6 +23,10 @@
Ignore call: not well typed
[instantiate] tests/string/memset_value.c:52: Warning:
Ignore call: not well typed
[instantiate] tests/string/memset_value.c:56: Warning:
Ignore call: not well typed
[instantiate] tests/string/memset_value.c:57: Warning:
Ignore call: not well typed
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
......@@ -32,6 +36,7 @@ struct X {
int y ;
};
typedef int named;
struct incomplete;
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
......@@ -151,27 +156,36 @@ void with_void(void *dest, int value)
return;
}
void with_incomplete(struct incomplete *dest, int value)
{
struct incomplete *res = memset((void *)dest,value,(unsigned int)10);
memset((void *)res,value,(unsigned int)10);
return;
}
[kernel] Parsing tests/string/result/memset_value.c (with preprocessing)
[kernel] Parsing tests/string/memset_value.c (with preprocessing)
[kernel] tests/string/memset_value.c:10: Warning:
dropping duplicate def'n of func chars at tests/string/memset_value.c:10 in favor of that at tests/string/result/memset_value.c:26
dropping duplicate def'n of func chars at tests/string/memset_value.c:10 in favor of that at tests/string/result/memset_value.c:27
[kernel] tests/string/memset_value.c:15: Warning:
dropping duplicate def'n of func uchars at tests/string/memset_value.c:15 in favor of that at tests/string/result/memset_value.c:50
dropping duplicate def'n of func uchars at tests/string/memset_value.c:15 in favor of that at tests/string/result/memset_value.c:51
[kernel] tests/string/memset_value.c:20: Warning:
dropping duplicate def'n of func nested_chars at tests/string/memset_value.c:20 in favor of that at tests/string/result/memset_value.c:78
dropping duplicate def'n of func nested_chars at tests/string/memset_value.c:20 in favor of that at tests/string/result/memset_value.c:79
[kernel] tests/string/memset_value.c:25: Warning:
dropping duplicate def'n of func integer at tests/string/memset_value.c:25 in favor of that at tests/string/result/memset_value.c:85
dropping duplicate def'n of func integer at tests/string/memset_value.c:25 in favor of that at tests/string/result/memset_value.c:86
[kernel] tests/string/memset_value.c:30: Warning:
dropping duplicate def'n of func with_named at tests/string/memset_value.c:30 in favor of that at tests/string/result/memset_value.c:92
dropping duplicate def'n of func with_named at tests/string/memset_value.c:30 in favor of that at tests/string/result/memset_value.c:93
[kernel] tests/string/memset_value.c:35: Warning:
dropping duplicate def'n of func structure at tests/string/memset_value.c:35 in favor of that at tests/string/result/memset_value.c:99
dropping duplicate def'n of func structure at tests/string/memset_value.c:35 in favor of that at tests/string/result/memset_value.c:100
[kernel] tests/string/memset_value.c:40: Warning:
dropping duplicate def'n of func pointers at tests/string/memset_value.c:40 in favor of that at tests/string/result/memset_value.c:107
dropping duplicate def'n of func pointers at tests/string/memset_value.c:40 in favor of that at tests/string/result/memset_value.c:108
[kernel] tests/string/memset_value.c:45: Warning:
dropping duplicate def'n of func nested at tests/string/memset_value.c:45 in favor of that at tests/string/result/memset_value.c:114
dropping duplicate def'n of func nested at tests/string/memset_value.c:45 in favor of that at tests/string/result/memset_value.c:115
[kernel] tests/string/memset_value.c:50: Warning:
dropping duplicate def'n of func with_void at tests/string/memset_value.c:50 in favor of that at tests/string/result/memset_value.c:122
dropping duplicate def'n of func with_void at tests/string/memset_value.c:50 in favor of that at tests/string/result/memset_value.c:123
[kernel] tests/string/memset_value.c:55: Warning:
dropping duplicate def'n of func with_incomplete at tests/string/memset_value.c:55 in favor of that at tests/string/result/memset_value.c:130
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
......@@ -181,6 +195,7 @@ struct X {
int y ;
};
typedef int named;
struct incomplete;
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
......@@ -305,4 +320,11 @@ void with_void(void *dest, int value)
return;
}
void with_incomplete(struct incomplete *dest, int value)
{
struct incomplete *res = memset((void *)dest,value,(unsigned int)10);
memset((void *)res,value,(unsigned int)10);
return;
}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment