added more tests

regression-tests/double/div_3.c

@@ -0,0 +1,7 @@
+//SAFE (WILL BE UNSAFE DUE TO APPROXIMATIONS FROM FRACTION)
+int main () {
+  double a = 4.0;
+  double b = 0.1;
+  assert(a/b== 40.0);
+  return 0;
+}

regression-tests/float/simple_bsed_orig_code.c

@@ -0,0 +1,87 @@
+//Global variables 'acting' as return variables
+int return_modMin;
+int return_modMax;
+int return_modStatus;
+
+int mod0_status;
+int mod1_status;
+
+int mod0_min;
+int mod1_min;
+
+int mod0_max;
+int mod1_max;
+
+int batt_min_output;
+int batt_max_output;
+int batt_status_output;
+
+void modStatus(int idx) {
+    if (idx == 0) {
+      return_modStatus = mod0_status;
+    } else {
+      return_modStatus = mod1_status;
+    }
+}
+
+void modMin(int idx) {
+    if (idx == 0) {
+      return_modMin = mod0_min;
+    } else {
+      return_modMin = mod1_min;
+    }
+}
+
+void modMax(int idx) {
+    if (idx == 0) {
+      return_modMax = mod0_max;
+    } else {
+      return_modMax = mod1_max;
+    }
+}
+
+void moduleDiag(int idx) {
+  modMin(idx);
+  modMax(idx);
+  modStatus(idx);
+
+  //Update the status
+  if (return_modStatus == 1) {
+    batt_status_output = 1;
+  } else {
+    batt_status_output = batt_status_output;
+  }
+
+  //Update the max value
+  if (return_modMax > batt_max_output) {
+    batt_max_output = return_modMax;
+  } else {
+    batt_max_output = batt_max_output;
+  }
+
+  //Update the min value
+  if (return_modMin < batt_min_output) {
+    batt_min_output = return_modMin;
+  } else {
+    batt_min_output = batt_min_output;
+  }
+}
+
+/*@
+  assigns return_modMax, return_modMin, return_modStatus, batt_min_output,
+          batt_max_output, batt_status_output;
+  ensures
+    ((\old(mod0_status) == 0 && \old(mod1_status) == 0) ==> batt_status_output == 0) &&
+    ((\old(mod0_status) == 1 || \old(mod1_status) == 1) ==> batt_status_output == 1);
+*/
+void batteryDiag(int dummy)
+{
+    //Initializing the battery values
+    batt_max_output = -2147483648;
+    batt_min_output = 2147483647;
+    batt_status_output = 0;
+
+    //Run the diagnostics, one module at the time
+    moduleDiag(0);
+    moduleDiag(1);
+}

regression-tests/float/simple_bsed_test.c

@@ -0,0 +1,122 @@
+//Global variables 'acting' as return variables
+float return_modMin;
+float return_modMax;
+int return_modStatus;
+
+int mod0_status;
+int mod1_status;
+
+float mod0_min;
+float mod1_min;
+
+float mod0_max;
+float mod1_max;
+
+float batt_min_output;
+float batt_max_output;
+int batt_status_output;
+
+/*@contract@*/
+void modStatus(int idx) {
+    if (idx == 0) {
+      return_modStatus = mod0_status;
+    } else {
+      return_modStatus = mod1_status;
+    }
+}
+
+/*@contract@*/
+void modMin(int idx) {
+    if (idx == 0) {
+      return_modMin = mod0_min;
+    } else {
+      return_modMin = mod1_min;
+    }
+}
+
+/*@contract@*/
+void modMax(int idx) {
+    if (idx == 0) {
+      return_modMax = mod0_max;
+    } else {
+      return_modMax = mod1_max;
+    }
+}
+
+/*@contract@*/
+void moduleDiag(int idx) {
+  modMin(idx);
+  modMax(idx);
+  modStatus(idx);
+
+  //Update the status
+  if (return_modStatus == 1) {
+    batt_status_output = 1;
+  } else {
+    batt_status_output = batt_status_output;
+  }
+
+  //Update the max value
+  if (return_modMax > batt_max_output) {
+    batt_max_output = return_modMax;
+  } else {
+    batt_max_output = batt_max_output;
+  }
+
+  //Update the min value
+  if (return_modMin < batt_min_output) {
+    batt_min_output = return_modMin;
+  } else {
+    batt_min_output = batt_min_output;
+  }
+}
+
+void batteryDiag(int dummy)
+{
+    //Initializing the battery values
+    batt_max_output = 5.0f;
+    batt_min_output = -5.0f;
+    batt_status_output = 0;
+
+    //Run the diagnostics, one module at the time
+    moduleDiag(0);
+    moduleDiag(1);
+}
+int extern non_det();
+
+void main()
+{
+  //Non-det assignment of all global C variables
+  // return_modMin = 0.0f;
+  // return_modMax = 0.0f;
+  // return_modStatus = 0;
+  mod0_status = non_det();
+  mod1_status = non_det();
+  mod0_min = -1.0f;
+  mod1_min = -1.0f;
+  mod0_max = 2.0f;
+  mod1_max = 2.0f;
+  // batt_max_output = -200.0f;
+  //batt_min_output = 200.0f;
+  // batt_status_output = 0;
+
+  //Declare the paramters of the function to be called
+  int dummy;
+
+  //Initialization of logical old-variables
+  // int old_mod0_status;
+  // int old_mod1_status;
+  // int old_batt_status_output;
+  // assume(old_mod0_status == mod0_status);
+  // assume(old_mod1_status == mod1_status);
+  // assume(old_batt_status_output == batt_status_output);
+
+  //Function call that the harness function verifies
+  batteryDiag(dummy);
+
+  //The 'ensures'-clauses translated into asserts
+  //  assert((!(((old_mod0_status == 0) && (old_mod1_status == 0)) &&
+  //    !(batt_status_output == 0)) && !(((old_mod0_status == 1) ||
+  //    (old_mod1_status == 1)) && !(batt_status_output == 1))));
+  assert(batt_max_output==-5.0f);
+}

