Closed lsf37 closed 2 months ago
Could this be something from lone time ago when SMP support was added. So checking `CONFIG_MAX_NUM_NODES' implied checking SMP support?
Could this be something from lone time ago when SMP support was added. So checking `CONFIG_MAX_NUM_NODES' implied checking SMP support?
It's possible that this is very old and made sense in a previous build system. There was a previous commit (1612acca477697f) that fixed a lot of these, but seems to have missed these two.
I should note that I have checked all other instances of config_set
now and they all refer to boolean values only, so these should really be the last ones unless somebody introduces new instances.
The FPU0002
test seems to be passing, but as expected IPC0028
is failing.
We should only merge this one after a fix for IPC0028
is merged (e.g. something like https://github.com/seL4/seL4/pull/986).
The offending commit that introduced these was https://github.com/seL4/sel4test/commit/d07b2383b563015d8e7dad5c587493be01cf8b3c from 2017. I've now added a commit on top that disables IPC0028 so we can at least re-enable the other test.
I'll make a new PR that re-enables IPC0028 which we can use for testing possible solutions for the issue with IPC0028.
config_set is true for 1 and false for all other values, so it does not make sense to use with CONFIG_MAX_NUM_NODES.
The two instances where this happened look like they are trying to guard CONFIG_MAX_NUM_NODES > 1 by checking whether CONFIG_MAX_NUM_NODES has any value at all, but doing so incorrectly. CONFIG_MAX_NUM_NODES has a default value of 1 and should always be set to a number, so we can just drop the guard. If this assumption about always having a numbers value is wrong, the code will not compile, which is acceptable.
Thanks to @jearc for spotting these.
This wrong setting has masked two SMP tests, which may now be failing.