/*
In this file we present the complete set of tests that reveals the 84 nonconformances in Samples and Real Programs evaluated with the JMLOK tool.
*/
// Samples
/* Test cases that reveal non conformances in the package BoundedStack */
// Class BoundedStack
public void testBoundedStack1(){
BoundedStack var1 = new BoundedStack(0);
}
public void testBoundedStack2(){
BoundedStack var1 = new BoundedStack((-1));
}
/* Test cases that reveal non conformances in the package dbc */
// Class Polar
public void testAngle(){
Polar var2 = new Polar(3.296908309475615d, 10.0d);
double var3 = var2.angle();
}
public void testImaginaryPart(){
Polar var2 = new Polar(0.0d, (-84.14709848078965d));
double var3 = var2.imaginaryPart();
}
public void testMagnitude(){
Polar var5 = new Polar(10.0d, 0.0d);
Rectangular var7 = new Rectangular(10.0d);
Complex var8 = var5.mul((Complex)var7);
}
public void testRealPart(){
Polar var2 = new Polar(100.0d, (-1.0d));
Polar var5 = new Polar(10.0d, 0.0d);
Complex var8 = var2.add((Complex)var5);
}
// Class Rectangular
public void testAngle(){
Rectangular var2 = new Rectangular(3.141592653589793d, 10.0d);
double var3 = var2.angle();
}
public void testImaginaryPart(){
Rectangular var1 = new Rectangular((-1.0d));
double var2 = var1.imaginaryPart();
}
public void testMagnitude{
Rectangular var2 = new Rectangular((-1.0d), 3.141592653589793d);
double var3 = var2.magnitude();
}
public void testRealPart(){
Rectangular var6 = new Rectangular((-1.0d));
double var7 = var6.realPart();
}
/* Test cases that reveal non conformances in the package list*/
// Class Link
public void testLink(){
OneWayNode var1 = new OneWayNode((java.lang.Object)0.0f);
Link var2 = var1.getNextLink();
Object var3 = var2.getEntry();
}
// Class E_OneWayList (list2)
public void testE_OneWayList(){
E_OneWayList var0 = new E_OneWayList();
assertTrue("Contract failed: var0.equals(var0)", var0.equals(var0));
}
// Class E_OneWayList (list3)
public void testE_OneWayList(){
TwoWayList var0 = new TwoWayList();
assertTrue("Contract failed: var0.equals(var0)", var0.equals(var0));
}
// Class TwoWayIterator (list3)
// Method isDone
public void testIsDone(){
TwoWayNode var0 = new TwoWayNode();
TwoWayIterator var2 = new TwoWayIterator(var0);
var2.last();
var2.last();
boolean var5 = var2.isDone();
}
// Method next
public void testNext(){
TwoWayNode var0 = new TwoWayNode();
TwoWayIterator var2 = new TwoWayIterator(var0);
var2.last();
var2.next();
}
/*Test cases that reveal non conformances in the package misc*/
// Class SingleSolution
public void testLimit(){
EqualsN var1 = new EqualsN((-214));
int var2 = var1.limit();
}
/* Test cases that reveal non conformances in the package stacks */
// Class BoundedStack
public void testBoundedStack1(){
BoundedStack var1 = new BoundedStack(0);
}
public void testBoundedStack2(){
BoundedStack var1 = new BoundedStack((-1));
}
/* ------------------------------------------------------------ */
// Real programs
// Bomber
// Class Building
public void testBuilding(){
Building var0 = new Building();
}
// Class Common
public void testCommon(){
int var4 = Common.distancePointToLine(32, (-4), 10, 1);
}
// Class Explosion
public void testExplosion(){
int[] var1 = new int[] { 1};
Explosion var11 = new Explosion(var1, 100, 0, (byte)10, 100, 1, 10, 1, (byte)(-1), (byte)1);
}
// Class FlakSmoke
public void testFlakSmoke(){
FlakSmoke var3 = new FlakSmoke(2, (-12288), 92160);
Object var10 = var3.getBoundingBox();
}
//HealthCard
// Class Allergies_Impl
public void testGetAllergyDesignation(){
Allergies_Impl var0 = new Allergies_Impl();
byte[] var4 = var0.getAllergyDesignation((short)10);
}
public void testRemoveAllergy(){
Allergies_Impl var0 = new Allergies_Impl();
var0.removeAllergy((short)3);
}
public void testSetAllergyDate(){
Allergies_Impl var0 = new Allergies_Impl();
Medicine_Impl var24 = new Medicine_Impl((byte)0, (byte)10, (byte)1, (byte)0);
byte[] var26 = var24.getDate();
CardUtil.cleanField(var26);
var0.setAllergyDate((short)3, var26);
}
public void testSetAllergyDesignation(){
byte[] var13 = new byte[] { (byte)(-1), (byte)1, (byte)10};
Allergies_Impl var0 = new Allergies_Impl();
Allergies_Impl var19 = new Allergies_Impl();
byte[] var21 = var19.getAllergyDate((short)0);
CardUtil.arrayCopy(var13, var21);
var0.setAllergyDesignation((short)10, var21);
}
// Class Appointments_Impl
public void testAppointments_Impl(){
Treatments_Impl var0 = new Treatments_Impl();
}
// Class CardException
public void testCardException(){
UserException.throwIt((short)514);
}
// Class CardRuntimeException
public void testCardRuntimeException(){
TransactionException.throwIt((short)1);
}
// Interface Common
public void testGetDate(){
byte[] var2 = new byte[] { (byte)10};
byte[] var5 = new byte[] { (byte)0, (byte)(-1)};
byte[] var9 = new byte[] { (byte)(-1), (byte)1, (byte)10};
byte[] var12 = new byte[] { (byte)1, (byte)100};
Appointment_Impl var14 = new Appointment_Impl((byte)10, var2, var5, var9, var12, (byte)0);
byte[] var15 = var14.getDate();
}
public void testGetHour(){
byte[] var12 = new byte[] { (byte)10};
byte[] var15 = new byte[] { (byte)0, (byte)(-1)};
byte[] var19 = new byte[] { (byte)(-1), (byte)1, (byte)10};
byte[] var22 = new byte[] { (byte)1, (byte)100};
Appointment_Impl var24 = new Appointment_Impl((byte)10, var12, var15, var19, var22, (byte)0);
byte[] var25 = var24.getHour();
}
public void testGetType(){
byte[] var2 = new byte[] { (byte)10};
byte[] var5 = new byte[] { (byte)0, (byte)(-1)};
byte[] var9 = new byte[] { (byte)(-1), (byte)1, (byte)10};
byte[] var12 = new byte[] { (byte)1, (byte)100};
Appointment_Impl var14 = new Appointment_Impl((byte)10, var2, var5, var9, var12, (byte)0);
byte var15 = var14.getType();
}
public void testVaccinationDate(){
byte[] var2 = new byte[] { (byte)0, (byte)0};
byte[] var4 = new byte[] { (byte)1};
Vaccine_Impl var5 = new Vaccine_Impl(var2, var4);
byte[] var6 = var5.getVaccinationDate();
}
public void testSetDate(){
Medicine_Impl var4 = new Medicine_Impl((byte)0, (byte)10, (byte)1, (byte)0);
var4.setTreatmentID((byte)0);
byte[] var17 = new byte[] { (byte)(-1), (byte)1, (byte)10};
Allergies_Impl var23 = new Allergies_Impl();
byte[] var25 = var23.getAllergyDate((short)0);
CardUtil.arrayCopy(var17, var25);
var4.setDate(var25);
}
public void testToString(){
byte[] var2 = new byte[] { (byte)10};
byte[] var5 = new byte[] { (byte)0, (byte)(-1)};
byte[] var9 = new byte[] { (byte)(-1), (byte)1, (byte)10};
byte[] var12 = new byte[] { (byte)1, (byte)100};
Appointment_Impl var14 = new Appointment_Impl((byte)10, var2, var5, var9, var12, (byte)0);
String var15 = var14.toString();
}
// Class Diagnostic_Impl
public void testGetDescription(){
Diagnostic_Impl var2 = new Diagnostic_Impl((byte)10, (byte)1);
var2.setAppointmentID((byte)0);
byte[] var7 = var2.getDescription((short)1, (short)100);
}
public void testDiagnostic(){
Diagnostic_Impl var2 = new Diagnostic_Impl((byte)(-1), (byte)10);
}
public void testSetAppointmentID(){
Diagnostic_Impl var2 = new Diagnostic_Impl((byte)10, (byte)1);
var2.setAppointmentID((byte)(-1));
}
public void testSetDescription(){
Diagnostic_Impl var2 = new Diagnostic_Impl((byte)10, (byte)1);
var2.setAppointmentID((byte)0);
byte[] var15 = new byte[] { (byte)(-1), (byte)1, (byte)10};
var2.setDescription(var15, (short)10, (short)0, true);
}
// Class Medicine_Impl
public void testMedicine_Impl(){
Medicine_Impl var4 = new Medicine_Impl((byte)100, (byte)(-1), (byte)(-1), (byte)(-1));
}
// Class Personal_Impl
public void testPersonal_Impl(){
Personal_Impl var0 = new Personal_Impl();
}
// Class Treatment_Impl
public void testGetMedicalRecommendation(){
Treatment_Impl var3 = new Treatment_Impl((byte)1, (byte)10, (byte)10);
byte[] var8 = var3.getMedicalRecommendation((short)100, (short)(-1));
}
public void testTreatment_Impl(){
Treatment_Impl var3 = new Treatment_Impl((byte)0, (byte)(-1), (byte)0);
}
public void testSetAppointmentID(){
Treatment_Impl var3 = new Treatment_Impl((byte)0, (byte)100, (byte)0);
var3.setAppointmentID((byte)(-1));
}
public void testSetDiagnosticID(){
Treatment_Impl var3 = new Treatment_Impl((byte)1, (byte)0, (byte)0);
var3.setDiagnosticID((byte)(-1));
}
public void testSetMedicalRecommendation(){
Treatment_Impl var3 = new Treatment_Impl((byte)1, (byte)0, (byte)0);
byte[] var10 = new byte[] { (byte)0, (byte)0};
var3.setMedicalRecommendation(var10, (short)100, (short)3, true);
}
public void testSetTreatmentID(){
Treatment_Impl var3 = new Treatment_Impl((byte)0, (byte)100, (byte)0);
var3.setAppointmentID((byte)100);
var3.setTreatmentID((byte)(-1));
}
// Class Vaccine_Impl
public void testSetDesignation(){
Vaccines_Impl var0 = new Vaccines_Impl();
Treatment_Impl var12 = new Treatment_Impl((byte)1, (byte)0, (byte)0);
byte[] var13 = var12.getHealthProblem();
var0.setVaccineDesignation((short)1, var13);
}
// Class Vaccines_Impl
public void testGetVaccineDesignation(){
Vaccines_Impl var0 = new Vaccines_Impl();
byte[] var2 = var0.getVaccineDesignation((short)10);
}
public void testRemoveVaccine(){
Vaccines_Impl var0 = new Vaccines_Impl();
var0.removeVaccine((short)25601);
}
public void testSetVaccineDesignation(){
Vaccines_Impl var0 = new Vaccines_Impl();
byte[] var11 = new byte[] { (byte)10};
var0.setVaccineDesignation((short)10, var11);
}
public void testValidateVaccinePosition(){
Vaccines_Impl var0 = new Vaccines_Impl();
boolean var1 = var0.validateVaccinePosition((short)(-1));
}
// JAccounting
// Class Account
public void testGetCurrency(){
Account var0 = Account.getDefault();
var0.setId((java.lang.Integer)1);
String var3 = var0.getCurrency();
}
public void testGetDescription(){
Account var0 = new Account();
String var4 = var0.getDescription();
}
public void testGetName(){
Account var0 = new Account();
var0.setDetailTypeKey(0);
String var5 = var0.getName();
}
//Class AClass
public void testAClass(){
AClass var0 = AClass.getDefault();
String var2 = var0.getName();
}
// Class ArrayUtils
public void testGetMaxIntArrayIndex(){
int[] var0 = new int[] { };
int var1 = ArrayUtils.getMaxIntArrayIndex(var0);
}
public void testStringArrayToIntArray(){
String[] var1 = new String[] { ""};
int[] var4 = ArrayUtils.stringArrayToIntArray(var1);
}
// Class mail.ByteArrayDataSource
public void testByteArrayDataSource(){
byte[] var3 = new byte[] { (byte)0};
ByteArrayDataSource var5 = new ByteArrayDataSource(var3, "country_select");
}
// Class util.ByteArrayDataSource
public void testConstructor(){
byte[] var5 = new byte[] { (byte)100};
ByteArrayDataSource var7 = new ByteArrayDataSource(var5, "hi!");
}
// Class Charge
public void testCharge(){
Charge var0 = new Charge();
}
// Class Company
public void testCompany(){
Company var0 = new Company();
var0.setActive(true);
Integer var4 = var0.getId();
}
// Class CookieUtils
public void testGetCookie(){
javax.servlet.http.Cookie var3 = CookieUtils.getCookie("<select name=\"color_select\" id=\"color_select\">\n<option value=\"Black\" style=\"color:Black\">Black\n<option value=\"Maroon\" style=\"color:Maroon\">Maroon\n<option value=\"Green\" style=\"color:Green\">Green\n<option value=\"Olive\" style=\"color:Olive\">Olive\n<option value=\"Navy\" style=\"color:Navy\">Navy\n<option value=\"Purple\" style=\"color:Purple\">Purple\n<option value=\"Teal\" style=\"color:Teal\">Teal\n<option value=\"Gray\" style=\"color:Gray\">Gray\n<option value=\"Silver\" style=\"color:Silver\">Silver\n<option value=\"Red\" style=\"color:Red\">Red\n<option value=\"Lime\" style=\"color:Lime\">Lime\n<option value=\"Yellow\" style=\"color:Yellow\">Yellow\n<option value=\"Blue\" style=\"color:Blue\">Blue\n<option value=\"Fuschia\" style=\"color:Fuschia\">Fuschia\n<option value=\"Aqua\" style=\"color:Aqua\">Aqua\n<option value=\"White\" style=\"color:White\">White\n</select>\n0", "accountKey=0 companyKey=nulljournalEntryKey=0Amount=null memo:null", 2);
}
public void testGetDeleteCookie(){
javax.servlet.http.Cookie var1 = CookieUtils.getDeleteCookie("<select id=\"month_select\" name=\"month_select\">\n<option value=\"0\">January\n<option value=\"1\">February\n<option value=\"2\">March\n<option value=\"3\">April\n<option value=\"4\">May\n<option value=\"5\">June\n<option value=\"6\">July\n<option value=\"7\">August\n<option value=\"8\">September\n<option value=\"9\">October\n<option value=\"10\" SELECTED>November\n<option value=\"11\">December\n</select>\n");
}
// Class CustomerLog
public void testGetCustomerKey(){
CustomerLog var0 = new CustomerLog();
int var4 = var0.getCustomerKey();
}
// Class DateUtils
public void testDateUtils(){
String var1 = DateUtils.monthAsString(100);
}
// Class Mailer (mail)
public void testMailer(){
mail.Mailer var1 = new mail.Mailer("0000000001");
}
// Class Mailer (util)
public void testMailer(){
util.Mailer var1 = new util.Mailer("ByteArrayDataSource");
}
// Class PageElements
public void testPageElements(){
RegisterAction var0 = new RegisterAction();
}
// Class PaymentDistribution
public void testPaymentDistribution(){
PaymentDistribution var0 = new PaymentDistribution();
}
// Class Preferences
public void testPreferences(){
Preferences var0 = new Preferences();
}
// Class Product
public void testProduct(){
Product var0 = Product.getDefault();
}
// Class Recurrence
public void testRecurrence(){
Recurrence var2 = new Recurrence();
}
// Class StringDataSource
public void testStringDataSource(){
StringDataSource var0 = new StringDataSource();
}
// Class Tax
public void testTax(){
Tax var2 = Tax.getDefault();
}
// Mondex
// Class APDU
public void testAPDU(){
APDU var0 = new APDU();
}
// Class ConPurseJC
public void testConPurseJC(){
byte[] var2 = new byte[] { (byte)1, (byte)(-1)};
ConPurseJC.install(var2);
}
// TransactedMemory
// Class AbstractTransactedMemory
public void testANewTag(){
TagToInfoSeqSeqMap var2 = new TagToInfoSeqSeqMap();
TagToInfoSeqSeqMap var3 = new TagToInfoSeqSeqMap();
org.jmlspecs.models.JMLValueToValueRelation var4 = var2.difference((org.jmlspecs.models.JMLValueToValueRelation)var3);
TagToInfoSeqSeqMap var20 = new TagToInfoSeqSeqMap();
org.jmlspecs.models.JMLValueToValueRelation var24 = var2.remove((org.jmlspecs.models.JMLType)var6, (org.jmlspecs.models.JMLType)var20);
TagToInfoSeqSeqMap var25 = new TagToInfoSeqSeqMap();
TagToInfoSeqSeqMap var26 = new TagToInfoSeqSeqMap();
org.jmlspecs.models.JMLValueToValueRelation var27 = var25.difference((org.jmlspecs.models.JMLValueToValueRelation)var26);
TagToInfoSeqSeqMap var29 = new TagToInfoSeqSeqMap();
TagToInfoSeqSeqMap var31 = new TagToInfoSeqSeqMap();
org.jmlspecs.models.JMLValueToValueRelation var33 = var29.difference((org.jmlspecs.models.JMLValueToValueRelation)var31);
org.jmlspecs.models.JMLValueToValueRelationEnumerator var35 = var31.elements();
InfoSeqSeq var37 = new InfoSeqSeq();
org.jmlspecs.models.JMLValueSet var39 = var37.toSet();
org.jmlspecs.models.JMLValueToValueMap var40 = var31.rangeRestrictedTo(var39);
org.jmlspecs.models.JMLValueToValueMap var41 = var25.restrictedTo(var39);
TagToInfoSeqSeqMap var45 = new TagToInfoSeqSeqMap();
InfoSeqSeq var58 = new InfoSeqSeq();
InfoSeqSeq var59 = new InfoSeqSeq();
InfoSeqSeq var62 = new InfoSeqSeq();
org.jmlspecs.models.JMLValueSequence var65 = var59.insertFront((org.jmlspecs.models.JMLType)var62);
org.jmlspecs.models.JMLValueSequence var66 = var58.insertFront((org.jmlspecs.models.JMLType)var62);
InfoSeqSeq var68 = new InfoSeqSeq();
InfoSeqSeq var72 = new InfoSeqSeq();
org.jmlspecs.models.JMLValueSequence var76 = var68.insertFront((org.jmlspecs.models.JMLType)var72);
org.jmlspecs.models.JMLValueSequence var77 = var66.insertAfterIndex(0, (org.jmlspecs.models.JMLType)var68);
org.jmlspecs.models.JMLValueSet var79 = var45.inverseElementImage((org.jmlspecs.models.JMLType)var66);
org.jmlspecs.models.JMLValueToValueRelation var80 = var25.restrictRangeTo(var79);
org.jmlspecs.models.JMLValueToValueMap var81 = var2.disjointUnion((org.jmlspecs.models.JMLValueToValueMap)var25);
org.jmlspecs.models.JMLValueSet var82 = var25.range();
AbstractTransactedMemory var83 = new AbstractTransactedMemory(100, 10, var82);
Tag var85 = var83.ANewTag(100);
}
// Class DPage
public void testDPage(){
DPage var6 = new DPage(true, 0, 100, 1, 1, 100);
}
// Class DTagData
public void testDTagData(){
DTagData var3 = new DTagData(true, (-1), false);
}
// Class Generation
public void testGeneration(){
Generation var1 = new Generation(10);
}
// Class GenGenbyte
public void testGenGenbyte(){
TestFramework.ReallyDTidy();
}
// Class Tag
public void testTag(){
Tag var1 = new Tag(10);
}
// Class Version
public void testVersion(){
Version var1 = new Version(100);
}