Commit 1fbfd5e
committed
linuxci: test compiling linux
Similarly to Xen, CBMC should be able to compile the linux kernel. As
compiling the full kernel is very time consuming, and with CBMC also
space consuming, only compile a core part all its dependencies, with
the smalles configuration possible. For this core part, we select the
KVM hypervisor.
Once this is working, the configuration, as well as targets to be
compiled can be increased.
When the linuxci fails, we want to be able to easily understand the
failure. The used one-line-scan tool already captures input files that
cannot be handled by goto-cc. Hence, also archives these files for easy
access in the web UI.
Signed-off-by: Norbert Manthey <nmanthey@amazon.de>1 parent 4b46a0a commit 1fbfd5e
1 file changed
+53
-0
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| 10 | + | |
| 11 | + | |
| 12 | + | |
| 13 | + | |
| 14 | + | |
| 15 | + | |
| 16 | + | |
| 17 | + | |
| 18 | + | |
| 19 | + | |
| 20 | + | |
| 21 | + | |
| 22 | + | |
| 23 | + | |
| 24 | + | |
| 25 | + | |
| 26 | + | |
| 27 | + | |
| 28 | + | |
| 29 | + | |
| 30 | + | |
| 31 | + | |
| 32 | + | |
| 33 | + | |
| 34 | + | |
| 35 | + | |
| 36 | + | |
| 37 | + | |
| 38 | + | |
| 39 | + | |
| 40 | + | |
| 41 | + | |
| 42 | + | |
| 43 | + | |
| 44 | + | |
| 45 | + | |
| 46 | + | |
| 47 | + | |
| 48 | + | |
| 49 | + | |
| 50 | + | |
| 51 | + | |
| 52 | + | |
| 53 | + | |
0 commit comments