consolidate integration with cover

Author: peterschrammel

regression/cbmc-cover/consider_goals1/if_icmp1.class

@@ -0,0 +1,31 @@
+class if_icmp1
+{
+  private static void f() {
+    int i = 10;
+    int j = 11;
+    if (i == j) {
+      assert false;
+    }
+    if (i >= j) {
+      assert false;
+    }
+    if (j > i) {
+      assert true;
+    } else {
+      assert false;
+    }
+    if (j <= i) {
+      assert false;
+    }
+    if (j < i) {
+      assert false;
+    } else {
+      assert true;
+    }
+  }
+
+  public static void main(String[] args)
+  {
+    f();
+  }
+}

regression/cbmc-cover/consider_goals1/if_icmp1.java

@@ -0,0 +1,8 @@
+CORE
+if_icmp1.class
+--cover location --no-trivial-tests
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 12 of 27 covered (44.4%)
+--
+^warning: ignoring

regression/cbmc-cover/consider_goals1/test.desc

@@ -0,0 +1,21 @@
+public class Person {
+
+  private int age;
+
+  //public method to get the age variable
+  public int getAge(){
+       return this.age;
+  }
+
+  //public method to set the age variable
+  public void setAge(int age){
+       this.age = age;
+  }
+
+  public static void main(String[] args) {
+    Person p = new Person();
+    p.setAge(10);
+    int x = p.getAge();
+  }
+}
+

regression/cbmc-cover/consider_goals2/Person.class

@@ -0,0 +1,8 @@
+CORE
+Person.class
+--cover location --no-trivial-tests
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 4 of 4 covered (100.0%)
+--
+^warning: ignoring

regression/cbmc-cover/consider_goals2/Person.java

@@ -0,0 +1,28 @@
+public class Person {
+
+  private int age;
+
+  //public method to get the age variable
+  public int getAge(){
+       return this.age;
+  }
+
+  //public method to set the age variable
+  public void setAge(int age){
+       int smokedCigarettes = 3;
+       this.age = age;
+   
+       double averageCigarettesPerYear = smokedCigarettes * 1.0 / age;
+
+       if(averageCigarettesPerYear >= 7300.0) {
+            assert false;
+       }
+  }
+
+  public static void main(String[] args) {
+    Person p = new Person();
+    p.setAge(10);
+    int x = p.getAge();
+  }
+}
+

regression/cbmc-cover/consider_goals2/test.desc

@@ -0,0 +1,8 @@
+CORE
+Person.class
+--cover location --no-trivial-tests
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 11 of 14 covered (78.6%)
+--
+^warning: ignoring

regression/cbmc-cover/consider_goals3/Person.class

@@ -0,0 +1,47 @@
+public class Person {
+
+  private int age;
+  private String x;
+
+  //public method to get the age variable
+  public int getAge(){
+       return this.age;
+  }
+
+  //public method to set the age variable
+  public void setAge(int age){
+       int smokedCigarettes = 3;
+       this.age = age;
+   
+       double averageCigarettesPerYear = smokedCigarettes * 1.0 / age;
+
+       if(averageCigarettesPerYear >= 7300.0) {
+            assert false;
+       }
+  }
+
+
+  public void setX(String newX) {
+    if (newX == null) {
+        x = "";
+    } else {
+        x = newX;
+    }
+  }
+
+  public String getX() {
+    if (x == null) {
+        return "";
+    } else {
+       return x;
+    }
+  }
+
+  public static void main(String[] args) {
+    Person p = new Person();
+    p.setAge(10);
+    int x = p.getAge();
+    String y = p.getX();
+  }
+}
+

regression/cbmc-cover/consider_goals3/Person.java

@@ -0,0 +1,8 @@
+CORE
+Person.class
+--cover location --no-trivial-tests
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 14 of 22 covered (63.6%)
+--
+^warning: ignoring

regression/cbmc-cover/consider_goals3/test.desc

@@ -0,0 +1,52 @@
+public class Person {
+
+  private int age;
+  private String x;
+  private int value;
+
+  //public method to get the age variable
+  public int getAge(){
+       return this.age;
+  }
+
+  //public method to set the age variable
+  public void setAge(int age){
+       int smokedCigarettes = 3;
+       this.age = age;
+   
+       double averageCigarettesPerYear = smokedCigarettes * 1.0 / age;
+
+       if(averageCigarettesPerYear >= 7300.0) {
+            assert false;
+       }
+  }
+
+  public void setX(String newX) {
+    if (newX == null) {
+        x = "";
+    } else {
+        x = newX;
+    }
+  }
+
+  public String getX() {
+    if (x == null) {
+        return "";
+    } else {
+       return x;
+    }
+  }
+  
+  public int getValue() {
+        return value*2; // return twice the value
+  }
+
+  public static void main(String[] args) {
+    Person p = new Person();
+    p.setAge(10);
+    int x = p.getAge();
+    String y = p.getX();
+    int z = p.getValue();
+  }
+}
+

