search

FormalADL / kAADL

1 stars 1 forks source link

some internal errors while " krun filename.k " #1

Closed suweining closed 9 years ago

suweining commented 9 years ago

today I modify the AADL.k(syntax of aadl) to eliminate the ambiguty：

 - syntax PkgDeclations ::= AADLDeclList 
 -                                       | NameVisDeclList 
 -                                       | PkgDeclations PkgDeclations
 + syntax PkgDeclations ::= AADLDeclList 
 +                                       | NameVisDeclList
 +                                       | AADLDeclList PkgDeclations 
 +                                       | NameVisDeclList PkgDeclations

Before modifying,the AADL.k can anlysis Ports.k ,but now it is wrong while "krun tests/unit/Ports.aadl".Here error massage:

Exception in thread "main" java.lang.AssertionError: The greatest lower bound (GLB) of sorts [ArrayElementImplList, PpeListValue, UnitsList, BooleanTerm]doesn't exist!

at org.kframework.backend.java.kil.KItem.<init>(KItem.java:190)
at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.visit(KILtoBackendJavaKILTransformer.java:159)

.....

at org.kframework.kil.AbstractVisitor.visitNode(AbstractVisitor.java:92)
at org.kframework.backend.java.symbolic.KILtoBackendJavaKILTransformer.transformTerm(KILtoBackendJavaKILTransformer.java:128)
at org.kframework.backend.java.kil.Term.of(Term.java:49)
at org.kframework.backend.java.symbolic.JavaSymbolicKRun.javaKILRun(JavaSymbolicKRun.java:97)
at org.kframework.backend.java.symbolic.JavaSymbolicKRun.internalRun(JavaSymbolicKRun.java:82)
at org.kframework.backend.java.symbolic.JavaSymbolicKRun.run(JavaSymbolicKRun.java:77)
at org.kframework.krun.Main.normalExecution(Main.java:370)
at org.kframework.krun.Main.execute_Krun(Main.java:1452)
at org.kframework.main.Main.main(Main.java:64)
suweining commented 9 years ago

I try to compile the AADL.k by " kompile --backend java AADL.k ",and this error still appear .While I use this command,"kompile AADL.k",to complie the AADL.k,the "krun tests/unit/Ports.aadl" is OK ! So ,I consider whether the java client is not stable .

suweining commented 9 years ago

I try using command "krun --backend java /tests/unit/Ports.aadl" to analyze the Ports.aadl . Same errors appeares again .