regression-tests/float/simple_bsed_tricera.c

@@ -0,0 +1,122 @@
+//Global variables 'acting' as return variables
+int return_modMin;
+int return_modMax;
+int return_modStatus;
+
+int mod0_status;
+int mod1_status;
+
+int mod0_min;
+int mod1_min;
+
+int mod0_max;
+int mod1_max;
+
+int batt_min_output;
+int batt_max_output;
+int batt_status_output;
+
+/*@contract@*/
+void modStatus(int idx) {
+    if (idx == 0) {
+      return_modStatus = mod0_status;
+    } else {
+      return_modStatus = mod1_status;
+    }
+}
+
+/*@contract@*/
+void modMin(int idx) {
+    if (idx == 0) {
+      return_modMin = mod0_min;
+    } else {
+      return_modMin = mod1_min;
+    }
+}
+
+/*@contract@*/
+void modMax(int idx) {
+    if (idx == 0) {
+      return_modMax = mod0_max;
+    } else {
+      return_modMax = mod1_max;
+    }
+}
+
+/*@contract@*/
+void moduleDiag(int idx) {
+  modMin(idx);
+  modMax(idx);
+  modStatus(idx);
+
+  //Update the status
+  if (return_modStatus == 1) {
+    batt_status_output = 1;
+  } else {
+    batt_status_output = batt_status_output;
+  }
+
+  //Update the max value
+  if (return_modMax > batt_max_output) {
+    batt_max_output = return_modMax;
+  } else {
+    batt_max_output = batt_max_output;
+  }
+
+  //Update the min value
+  if (return_modMin < batt_min_output) {
+    batt_min_output = return_modMin;
+  } else {
+    batt_min_output = batt_min_output;
+  }
+}
+
+void batteryDiag(int dummy)
+{
+    //Initializing the battery values
+    batt_max_output = -2147483648;
+    batt_min_output = 2147483647;
+    batt_status_output = 0;
+
+    //Run the diagnostics, one module at the time
+    moduleDiag(0);
+    moduleDiag(1);
+}
+
+extern int non_det();
+
+void main()
+{
+  //Non-det assignment of all global C variables
+  return_modMin = non_det();
+  return_modMax = non_det();
+  return_modStatus = non_det();
+  mod0_status = non_det();
+  mod1_status = non_det();
+  mod0_min = non_det();
+  mod1_min = non_det();
+  mod0_max = non_det();
+  mod1_max = non_det();
+  batt_min_output = non_det();
+  batt_max_output = non_det();
+  batt_status_output = non_det();
+
+  //Declare the paramters of the function to be called
+  int dummy;
+
+  //Initialization of logical old-variables
+  int old_mod0_status;
+  int old_mod1_status;
+  int old_batt_status_output;
+  assume(old_mod0_status == mod0_status);
+  assume(old_mod1_status == mod1_status);
+  assume(old_batt_status_output == batt_status_output);
+
+  //Function call that the harness function verifies
+  batteryDiag(dummy);
+
+  //The 'ensures'-clauses translated into asserts
+  assert((!(((old_mod0_status == 0) && (old_mod1_status == 0)) &&
+    !(batt_status_output == 0)) && !(((old_mod0_status == 1) ||
+    (old_mod1_status == 1)) && !(batt_status_output == 1))));
+}