fixing some compilation issues with the benchmarks

Author: sohah

java/java-ranger-regression/alarm/impl/ALARM_Functional.java

@@ -1712,78 +1712,5 @@ void ALARM_Functional(Infusion_Manager_Outputs rtu_IM_IN,
         rty_ALARM_OUT.Highest_Level_Alarm = localB.ALARM_OUT_Highest_Level_Alarm;
         rty_ALARM_OUT.Log_Message_ID = localB.ALARM_OUT_Log_Message_ID;
 
-       /* boolean checkCondition;
-        boolean checkOutput;
-
-
-        //Prop1: empty_reservoir_implies_alarm_L4
-        checkCondition = rtu_TLM_MODE_IN.System_On && rtu_SYS_STAT_IN.In_Therapy && rtu_SYS_STAT_IN.Reservoir_Empty;
-        checkOutput = rty_ALARM_OUT.Highest_Level_Alarm == 4;
-        assert (!checkCondition || checkOutput);
-*/
-
-        //Prop2: air_in_line_implies_grt_L3_alarm
-        /*checkCondition = (rtu_TLM_MODE_IN.System_On && rtu_SENSOR_IN.Air_In_Line);
-        checkOutput = (rty_ALARM_OUT.Highest_Level_Alarm >= 3);
-        assert (!checkCondition || checkOutput);*/
-
-        /*
-        // Prop3: volume_infused_grt_VTBI_Hi_causes_grt_L3_alarm
-        checkCondition =
-                (rtu_TLM_MODE_IN.System_On && rtu_SYS_STAT_IN.In_Therapy && (rtu_SYS_STAT_IN.Volume_Infused > rtu_DB_IN.VTBI_High));
-        checkOutput = (rty_ALARM_OUT.Highest_Level_Alarm >= 3);
-        assert (!checkCondition || checkOutput);
-
-        // Prop4: occlusion_implies_grt_L3_alarm
-        checkCondition = (rtu_TLM_MODE_IN.System_On && rtu_SENSOR_IN.Occlusion);
-        checkOutput = (rty_ALARM_OUT.Highest_Level_Alarm >= 3);
-        assert (!checkCondition || checkOutput);
-*/
-        //      Prop5: door_open_implies_grt_L3_alarm
-        /*checkCondition = (rtu_TLM_MODE_IN.System_On && rtu_SENSOR_IN.Door_Open);
-        checkOutput = (rty_ALARM_OUT.Highest_Level_Alarm >= 3);
-        assert (!checkCondition || checkOutput);*/
-/*
-        //Prop6: alarm_gte_L3_causes_audio_output_EQ_audio_level
-        checkCondition =
-                (rtu_TLM_MODE_IN.System_On && (rty_ALARM_OUT.Highest_Level_Alarm >= 3) && (rtu_OP_CMD_IN.Disable_Audio == 0));
-        checkOutput =
-                ((rty_ALARM_OUT.Audio_Notification_Command == rtu_CONST_IN.Audio_Level) && (rty_ALARM_OUT.Is_Audio_Disabled == 0));
-        assert (!checkCondition || checkOutput);
-
-
-        //Prop7: no_audio_if_audio_disabled
-        checkCondition = (rtu_TLM_MODE_IN.System_On && (rtu_OP_CMD_IN.Disable_Audio > 0));
-        checkOutput =
-                ((rty_ALARM_OUT.Audio_Notification_Command == 0) && (rty_ALARM_OUT.Is_Audio_Disabled == rtu_OP_CMD_IN.Disable_Audio));
-        assert (!checkCondition || checkOutput);
-
-        //Prop8: low_reservoir_implies_grt_L2_alarm
-        checkCondition =
-                (rtu_TLM_MODE_IN.System_On && rtu_SYS_STAT_IN.In_Therapy && (rtu_SYS_STAT_IN.Reservoir_Volume < rtu_CONST_IN.Low_Reservoir));
-        checkOutput = (rty_ALARM_OUT.Highest_Level_Alarm >= 2);
-        assert (!checkCondition || checkOutput);
-
-        //Prop9 : alarm_value_range
-        checkCondition = (rtu_TLM_MODE_IN.System_On);
-        checkOutput = ((rty_ALARM_OUT.Highest_Level_Alarm >= 0) && (rty_ALARM_OUT.Highest_Level_Alarm <= 4));
-        assert (!checkCondition || checkOutput);
-*/
-        //Prop10: audio_disabled_range
-        /*checkCondition = (rtu_TLM_MODE_IN.System_On);
-        checkOutput = (rty_ALARM_OUT.Is_Audio_Disabled == rtu_OP_CMD_IN.Disable_Audio);
-        assert (!checkCondition || checkOutput);
-*/
-
-        /*************** discovery repaired properties *******************/
-       /* checkCondition = (rtu_TLM_MODE_IN.System_On && rtu_SYS_STAT_IN.In_Therapy && rtu_SYS_STAT_IN.Reservoir_Empty);
-        checkOutput = (rty_ALARM_OUT.Log_Message_ID ==0) ^ (rty_ALARM_OUT.Log_Message_ID == 77);
-        assert (!checkCondition || checkOutput);
-*/
-
-
-        //assert ((rty_ALARM_OUT.Notification_Message <= 19) && (rty_ALARM_OUT.Notification_Message > 0));
-//        assert !(rty_ALARM_OUT.Highest_Level_Alarm == 0 && (rtu_TLM_MODE_IN.System_On));
-
     }
 }

