#35 Location_Linking_Test Verifier RTE
Currently compiling: Location_Linking_Test.fa
Current compile environment: ============================================================
Compilation environment for Location_Linking_Test.fa
============================================================
Main directory: Main
------------------------------------------------------------
Unparsable files: ( )
Compile stack: ( Location_Linking_Test, Location_Linking_Template_1.Std_Location_Linking_Realiz )
Static_Array_Template is complete.
Theories: ( Boolean_Theory, Integer_Theory, Set_Theory, Modified_String_Theory )
Integer_Theory is complete.
Theories: ( Boolean_Theory, Set_Theory )
Location_Linking_Test is complete.
Theories: ( Boolean_Theory, Integer_Theory, Set_Theory, Modified_String_Theory )
Character_Template is complete.
Theories: ( Boolean_Theory, Integer_Theory, Set_Theory )
Std_Char_Str_Fac is complete.
Theories: ( Boolean_Theory, Integer_Theory, Set_Theory, Modified_String_Theory )
Boolean_Template is complete.
Theories: ( Boolean_Theory )
Modified_String_Theory is complete.
Theories: ( Boolean_Theory, Integer_Theory, Set_Theory )
Char_Str_Template is complete.
Theories: ( Boolean_Theory, Integer_Theory, Set_Theory, Modified_String_Theory )
Location_Linking_Template_1 is complete.
Theories: ( Boolean_Theory, Integer_Theory, Set_Theory, Modified_String_Theory )
Integer_Template is complete.
Theories: ( Boolean_Theory, Integer_Theory, Set_Theory )
Location_Linking_Template_1.Std_Location_Linking_Realiz is incomplete.
Theories: ( )
Std_Boolean_Fac is complete.
Theories: ( Boolean_Theory )
Boolean_Theory is complete.
Theories: ( )
Std_Character_Fac is complete.
Theories: ( Boolean_Theory, Integer_Theory, Set_Theory )
Std_Integer_Fac is complete.
Theories: ( Boolean_Theory, Integer_Theory, Set_Theory )
Set_Theory is complete.
Theories: ( Boolean_Theory )
------------------------------------------------------------
Unexpected exception: java.lang.RuntimeException
java.lang.RuntimeException
at edu.clemson.cs.r2jt.absyn.Exp.copy(Exp.java:272)
at edu.clemson.cs.r2jt.absyn.AltItemExp.copy(AltItemExp.java:292)
at edu.clemson.cs.r2jt.absyn.AlternativeExp.copy(AlternativeExp.java:274)
at edu.clemson.cs.r2jt.absyn.LambdaExp.copy(LambdaExp.java:270)
at edu.clemson.cs.r2jt.absyn.LambdaExp.replace(LambdaExp.java:232)
at edu.clemson.cs.r2jt.absyn.EqualsExp.replace(EqualsExp.java:298)
at edu.clemson.cs.r2jt.absyn.InfixExp.replace(InfixExp.java:755)
at edu.clemson.cs.r2jt.absyn.InfixExp.replace(InfixExp.java:754)
at edu.clemson.cs.r2jt.absyn.InfixExp.replace(InfixExp.java:755)
at edu.clemson.cs.r2jt.absyn.InfixExp.replace(InfixExp.java:755)
at edu.clemson.cs.r2jt.absyn.InfixExp.replace(InfixExp.java:755)
at edu.clemson.cs.r2jt.absyn.InfixExp.replace(InfixExp.java:755)
at edu.clemson.cs.r2jt.absyn.InfixExp.replace(InfixExp.java:755)
at edu.clemson.cs.r2jt.absyn.InfixExp.replace(InfixExp.java:755)
at edu.clemson.cs.r2jt.absyn.InfixExp.replace(InfixExp.java:755)
at edu.clemson.cs.r2jt.absyn.InfixExp.replace(InfixExp.java:755)
at edu.clemson.cs.r2jt.absyn.InfixExp.replace(InfixExp.java:755)
at edu.clemson.cs.r2jt.absyn.InfixExp.replace(InfixExp.java:755)
at edu.clemson.cs.r2jt.absyn.InfixExp.replace(InfixExp.java:755)
at edu.clemson.cs.r2jt.absyn.InfixExp.replace(InfixExp.java:755)
at edu.clemson.cs.r2jt.absyn.InfixExp.replace(InfixExp.java:755)
at edu.clemson.cs.r2jt.absyn.InfixExp.replace(InfixExp.java:755)
at edu.clemson.cs.r2jt.absyn.InfixExp.replace(InfixExp.java:755)
at edu.clemson.cs.r2jt.absyn.InfixExp.replace(InfixExp.java:755)
at edu.clemson.cs.r2jt.absyn.InfixExp.replace(InfixExp.java:755)
at edu.clemson.cs.r2jt.verification.Verifier.applyEBFuncAssignStmtRule(Verifier.java:833)
at edu.clemson.cs.r2jt.verification.Verifier.applyProofRulesToAssertiveCode(Verifier.java:1340)
at edu.clemson.cs.r2jt.verification.Verifier.visitEBCodeRule(Verifier.java:6491)
at edu.clemson.cs.r2jt.verification.Verifier.applyEBRules(Verifier.java:856)
at edu.clemson.cs.r2jt.verification.Verifier.applyPartOneWhileRule(Verifier.java:1239)
at edu.clemson.cs.r2jt.verification.Verifier.applyEBWhileRuleStmt(Verifier.java:982)
at edu.clemson.cs.r2jt.verification.Verifier.applyProofRulesToAssertiveCode(Verifier.java:1357)
at edu.clemson.cs.r2jt.verification.Verifier.visitEBCodeRule(Verifier.java:6491)
at edu.clemson.cs.r2jt.verification.Verifier.applyEBRules(Verifier.java:856)
at edu.clemson.cs.r2jt.verification.Verifier.visitFacilityOperationDec(Verifier.java:7027)
at edu.clemson.cs.r2jt.verification.Verifier.visitProcedures(Verifier.java:7455)
at edu.clemson.cs.r2jt.verification.Verifier.visitFacilityModuleDec(Verifier.java:6783)
at edu.clemson.cs.r2jt.absyn.FacilityModuleDec.accept(FacilityModuleDec.java:155)
at edu.clemson.cs.r2jt.verification.Verifier.visitModuleDec(Verifier.java:7066)
at edu.clemson.cs.r2jt.init.Controller.verifyModuleDec(Controller.java:1228)
at edu.clemson.cs.r2jt.init.Controller.compileNewTargetSource(Controller.java:515)
at edu.clemson.cs.r2jt.init.Controller.compileTargetSource(Controller.java:221)
at edu.clemson.cs.r2jt.Main.compileMainSource(Main.java:369)
at edu.clemson.cs.r2jt.Main.compileFiles(Main.java:328)
at edu.clemson.cs.r2jt.Main.runMain(Main.java:275)
at edu.clemson.cs.r2jt.ResolveCompiler.compile(ResolveCompiler.java:95)
at webui.core.WebCompiler.generateVcs(WebCompiler.java:493)
at webui.core.WebCompiler.processRequest(WebCompiler.java:256)
at webui.core.WebCompiler.doPost(WebCompiler.java:1173)
at javax.servlet.http.HttpServlet.service(HttpServlet.java:637)
at javax.servlet.http.HttpServlet.service(HttpServlet.java:717)
at org.apache.catalina.core.ApplicationFilterChain.internalDoFilter(ApplicationFilterChain.java:290)
at org.apache.catalina.core.ApplicationFilterChain.doFilter(ApplicationFilterChain.java:206)
at org.apache.catalina.core.StandardWrapperValve.invoke(StandardWrapperValve.java:233)
at org.apache.catalina.core.StandardContextValve.invoke(StandardContextValve.java:191)
at org.apache.catalina.core.StandardHostValve.invoke(StandardHostValve.java:127)
at org.apache.catalina.valves.ErrorReportValve.invoke(ErrorReportValve.java:102)
at org.apache.catalina.core.StandardEngineValve.invoke(StandardEngineValve.java:109)
at org.apache.catalina.connector.CoyoteAdapter.service(CoyoteAdapter.java:300)
at org.apache.coyote.http11.Http11Processor.process(Http11Processor.java:859)
at org.apache.coyote.http11.Http11Protocol$Http11ConnectionHandler.process(Http11Protocol.java:588)
at org.apache.tomcat.util.net.JIoEndpoint$Worker.run(JIoEndpoint.java:489)
at java.lang.Thread.run(Thread.java:679)
java.lang.RuntimeException
Please contact: Reusable Software Research Group
murali@cs.clemson.edu
Developed at Department of Computer Science
Clemson University, Clemson SC USA 29634
Version 2011.1.18