regression/cbmc-cover/consider_goals4/Person.class

@@ -0,0 +1,8 @@
+CORE
+Person.class
+--cover location --no-trivial-tests
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 15 of 23 covered (65.2%)
+--
+^warning: ignoring

regression/cbmc-cover/consider_goals4/Person.java

@@ -0,0 +1,18 @@
+
+public class Account{
+    
+    public static void main(String[] args){
+        String name = "Neil Peart";
+        int ID=2112; 
+        double salary = 1000000;
+        
+        Employee employee = new Employee(name, ID, salary);
+        
+        employee.setName(name);
+        employee.setID(ID);
+        employee.setSalary(salary);
+        
+        employee.display();
+    }
+}
+

regression/cbmc-cover/consider_goals4/test.desc

@@ -0,0 +1,41 @@
+public class Employee {
+    private String name;
+    private int ID;
+    private double salary;
+    
+    public Employee( String name, int ID, double salary){
+        setName(name);
+        setID(ID);
+        setSalary(salary);
+    }
+
+    public void display(){
+        System.out.printf("Employee %s, ID:%d earns %.2f per month", getName(),getID(),getSalary());
+    }
+    
+    public void setName( String name ){
+        this.name = name;
+    }
+    
+    public void setID( int ID ){
+        this.ID = ID;
+    }
+    
+    public void setSalary( double salary ){
+        this.salary = salary;
+    }
+    
+    public String getName(){
+        return name;
+    }
+    
+    public int getID(){
+        return ID;
+    }
+    
+    public double getSalary(){
+        return salary;
+    }
+}
+
+

regression/cbmc-cover/consider_goals5/Person.class

@@ -0,0 +1,8 @@
+CORE
+Account.class
+--cover location --no-trivial-tests
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 13 of 13 covered (100.0%)
+--
+^warning: ignoring

regression/cbmc-cover/consider_goals5/Person.java

@@ -0,0 +1,28 @@
+public class Person {
+
+  private int age;
+
+  //public method to get the age variable
+  public int getAge(){
+       return this.age;
+  }
+
+  //public method to set the age variable
+  public void setAge(int age){
+       int smokedCigarettes = 3;
+       this.age = age;
+   
+       double averageCigarettesPerYear = smokedCigarettes * 1.0 / age;
+
+       if(averageCigarettesPerYear >= 7300.0) {
+            assert false;
+       }
+  }
+
+  public static void main(String[] args) {
+    Person p = new Person();
+    p.setAge(10);
+    int x = p.getAge();
+  }
+}
+

regression/cbmc-cover/consider_goals5/test.desc

@@ -0,0 +1,8 @@
+CORE
+Person.class
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 13 of 16 covered (81.2%)
+--
+^warning: ignoring

regression/cbmc-cover/consider_goals6/Account.class

@@ -0,0 +1,52 @@
+public class Person {
+
+  private int age;
+  private String x;
+  private int value;
+
+  //public method to get the age variable
+  public int getAge(){
+       return this.age;
+  }
+
+  //public method to set the age variable
+  public void setAge(int age){
+       int smokedCigarettes = 3;
+       this.age = age;
+   
+       double averageCigarettesPerYear = smokedCigarettes * 1.0 / age;
+
+       if(averageCigarettesPerYear >= 7300.0) {
+            assert false;
+       }
+  }
+
+  public void setX(String newX) {
+    if (newX == null) {
+        x = "";
+    } else {
+        x = newX;
+    }
+  }
+
+  public String getX() {
+    if (x == null) {
+        return "";
+    } else {
+       return x;
+    }
+  }
+  
+  public int getValue() {
+        return value*2; // return twice the value
+  }
+
+  public static void main(String[] args) {
+    Person p = new Person();
+    p.setAge(10);
+    int x = p.getAge();
+    String y = p.getX();
+    int z = p.getValue();
+  }
+}
+

regression/cbmc-cover/consider_goals6/Account.java

@@ -0,0 +1,8 @@
+CORE
+Person.class
+--cover location
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 18 of 26 covered (69.2%)
+--
+^warning: ignoring