diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 26b929d31b..7c957b72df 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -801,43 +801,48 @@ struct let b = Mem e, NoOffset in (* base pointer *) let t = Cilfacade.typeOfLval b in (* static type of base *) let p = eval_lv a gs st b in (* abstract base addresses *) - let v = (* abstract base value *) + (* pre VLA: *) + (* let cast_ok = function Addr a -> sizeOf t <= sizeOf (get_type_addr a) | _ -> false in *) + let cast_ok a = let open Addr in - (* pre VLA: *) - (* let cast_ok = function Addr a -> sizeOf t <= sizeOf (get_type_addr a) | _ -> false in *) - let cast_ok = function - | Addr (x, o) -> - begin - let at = get_type_addr (x, o) in - if M.tracing then M.tracel "evalint" "cast_ok %a %a %a\n" Addr.pretty (Addr (x, o)) CilType.Typ.pretty (Cil.unrollType x.vtype) CilType.Typ.pretty at; - if at = TVoid [] then (* HACK: cast from alloc variable is always fine *) - true - else - match Cil.getInteger (sizeOf t), Cil.getInteger (sizeOf at) with - | Some i1, Some i2 -> Cilint.compare_cilint i1 i2 <= 0 - | _ -> - if contains_vla t || contains_vla (get_type_addr (x, o)) then - begin - (* TODO: Is this ok? *) - M.info ~category:Unsound "Casting involving a VLA is assumed to work"; - true - end - else - false - end - | NullPtr | UnknownPtr -> true (* TODO: are these sound? *) - | _ -> false + match a with + | Addr (x, o) -> + begin + let at = get_type_addr (x, o) in + if M.tracing then M.tracel "evalint" "cast_ok %a %a %a\n" Addr.pretty (Addr (x, o)) CilType.Typ.pretty (Cil.unrollType x.vtype) CilType.Typ.pretty at; + if at = TVoid [] then (* HACK: cast from alloc variable is always fine *) + true + else + match Cil.getInteger (sizeOf t), Cil.getInteger (sizeOf at) with + | Some i1, Some i2 -> Cilint.compare_cilint i1 i2 <= 0 + | _ -> + if contains_vla t || contains_vla (get_type_addr (x, o)) then + begin + (* TODO: Is this ok? *) + M.info ~category:Unsound "Casting involving a VLA is assumed to work"; + true + end + else + false + end + | NullPtr | UnknownPtr -> true (* TODO: are these sound? *) + | _ -> false + in + (** Lookup value at base address [addr] with given offset [ofs]. *) + let lookup_with_offs addr = + let v = (* abstract base value *) + if cast_ok addr then + get ~top:(VD.top_value t) a gs st (AD.singleton addr) (Some exp) (* downcasts are safe *) + else + VD.top () (* upcasts not! *) in - if AD.for_all cast_ok p then - get ~top:(VD.top_value t) a gs st p (Some exp) (* downcasts are safe *) - else - VD.top () (* upcasts not! *) + let v' = VD.cast t v in (* cast to the expected type (the abstract type might be something other than t since we don't change addresses upon casts!) *) + if M.tracing then M.tracel "cast" "Ptr-Deref: cast %a to %a = %a!\n" VD.pretty v d_type t VD.pretty v'; + let v' = VD.eval_offset a (fun x -> get a gs st x (Some exp)) v' (convert_offset a gs st ofs) (Some exp) None t in (* handle offset *) + let v' = do_offs v' ofs in (* handle blessed fields? *) + v' in - let v' = VD.cast t v in (* cast to the expected type (the abstract type might be something other than t since we don't change addresses upon casts!) *) - if M.tracing then M.tracel "cast" "Ptr-Deref: cast %a to %a = %a!\n" VD.pretty v d_type t VD.pretty v'; - let v' = VD.eval_offset a (fun x -> get a gs st x (Some exp)) v' (convert_offset a gs st ofs) (Some exp) None t in (* handle offset *) - let v' = do_offs v' ofs in (* handle blessed fields? *) - v' + AD.fold (fun a acc -> VD.join acc (lookup_with_offs a)) p (VD.bot ()) (* Binary operators *) (* Eq/Ne when both values are equal and casted to the same type *) | BinOp (op, (CastE (t1, e1) as c1), (CastE (t2, e2) as c2), typ) when typeSig t1 = typeSig t2 && (op = Eq || op = Ne) -> diff --git a/src/cdomains/structDomain.ml b/src/cdomains/structDomain.ml index a9c390bad5..33fb313f08 100644 --- a/src/cdomains/structDomain.ml +++ b/src/cdomains/structDomain.ml @@ -12,6 +12,7 @@ sig include Lattice.S val is_bot_value: t -> bool val is_top_value: t -> typ -> bool + val top_value: ?varAttr:attributes -> typ -> t end module type S = @@ -49,7 +50,11 @@ struct let pretty () = M.pretty () let replace s field value = M.add field value s - let get s field = M.find field s + let get s field = + match M.find_opt field s with + | Some v -> v + | None -> Val.top_value field.ftype + let fold = M.fold let map = M.map let keys x = M.fold (fun k _ a -> k::a) x [] diff --git a/src/cdomains/structDomain.mli b/src/cdomains/structDomain.mli index d33d632970..d83d807096 100644 --- a/src/cdomains/structDomain.mli +++ b/src/cdomains/structDomain.mli @@ -7,6 +7,7 @@ sig include Lattice.S val is_bot_value: t -> bool val is_top_value: t -> typ -> bool + val top_value: ?varAttr:attributes -> typ -> t end module type S = diff --git a/tests/regression/43-struct-domain/27-chrony-nameserv-sched-array.c b/tests/regression/43-struct-domain/27-chrony-nameserv-sched-array.c new file mode 100644 index 0000000000..a0b8b2a4e3 --- /dev/null +++ b/tests/regression/43-struct-domain/27-chrony-nameserv-sched-array.c @@ -0,0 +1,233 @@ +// PARAM: --set ana.malloc.wrappers '["Malloc", "Realloc", "Malloc2", "Realloc2", "ARR_CreateInstance", "realloc_array", "ARR_GetNewElement"]' --disable sem.unknown_function.spawn --disable sem.unknown_function.invalidate.globals +// extracted from chrony +#include +#include +#include + +// memory.c + +void * +Malloc(size_t size) +{ + void *r; + + r = malloc(size); + + return r; +} + +void * +Realloc(void *ptr, size_t size) +{ + void *r; + + r = realloc(ptr, size); + + return r; +} + +static size_t +get_array_size(size_t nmemb, size_t size) +{ + size_t array_size; + + array_size = nmemb * size; + + return array_size; +} + +void * +Realloc2(void *ptr, size_t nmemb, size_t size) +{ + return Realloc(ptr, get_array_size(nmemb, size)); +} + +#define MallocNew(T) ((T *) Malloc(sizeof(T))) +#define MallocArray(T, n) ((T *) Malloc2(n, sizeof(T))) +#define ReallocArray(T, n, x) ((T *) Realloc2((void *)(x), n, sizeof(T))) +#define Free(x) free(x) + +// array.c + +struct ARR_Instance_Record { + void *data; + unsigned int elem_size; + unsigned int used; + unsigned int allocated; +}; + +typedef struct ARR_Instance_Record *ARR_Instance; + +ARR_Instance +ARR_CreateInstance(unsigned int elem_size) +{ + ARR_Instance array; + + assert(elem_size > 0); + + array = MallocNew(struct ARR_Instance_Record); + + array->data = NULL; + array->elem_size = elem_size; + array->used = 0; + array->allocated = 0; + + return array; +} + +void * +ARR_GetElement(ARR_Instance array, unsigned int index) +{ + assert(index < array->used); // UNKNOWN + return (void *)((char *)array->data + (size_t)index * array->elem_size); +} + +static void +realloc_array(ARR_Instance array, unsigned int min_size) +{ + assert(min_size <= 2 * min_size); // UNKNOWN + if (array->allocated >= min_size && array->allocated <= 2 * min_size) + return; + + if (array->allocated < min_size) { + while (array->allocated < min_size) + array->allocated = array->allocated ? 2 * array->allocated : 1; + } else { + array->allocated = min_size; + } + + array->data = Realloc2(array->data, array->allocated, array->elem_size); +} + +void * +ARR_GetNewElement(ARR_Instance array) +{ + array->used++; + realloc_array(array, array->used); + return ARR_GetElement(array, array->used - 1); +} + +unsigned int +ARR_GetSize(ARR_Instance array) +{ + return array->used; +} + +// sched.c + +typedef void* SCH_ArbitraryArgument; +typedef void (*SCH_FileHandler)(SCH_ArbitraryArgument); + +typedef struct { + SCH_FileHandler handler; + SCH_ArbitraryArgument arg; +} FileHandlerEntry; + +static ARR_Instance file_handlers; + +void +SCH_Initialise(void) +{ + file_handlers = ARR_CreateInstance(sizeof (FileHandlerEntry)); +} + +void +SCH_AddFileHandler +(SCH_FileHandler handler, SCH_ArbitraryArgument arg) +{ + int fd; // rand + FileHandlerEntry *ptr; + + while (ARR_GetSize(file_handlers) <= fd) { + ptr = ARR_GetNewElement(file_handlers); + ptr->handler = NULL; + ptr->arg = NULL; + } + + ptr = ARR_GetElement(file_handlers, fd); + + /* Don't want to allow the same fd to register a handler more than + once without deleting a previous association - this suggests + a bug somewhere else in the program. */ + assert(!ptr->handler); // UNKNOWN + + ptr->handler = handler; + ptr->arg = arg; +} + +static void +dispatch_filehandlers() +{ + FileHandlerEntry *ptr; + int fd; // rand + + ptr = (FileHandlerEntry *)ARR_GetElement(file_handlers, fd); + SCH_FileHandler stuff = *(ptr->handler); + if (ptr->handler) + (ptr->handler)(ptr->arg); +} + +// nameserv_async.c + +typedef void (*DNS_NameResolveHandler)(void *anything); + +struct DNS_Async_Instance { + DNS_NameResolveHandler handler; + void *arg; + pthread_t thread; +}; + +static void * +start_resolving(void *anything) +{ + struct DNS_Async_Instance *inst = (struct DNS_Async_Instance *)anything; + + return NULL; +} + +static void +end_resolving(void *anything) +{ + struct DNS_Async_Instance *inst = (struct DNS_Async_Instance *)anything; + + DNS_NameResolveHandler h = inst->handler; + (inst->handler)(inst->arg); + + Free(inst); +} + +void +DNS_Name2IPAddressAsync(DNS_NameResolveHandler handler, void *anything) +{ + struct DNS_Async_Instance *inst; + + inst = MallocNew(struct DNS_Async_Instance); + inst->handler = handler; + inst->arg = anything; + + pthread_create(&inst->thread, NULL, start_resolving, inst); + + SCH_AddFileHandler(end_resolving, inst); +} + +// stub + +void foo(void *arg) { + assert(1); // reachable +} + +void bar(void *arg) { + int *p = arg; + int y = *p; + assert(1); // reachable + assert(y); // TODO +} + +int main() { + SCH_Initialise(); + DNS_Name2IPAddressAsync(foo, NULL); + int x = 1; + DNS_Name2IPAddressAsync(bar, &x); + dispatch_filehandlers(); + return 0; +} \ No newline at end of file diff --git a/tests/regression/43-struct-domain/28-chrony-nameserv-sched-array2.c b/tests/regression/43-struct-domain/28-chrony-nameserv-sched-array2.c new file mode 100644 index 0000000000..0394e9ca62 --- /dev/null +++ b/tests/regression/43-struct-domain/28-chrony-nameserv-sched-array2.c @@ -0,0 +1,276 @@ +// PARAM: --set ana.malloc.wrappers '["Malloc", "Realloc", "Malloc2", "Realloc2", "ARR_CreateInstance", "realloc_array", "ARR_GetNewElement"]' --disable sem.unknown_function.spawn --disable sem.unknown_function.invalidate.globals +// extracted from chrony +#include +#include +#include + +// memory.c + +void * +Malloc(size_t size) +{ + void *r; + + r = malloc(size); + + return r; +} + +void * +Realloc(void *ptr, size_t size) +{ + void *r; + + r = realloc(ptr, size); + + return r; +} + +static size_t +get_array_size(size_t nmemb, size_t size) +{ + size_t array_size; + + array_size = nmemb * size; + + return array_size; +} + +void * +Realloc2(void *ptr, size_t nmemb, size_t size) +{ + return Realloc(ptr, get_array_size(nmemb, size)); +} + +#define MallocNew(T) ((T *) Malloc(sizeof(T))) +#define MallocArray(T, n) ((T *) Malloc2(n, sizeof(T))) +#define ReallocArray(T, n, x) ((T *) Realloc2((void *)(x), n, sizeof(T))) +#define Free(x) free(x) + +// array.c + +struct ARR_Instance_Record { + void *data; + unsigned int elem_size; + unsigned int used; + unsigned int allocated; +}; + +typedef struct ARR_Instance_Record *ARR_Instance; + +ARR_Instance +ARR_CreateInstance(unsigned int elem_size) +{ + ARR_Instance array; + + assert(elem_size > 0); + + array = MallocNew(struct ARR_Instance_Record); + + array->data = NULL; + array->elem_size = elem_size; + array->used = 0; + array->allocated = 0; + + return array; +} + +void * +ARR_GetElement(ARR_Instance array, unsigned int index) +{ + assert(index < array->used); // UNKNOWN + return (void *)((char *)array->data + (size_t)index * array->elem_size); +} + +static void +realloc_array(ARR_Instance array, unsigned int min_size) +{ + assert(min_size <= 2 * min_size); // UNKNOWN + if (array->allocated >= min_size && array->allocated <= 2 * min_size) + return; + + if (array->allocated < min_size) { + while (array->allocated < min_size) + array->allocated = array->allocated ? 2 * array->allocated : 1; + } else { + array->allocated = min_size; + } + + array->data = Realloc2(array->data, array->allocated, array->elem_size); +} + +void * +ARR_GetNewElement(ARR_Instance array) +{ + array->used++; + realloc_array(array, array->used); + return ARR_GetElement(array, array->used - 1); +} + +unsigned int +ARR_GetSize(ARR_Instance array) +{ + return array->used; +} + +// sched.c + +typedef void* SCH_ArbitraryArgument; +typedef void (*SCH_FileHandler)(SCH_ArbitraryArgument); + +typedef struct { + SCH_FileHandler handler; + SCH_ArbitraryArgument arg; +} FileHandlerEntry; + +static ARR_Instance file_handlers; + +void +SCH_Initialise(void) +{ + file_handlers = ARR_CreateInstance(sizeof (FileHandlerEntry)); +} + +void +SCH_AddFileHandler +(SCH_FileHandler handler, SCH_ArbitraryArgument arg) +{ + int fd; // rand + FileHandlerEntry *ptr; + + while (ARR_GetSize(file_handlers) <= fd) { + ptr = ARR_GetNewElement(file_handlers); + ptr->handler = NULL; + ptr->arg = NULL; + } + + ptr = ARR_GetElement(file_handlers, fd); + + /* Don't want to allow the same fd to register a handler more than + once without deleting a previous association - this suggests + a bug somewhere else in the program. */ + assert(!ptr->handler); // UNKNOWN + + ptr->handler = handler; + ptr->arg = arg; +} + +static void +dispatch_filehandlers() +{ + FileHandlerEntry *ptr; + int fd; // rand + + ptr = (FileHandlerEntry *)ARR_GetElement(file_handlers, fd); + SCH_FileHandler stuff = *(ptr->handler); + if (ptr->handler) + (ptr->handler)(ptr->arg); +} + +// nameserv_async.c + +typedef void (*DNS_NameResolveHandler)(void *anything); + +struct DNS_Async_Instance { + DNS_NameResolveHandler handler; + void *arg; + pthread_t thread; +}; + +static void * +start_resolving(void *anything) +{ + struct DNS_Async_Instance *inst = (struct DNS_Async_Instance *)anything; + + return NULL; +} + +static void +end_resolving(void *anything) +{ + struct DNS_Async_Instance *inst = (struct DNS_Async_Instance *)anything; + + DNS_NameResolveHandler h = inst->handler; + (inst->handler)(inst->arg); + + Free(inst); +} + +void +DNS_Name2IPAddressAsync(DNS_NameResolveHandler handler, void *anything) +{ + struct DNS_Async_Instance *inst; + + inst = MallocNew(struct DNS_Async_Instance); + inst->handler = handler; + inst->arg = anything; + + pthread_create(&inst->thread, NULL, start_resolving, inst); + + SCH_AddFileHandler(end_resolving, inst); +} + +// nameserv_async.c copy + +typedef void (*DNS_NameResolveHandler2)(void *anything2); + +struct DNS_Async_Instance2 { + DNS_NameResolveHandler2 handler2; + void *arg2; + pthread_t thread2; +}; + +static void * +start_resolving2(void *anything2) +{ + struct DNS_Async_Instance2 *inst2 = (struct DNS_Async_Instance2 *)anything2; + + return NULL; +} + +static void +end_resolving2(void *anything2) +{ + struct DNS_Async_Instance2 *inst2 = (struct DNS_Async_Instance2 *)anything2; + + DNS_NameResolveHandler2 h = inst2->handler2; + (inst2->handler2)(inst2->arg2); + + Free(inst2); +} + +void +DNS_Name2IPAddressAsync2(DNS_NameResolveHandler2 handler2, void *anything2) +{ + struct DNS_Async_Instance2 *inst2; + + inst2 = MallocNew(struct DNS_Async_Instance2); + inst2->handler2 = handler2; + inst2->arg2 = anything2; + + pthread_create(&inst2->thread2, NULL, start_resolving2, inst2); + + SCH_AddFileHandler(end_resolving2, inst2); +} + +// stub + +void foo(void *arg) { + assert(1); // reachable +} + +void bar(void *arg) { + int *p = arg; + int y = *p; + assert(1); // reachable + assert(y); // TODO +} + +int main() { + SCH_Initialise(); + DNS_Name2IPAddressAsync(foo, NULL); + int x = 1; + DNS_Name2IPAddressAsync2(bar, &x); + dispatch_filehandlers(); + return 0; +} \ No newline at end of file diff --git a/tests/regression/43-struct-domain/29-chrony-nameserv-sched-array2-set-struct.c b/tests/regression/43-struct-domain/29-chrony-nameserv-sched-array2-set-struct.c new file mode 100644 index 0000000000..72c9072e51 --- /dev/null +++ b/tests/regression/43-struct-domain/29-chrony-nameserv-sched-array2-set-struct.c @@ -0,0 +1,276 @@ +// PARAM: --set ana.malloc.wrappers '["Malloc", "Realloc", "Malloc2", "Realloc2", "ARR_CreateInstance", "realloc_array", "ARR_GetNewElement"]' --set ana.base.structs.domain sets --disable sem.unknown_function.spawn --disable sem.unknown_function.invalidate.globals +// extracted from chrony +#include +#include +#include + +// memory.c + +void * +Malloc(size_t size) +{ + void *r; + + r = malloc(size); + + return r; +} + +void * +Realloc(void *ptr, size_t size) +{ + void *r; + + r = realloc(ptr, size); + + return r; +} + +static size_t +get_array_size(size_t nmemb, size_t size) +{ + size_t array_size; + + array_size = nmemb * size; + + return array_size; +} + +void * +Realloc2(void *ptr, size_t nmemb, size_t size) +{ + return Realloc(ptr, get_array_size(nmemb, size)); +} + +#define MallocNew(T) ((T *) Malloc(sizeof(T))) +#define MallocArray(T, n) ((T *) Malloc2(n, sizeof(T))) +#define ReallocArray(T, n, x) ((T *) Realloc2((void *)(x), n, sizeof(T))) +#define Free(x) free(x) + +// array.c + +struct ARR_Instance_Record { + void *data; + unsigned int elem_size; + unsigned int used; + unsigned int allocated; +}; + +typedef struct ARR_Instance_Record *ARR_Instance; + +ARR_Instance +ARR_CreateInstance(unsigned int elem_size) +{ + ARR_Instance array; + + assert(elem_size > 0); + + array = MallocNew(struct ARR_Instance_Record); + + array->data = NULL; + array->elem_size = elem_size; + array->used = 0; + array->allocated = 0; + + return array; +} + +void * +ARR_GetElement(ARR_Instance array, unsigned int index) +{ + assert(index < array->used); // UNKNOWN + return (void *)((char *)array->data + (size_t)index * array->elem_size); +} + +static void +realloc_array(ARR_Instance array, unsigned int min_size) +{ + assert(min_size <= 2 * min_size); // UNKNOWN + if (array->allocated >= min_size && array->allocated <= 2 * min_size) + return; + + if (array->allocated < min_size) { + while (array->allocated < min_size) + array->allocated = array->allocated ? 2 * array->allocated : 1; + } else { + array->allocated = min_size; + } + + array->data = Realloc2(array->data, array->allocated, array->elem_size); +} + +void * +ARR_GetNewElement(ARR_Instance array) +{ + array->used++; + realloc_array(array, array->used); + return ARR_GetElement(array, array->used - 1); +} + +unsigned int +ARR_GetSize(ARR_Instance array) +{ + return array->used; +} + +// sched.c + +typedef void* SCH_ArbitraryArgument; +typedef void (*SCH_FileHandler)(SCH_ArbitraryArgument); + +typedef struct { + SCH_FileHandler handler; + SCH_ArbitraryArgument arg; +} FileHandlerEntry; + +static ARR_Instance file_handlers; + +void +SCH_Initialise(void) +{ + file_handlers = ARR_CreateInstance(sizeof (FileHandlerEntry)); +} + +void +SCH_AddFileHandler +(SCH_FileHandler handler, SCH_ArbitraryArgument arg) +{ + int fd; // rand + FileHandlerEntry *ptr; + + while (ARR_GetSize(file_handlers) <= fd) { + ptr = ARR_GetNewElement(file_handlers); + ptr->handler = NULL; + ptr->arg = NULL; + } + + ptr = ARR_GetElement(file_handlers, fd); + + /* Don't want to allow the same fd to register a handler more than + once without deleting a previous association - this suggests + a bug somewhere else in the program. */ + assert(!ptr->handler); // UNKNOWN + + ptr->handler = handler; + ptr->arg = arg; +} + +static void +dispatch_filehandlers() +{ + FileHandlerEntry *ptr; + int fd; // rand + + ptr = (FileHandlerEntry *)ARR_GetElement(file_handlers, fd); + SCH_FileHandler stuff = *(ptr->handler); + if (ptr->handler) + (ptr->handler)(ptr->arg); +} + +// nameserv_async.c + +typedef void (*DNS_NameResolveHandler)(void *anything); + +struct DNS_Async_Instance { + DNS_NameResolveHandler handler; + void *arg; + pthread_t thread; +}; + +static void * +start_resolving(void *anything) +{ + struct DNS_Async_Instance *inst = (struct DNS_Async_Instance *)anything; + + return NULL; +} + +static void +end_resolving(void *anything) +{ + struct DNS_Async_Instance *inst = (struct DNS_Async_Instance *)anything; + + DNS_NameResolveHandler h = inst->handler; + (inst->handler)(inst->arg); + + Free(inst); +} + +void +DNS_Name2IPAddressAsync(DNS_NameResolveHandler handler, void *anything) +{ + struct DNS_Async_Instance *inst; + + inst = MallocNew(struct DNS_Async_Instance); + inst->handler = handler; + inst->arg = anything; + + pthread_create(&inst->thread, NULL, start_resolving, inst); + + SCH_AddFileHandler(end_resolving, inst); +} + +// nameserv_async.c copy + +typedef void (*DNS_NameResolveHandler2)(void *anything2); + +struct DNS_Async_Instance2 { + DNS_NameResolveHandler2 handler2; + void *arg2; + pthread_t thread2; +}; + +static void * +start_resolving2(void *anything2) +{ + struct DNS_Async_Instance2 *inst2 = (struct DNS_Async_Instance2 *)anything2; + + return NULL; +} + +static void +end_resolving2(void *anything2) +{ + struct DNS_Async_Instance2 *inst2 = (struct DNS_Async_Instance2 *)anything2; + + DNS_NameResolveHandler2 h = inst2->handler2; + (inst2->handler2)(inst2->arg2); + + Free(inst2); +} + +void +DNS_Name2IPAddressAsync2(DNS_NameResolveHandler2 handler2, void *anything2) +{ + struct DNS_Async_Instance2 *inst2; + + inst2 = MallocNew(struct DNS_Async_Instance2); + inst2->handler2 = handler2; + inst2->arg2 = anything2; + + pthread_create(&inst2->thread2, NULL, start_resolving2, inst2); + + SCH_AddFileHandler(end_resolving2, inst2); +} + +// stub + +void foo(void *arg) { + assert(1); // reachable +} + +void bar(void *arg) { + int *p = arg; + int y = *p; + assert(1); // reachable + assert(y); // TODO +} + +int main() { + SCH_Initialise(); + DNS_Name2IPAddressAsync(foo, NULL); + int x = 1; + DNS_Name2IPAddressAsync2(bar, &x); + dispatch_filehandlers(); + return 0; +} \ No newline at end of file diff --git a/tests/regression/43-struct-domain/30-ambig-field.c b/tests/regression/43-struct-domain/30-ambig-field.c new file mode 100644 index 0000000000..91f18d9df0 --- /dev/null +++ b/tests/regression/43-struct-domain/30-ambig-field.c @@ -0,0 +1,40 @@ +// PARAM: --disable sem.unknown_function.spawn --disable sem.unknown_function.invalidate.globals +#include + +struct S1 { + void (*f1)(void); +}; + +struct S2 { + void (*f2)(void); +}; + +void foo() { + assert(1); // reachable +} + +void bar() { + assert(1); // reachable +} + +int main() { + struct S1 s1 = {.f1 = &foo}; + struct S2 s2 = {.f2 = &bar}; + int r; // rand + void *sp; + + if (r) + sp = &s1; + else + sp = &s2; + // simulate imprecision + // in chrony this wouldn't be path-based but joined in the global invariant + + // one of these field accesses is randomly invalid + void (*fp1)(void) = ((struct S1*)sp)->f1; + void (*fp2)(void) = ((struct S2*)sp)->f2; + // but we shouldn't forget &foo and &bar here and consider both dead + fp1(); + fp2(); + return 0; +}