java/java-ranger-regression/alarm/impl/Alarm_Outputs.java

@@ -1,3 +1,4 @@
+import org.sosy_lab.sv_benchmarks.Verifier;
 
 public class Alarm_Outputs {
     int Is_Audio_Disabled = Verifier.nondetInt();

java/java-ranger-regression/alarm/impl/Config_Outputs.java

@@ -1,3 +1,4 @@
+import org.sosy_lab.sv_benchmarks.Verifier;
 
 public class Config_Outputs {
     int Patient_ID = Verifier.nondetInt();

java/java-ranger-regression/alarm/impl/Device_Configuration_Inputs.java

@@ -1,3 +1,4 @@
+import org.sosy_lab.sv_benchmarks.Verifier;
 
 public class Device_Configuration_Inputs {
     int Audio_Enable_Duration = Verifier.nondetInt();

java/java-ranger-regression/alarm/impl/Device_Sensor_Inputs.java

@@ -1,3 +1,4 @@
+import org.sosy_lab.sv_benchmarks.Verifier;
 
 public class Device_Sensor_Inputs {
 

java/java-ranger-regression/alarm/impl/Drug_Database_Inputs.java

@@ -1,3 +1,4 @@
+import org.sosy_lab.sv_benchmarks.Verifier;
 
 public class Drug_Database_Inputs {
 

java/java-ranger-regression/alarm/impl/Infusion_Manager_Outputs.java

@@ -1,3 +1,4 @@
+import org.sosy_lab.sv_benchmarks.Verifier;
 
 public class Infusion_Manager_Outputs {
     public int Commanded_Flow_Rate = Verifier.nondetInt();

java/java-ranger-regression/alarm/impl/Log_Output.java

@@ -1,3 +1,4 @@
+import org.sosy_lab.sv_benchmarks.Verifier;
 
 public class Log_Output {
     public int Log = Verifier.nondetInt();

java/java-ranger-regression/alarm/impl/Operator_Commands.java

@@ -1,3 +1,4 @@
+import org.sosy_lab.sv_benchmarks.Verifier;
 
 public class Operator_Commands {
 

java/java-ranger-regression/alarm/impl/System_Monitor_Output.java

@@ -1,3 +1,4 @@
+import org.sosy_lab.sv_benchmarks.Verifier;
 
 public class System_Monitor_Output {
     boolean System_Monitor_Failed = Verifier.nondetBoolean();