#34 Write_Line operation not found by verifier (NPE)

[Chuck Cook]

Currently compiling: Alt_Rev_Stack.fa
Current compile environment: ============================================================
Compilation environment for Alt_Rev_Stack.fa
============================================================
Main directory: Main
------------------------------------------------------------
Unparsable files: ( )
Compile stack: ( Alt_Rev_Stack )
Static_Array_Template is complete.
Theories: ( Boolean_Theory, Integer_Theory, Set_Theory, Modified_String_Theory )
Integer_Theory is complete.
Theories: ( Boolean_Theory, Set_Theory )
Stack_Template.Obvious_Reading_Realiz is complete.
Theories: ( Boolean_Theory, Integer_Theory, Set_Theory, Modified_String_Theory )
Stack_Template.Reading_Capability 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 )
Stack_Template.Array_Realiz 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 )
Stack_Template.Writing_Capability is complete.
Theories: ( Boolean_Theory, Integer_Theory, Set_Theory, Modified_String_Theory )
Alt_Rev_Stack 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 )
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 )
Stack_Template.Obvious_Writing_Realiz is complete.
Theories: ( Boolean_Theory, Integer_Theory, Set_Theory, Modified_String_Theory )
Std_Integer_Fac is complete.
Theories: ( Boolean_Theory, Integer_Theory, Set_Theory )
Static_Array_Template.Std_Array_Realiz is incomplete.
Theories: ( )
Stack_Template is complete.
Theories: ( Boolean_Theory, Integer_Theory, Set_Theory, Modified_String_Theory )
Set_Theory is complete.
Theories: ( Boolean_Theory )
------------------------------------------------------------

Unexpected exception: java.lang.RuntimeException: Error passed operation not found: Write_Line

java.lang.RuntimeException: Error passed operation not found: Write_Line

at edu.clemson.cs.r2jt.verification.Verifier.applyEBCallStmtRule(Verifier.java:607)
at edu.clemson.cs.r2jt.verification.Verifier.applyProofRulesToAssertiveCode(Verifier.java:1344)
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: Error passed operation not found: Write_Line

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

[Yu-Shan Sun]

Will wait until the new Symbol Table is implemented to fix it. We should be able to extract the Operation easily then.