mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-18 22:56:26 +00:00
Code Activity

Fix instance of "flexible array member". (#9883)

Browse source 
This is another PR towards the goal of getting a clean build with clang,
using the compiler options used in building clang-tidy.

In https://github.com/Z3Prover/z3/pull/9800, we changed the build flags
to eliminate a warning for zero-length arrays. In that PR, I missed this
one: there was one instance of m_arr[] instead of m_arr[0]. In the
clang-tidy build, that gives warnings like:
```
/Users/daviddetlefs/llvm-project/build_dbg/_deps/z3-src/src/model/func_interp.h:43:12: warning: flexible array members are a C99 feature [-Wc99-extensions]
```

The PR fixes this, making it a zero-length array, the idiom used in all
the other similar cases. I also added the compiler flag that produced
this warning, so we can notice such changes in the future.
This commit is contained in:
davedets 2026-06-16 15:09:18 -07:00 • committed by GitHub
parent bcc3523b23
commit 9091df56cb
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/model/func_interp.h
View file

@ -40,7 +40,7 @@ class func_entry {
// m_result and m_args[i] must be ground terms.
expr * m_result;
expr * m_args[];
expr * m_args[0];
static unsigned get_obj_size(unsigned arity) { return sizeof(func_entry) + arity * sizeof(expr*); }
func_entry(ast_manager & m, unsigned arity, expr * const * args, expr * result);