diff --git a/regression/cbmc/simplify-array-size/main.c b/regression/cbmc/simplify-array-size/main.c new file mode 100644 index 00000000000..e25583325ad --- /dev/null +++ b/regression/cbmc/simplify-array-size/main.c @@ -0,0 +1,36 @@ +#include +#include + +struct state +{ + size_t size; + int slots[]; +}; + +struct hash_table +{ + struct state *p_impl; +}; + +void main(void) +{ + struct hash_table map; + size_t num_entries; + __CPROVER_assume(num_entries <= 8ul); + size_t required_bytes = num_entries * sizeof(int) + sizeof(struct state); + struct state *impl = malloc(required_bytes); + if(impl != NULL) + { + impl->size = num_entries; + map.p_impl = impl; + } + else + map.p_impl = NULL; + + if(impl != NULL) + { + // keep this line even though it is never read + struct state *state = impl; + memset(impl->slots, 0, sizeof(int) * map.p_impl->size); + } +} diff --git a/regression/cbmc/simplify-array-size/test.desc b/regression/cbmc/simplify-array-size/test.desc new file mode 100644 index 00000000000..b06cb557a6d --- /dev/null +++ b/regression/cbmc/simplify-array-size/test.desc @@ -0,0 +1,12 @@ +CORE broken-smt-backend +main.c +--malloc-may-fail --malloc-fail-null +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^Invariant check failed +^warning: ignoring +-- +Simplification of array sizes must be applied consistently and must not result +in value-set assignment invariant failures. diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 4d6f1d8352f..7bb55a18693 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -84,6 +84,8 @@ renamedt goto_symex_statet::assignment( // the type might need renaming rename(lhs.type(), l1_identifier, ns); + if(rhs_is_simplified) + simplify(lhs, ns); lhs.update_type(); if(run_validation_checks) {