/*

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);

}