Feature #10461

Support verification of Linux kernel modules on the ARM architecture

Added by Evgeny Novikov 5 months ago. Updated 5 months ago.

Target version:
Start date:
Due date:
% Done:


Estimated time:
(Total: 0.00 h)
Published in build:


As an example of the ARM support let's consider verification of Linux kernel modules on this architecture.


Feature #10472: Support lightweight configuration of verification tools for target architectureClosedIlja Zakharov




Updated by Evgeny Novikov 5 months ago

I expect 3 components of Klever needs to be adjusted to meet a non-standard architecture. They are CIF, CIL and a verifier (at the moment just CPAchecker). I hope that at least for CIL and CPAchecker nothing except some (maybe just one) option will be necessary. As for CIF, cross CIF should be used. Anyway, I do not expect many differences between various architectures. Moreover, we can take into account different aspects of particular projects by describing architecture adjustments separately for all supported project if they need this at all.

That's why I suggest to include a new file called architecture.json which will incorporate all specific stuff corresponding to different architectures into verification jobs and allow users to select one of described architectures within job.json.

If somebody has any objections it would be great to hear them here soon before I will implement the suggested approach.


Updated by Evgeny Novikov 5 months ago

  • Status changed from New to Resolved

I did the job in branch arm-support. I did not implement a job specific architecture description because we do not support appropriate projects for testing. So, architecture specific configuration is global for all now, but it will be quite easy to change this in future if necessary.

Besides, CIL does not support ARM specific processing (#10471), but it does not seem that this cause considerable issues.

If one would like to verify Linux kernel modules on ARM, one should get cross CIF (How to get cross CIF for building and verification of Linux kernel loadable modules on ARM), prepare an appropriate build base and specify "architecture": "ARM" within job.json.


Updated by Evgeny Novikov 5 months ago

  • Status changed from Resolved to Closed

Tests passed, so, I merged the branch to master in e6a028d78.

Also available in: Atom PDF