Z3Prover / z3

The Z3 Theorem Prover
Other
10.16k stars 1.47k forks source link

Compilation warnings on Mac (fresh pull of master) #4727

Closed LeventErkok closed 3 years ago

LeventErkok commented 3 years ago

In case this is of interest. The following seems particularly worrisome:

../src/sat/smt/q_model_finder.cpp:29:13: warning: reference 'ctx' is not yet bound to a value when used here [-Wuninitialized]
        ctx(ctx), m(ctx.get_manager()) {}
            ^

There're also the following warnings, which seem more benign:

../src/smt/smt_model_finder.h:123:32: warning: 'operator()' overrides a member function but is not marked 'override'
      [-Winconsistent-missing-override]
        quantifier_macro_info* operator()(quantifier* q);
                               ^
../src/model/model_macro_solver.h:24:36: note: overridden virtual function is here
    virtual quantifier_macro_info* operator()(quantifier* q) = 0;
                                   ^
../src/sat/smt/q_model_fixer.h:74:32: warning: 'operator()' overrides a member function but is not marked 'override'
      [-Winconsistent-missing-override]
        quantifier_macro_info* operator()(quantifier* q);
                               ^
../src/sat/smt/fpa_solver.h:74:25: warning: 'clone' overrides a member function but is not marked 'override' [-Winconsistent-missing-override]
        euf::th_solver* clone(sat::solver*, euf::solver& ctx) { return alloc(solver, ctx); }
                        ^
../src/sat/smt/sat_th.h:102:28: note: overridden virtual function is here
        virtual th_solver* clone(sat::solver* s, euf::solver& ctx) = 0;  
                           ^
../src/sat/smt/q_model_fixer.h:74:32: warning: 'operator()' overrides a member function but is not marked 'override'
      [-Winconsistent-missing-override]
        quantifier_macro_info* operator()(quantifier* q);
                               ^
../src/model/model_macro_solver.h:24:36: note: overridden virtual function is here
    virtual quantifier_macro_info* operator()(quantifier* q) = 0;
                                   ^
../src/sat/smt/q_model_fixer.h:74:32: warning: 'operator()' overrides a member function but is not marked 'override'
      [-Winconsistent-missing-override]
        quantifier_macro_info* operator()(quantifier* q);
                               ^
../src/model/model_macro_solver.h:24:36: note: overridden virtual function is here
    virtual quantifier_macro_info* operator()(quantifier* q) = 0;
                                   ^
../src/sat/smt/fpa_solver.h:74:25: warning: 'clone' overrides a member function but is not marked 'override' [-Winconsistent-missing-override]
        euf::th_solver* clone(sat::solver*, euf::solver& ctx) { return alloc(solver, ctx); }
                        ^
../src/sat/smt/sat_th.h:102:28: note: overridden virtual function is here
        virtual th_solver* clone(sat::solver* s, euf::solver& ctx) = 0;  
                           ^
nunoplopes commented 3 years ago

Nikolaj has fixed these, thanks.

LeventErkok commented 3 years ago

@nunoplopes I'm still seeing these:

../src/smt/smt_model_finder.h:123:32: warning: 'operator()' overrides a member function but is not marked 'override' [-Winconsistent-missing-override]
        quantifier_macro_info* operator()(quantifier* q);
                               ^
../src/model/model_macro_solver.h:24:36: note: overridden virtual function is here
    virtual quantifier_macro_info* operator()(quantifier* q) = 0;
                                   ^
LeventErkok commented 3 years ago

@nunoplopes @NikolajBjorner

I also always get this:

/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/ranlib: file: math/lp/lp.a(dense_matrix.o) has no symbols

Though this is probably just informative and not anything to worry about.

nunoplopes commented 3 years ago

Fixed the override warning, thanks! The ranlib one can't be fixed, but it's benign.