Use passed in options to set scheduler

[palacios.git] / palacios / src / palacios / vmm.c

diff --git a/palacios/src/palacios/vmm.c b/palacios/src/palacios/vmm.c
index 5f164b7..6e32e88 100644 (file)
--- a/palacios/src/palacios/vmm.c
+++ b/palacios/src/palacios/vmm.c
@@ -26,7 +26,7 @@
 #include <palacios/vmm_sprintf.h>
 #include <palacios/vmm_extensions.h>
 #include <palacios/vmm_timeout.h>
-
+#include <palacios/vmm_options.h>
 
 #ifdef V3_CONFIG_SVM
 #include <palacios/svm.h>
@@ -99,8 +99,7 @@ static void deinit_cpu(void * arg) {
     }
 }
 
-
-void Init_V3(struct v3_os_hooks * hooks, char * cpu_mask, int num_cpus) {
+void Init_V3(struct v3_os_hooks * hooks, char * cpu_mask, int num_cpus, char *options) {
     int i = 0;
     int minor = 0;
     int major = 0;
@@ -117,6 +116,9 @@ void Init_V3(struct v3_os_hooks * hooks, char * cpu_mask, int num_cpus) {
        v3_cpu_types[i] = V3_INVALID_CPU;
     }
 
+    // Parse host-os defined options into an easily-accessed format.
+    v3_parse_options(options);
+
     // Register all the possible device types
     V3_init_devices();