-
Notifications
You must be signed in to change notification settings - Fork 25
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
CSV Statistics Export: Ambiguous Usage of Comma #1533
Labels
Comments
JonasKlamroth
added a commit
to JonasKlamroth/key
that referenced
this issue
Feb 21, 2024
wadoon
pushed a commit
to JonasKlamroth/key
that referenced
this issue
Feb 23, 2024
wadoon
added a commit
to wadoon/key
that referenced
this issue
Mar 10, 2024
# By Drodt (57) and others # Via GitHub (17) and others * origin/main: (147 commits) Merge main into extraxt-new-core fixes KeYProject#1533 added checkbox to disable example loader directly in dialog address reviewer comments: set border + spotless + typo JML enabled keys indicator for the status line add test case for adt taclets Fix position info for equality expr errors Revert debugging code Spotless Add ADT Deconstructors Moved TestSMTMod to newsmt2 spotless applied to TestSMTMod Added test for Modulo Translation Added translation from KeY mod to SMT mod. Soundness derived from translation of KeY div to SMT div preventing NPEs in overloaded operators added test cases for operator overloading activate the OverloadedOperatorHandler.java for LocSet datatype and repair translation Bump ch.qos.logback:logback-classic from 1.4.14 to 1.5.0 Update README.md (license date and Java version) ... # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java # key.core/src/main/java/de/uka/ilkd/key/settings/GeneralSettings.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLConstruct.java # key.ui/build.gradle # keyext.caching/src/test/java/de/uka/ilkd/key/proof/reference/TestReferenceSearcher.java
wadoon
added a commit
that referenced
this issue
Mar 14, 2024
# By Drodt (57) and others # Via GitHub (26) and others * origin/main: (158 commits) ColorSettings: drop old configuration file format Merge main into extraxt-new-core Bump ch.qos.logback:logback-classic from 1.5.0 to 1.5.3 fixes #1533 added checkbox to disable example loader directly in dialog address reviewer comments: set border + spotless + typo JML enabled keys indicator for the status line add test case for adt taclets Fix position info for equality expr errors Revert debugging code Spotless Add ADT Deconstructors Moved TestSMTMod to newsmt2 spotless applied to TestSMTMod Added test for Modulo Translation Added translation from KeY mod to SMT mod. Soundness derived from translation of KeY div to SMT div preventing NPEs in overloaded operators added test cases for operator overloading activate the OverloadedOperatorHandler.java for LocSet datatype and repair translation ... # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/logic/op/LocationVariable.java # key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java # key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FieldTypeToSortCondition.java # key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticFieldCondition.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java
wadoon
added a commit
to wadoon/key
that referenced
this issue
Mar 16, 2024
* main: (149 commits) ColorSettings: drop old configuration file format Merge main into extraxt-new-core Bump ch.qos.logback:logback-classic from 1.5.0 to 1.5.3 fixes KeYProject#1533 added checkbox to disable example loader directly in dialog address reviewer comments: set border + spotless + typo JML enabled keys indicator for the status line add test case for adt taclets Fix position info for equality expr errors Revert debugging code Spotless Add ADT Deconstructors Moved TestSMTMod to newsmt2 spotless applied to TestSMTMod Added test for Modulo Translation Added translation from KeY mod to SMT mod. Soundness derived from translation of KeY div to SMT div preventing NPEs in overloaded operators added test cases for operator overloading activate the OverloadedOperatorHandler.java for LocSet datatype and repair translation ... # Conflicts: # key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/AbstractSideProofRule.java # key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java # key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java # key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java # key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelManager.java # key.core/src/main/java/de/uka/ilkd/key/pp/AbbrevMap.java # key.core/src/main/java/de/uka/ilkd/key/proof/Statistics.java # key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java # key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java # key.core/src/main/java/de/uka/ilkd/key/proof/io/intermediate/MergeAppIntermediate.java # key.core/src/main/java/de/uka/ilkd/key/proof/io/intermediate/MergePartnerAppIntermediate.java # key.core/src/main/java/de/uka/ilkd/key/proof/io/intermediate/SMTAppIntermediate.java # key.core/src/main/java/de/uka/ilkd/key/proof/io/intermediate/TacletAppIntermediate.java # key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java # key.core/src/main/java/de/uka/ilkd/key/rule/ObserverToUpdateRule.java # key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java # key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRule.java # key.core/src/main/java/de/uka/ilkd/key/rule/merge/procedures/MergeByIfThenElse.java # key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java # key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/DefinedSymbolsHandler.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java # key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlIO.java # key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java # key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java # key.core/src/main/java/de/uka/ilkd/key/util/mergerule/SymbolicExecutionState.java # key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java # key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java # key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java # key.ui/src/main/java/de/uka/ilkd/key/gui/mergerule/MergeProcedureCompletion.java # keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java # keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java # keyext.slicing/src/main/java/org/key_project/slicing/ui/ShowNodeInfoAction.java # keyext.slicing/src/test/java/org/key_project/slicing/DependencyGraphTest.java
wadoon
added a commit
that referenced
this issue
Mar 17, 2024
# By Drodt (57) and others # Via GitHub (25) and others * origin/main: (157 commits) ColorSettings: drop old configuration file format Merge main into extraxt-new-core Bump ch.qos.logback:logback-classic from 1.5.0 to 1.5.3 fixes #1533 added checkbox to disable example loader directly in dialog address reviewer comments: set border + spotless + typo JML enabled keys indicator for the status line add test case for adt taclets Fix position info for equality expr errors Revert debugging code Spotless Add ADT Deconstructors Moved TestSMTMod to newsmt2 spotless applied to TestSMTMod Added test for Modulo Translation Added translation from KeY mod to SMT mod. Soundness derived from translation of KeY div to SMT div preventing NPEs in overloaded operators added test cases for operator overloading activate the OverloadedOperatorHandler.java for LocSet datatype and repair translation ... # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/logic/sort/AbstractSort.java # key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java # key.core/src/main/java/de/uka/ilkd/key/logic/sort/Sort.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java # key.core/src/test/java/de/uka/ilkd/key/parser/TestDeclParser.java
wadoon
added a commit
that referenced
this issue
Mar 17, 2024
# By Drodt (57) and others # Via GitHub (9) and others * main: (103 commits) ColorSettings: drop old configuration file format Merge main into extraxt-new-core Bump ch.qos.logback:logback-classic from 1.5.0 to 1.5.3 fixes #1533 added checkbox to disable example loader directly in dialog address reviewer comments: set border + spotless + typo JML enabled keys indicator for the status line add test case for adt taclets Fix position info for equality expr errors Revert debugging code Spotless Add ADT Deconstructors Moved TestSMTMod to newsmt2 spotless applied to TestSMTMod Added test for Modulo Translation Added translation from KeY mod to SMT mod. Soundness derived from translation of KeY div to SMT div Document ncore Fix merge import errors Fix merge errors ... # Conflicts: # key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ClassAxiomAndInvariantProofReferencesAnalyst.java # key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionAuxiliaryContract.java # key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleInvariantTranslator.java # key.core/build.gradle # key.core/src/main/java/de/uka/ilkd/key/informationflow/po/BlockExecutionPO.java # key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowContractPO.java # key.core/src/main/java/de/uka/ilkd/key/informationflow/po/LoopInvExecutionPO.java # key.core/src/main/java/de/uka/ilkd/key/informationflow/po/SymbolicExecutionPO.java # key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/TwoStateMethodPredicateSnippet.java # key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/BlockInfFlowUnfoldTacletBuilder.java # key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowBlockContractTacletBuilder.java # key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowLoopInvariantTacletBuilder.java # key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/LoopInfFlowUnfoldTacletBuilder.java # key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java # key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java # key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java # key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYTypeConverter.java # key.core/src/main/java/de/uka/ilkd/key/java/Services.java # key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/KeYJavaType.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/Literal.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/DLEmbeddedExpression.java # key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/EmptyMapLiteral.java # key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/FreeLiteral.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java # key.core/src/main/java/de/uka/ilkd/key/ldt/BooleanLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/CharListLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/DoubleLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/FloatLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/FreeLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/HeapLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/IntegerLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/LDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/LocSetLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/MapLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/PermissionLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/RealLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/SeqLDT.java # key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java # key.core/src/main/java/de/uka/ilkd/key/logic/op/IProgramVariable.java # key.core/src/main/java/de/uka/ilkd/key/logic/op/LocationVariable.java # key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramConstant.java # key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java # key.core/src/main/java/de/uka/ilkd/key/logic/sort/ArraySort.java # key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java # key.core/src/main/java/de/uka/ilkd/key/macros/AbstractBlastingMacro.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java # key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java # key.core/src/main/java/de/uka/ilkd/key/pp/SelectPrinter.java # key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java # key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/DependencyContractPO.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java # key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java # key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java # key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java # key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopContractRule.java # key.core/src/main/java/de/uka/ilkd/key/rule/ObserverToUpdateRule.java # key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java # key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java # key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java # key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRuleBuiltInRuleApp.java # key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ArrayPostDecl.java # key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ConstantValue.java # key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ConstructorCall.java # key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnhancedForElimination.java # key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnumConstantValue.java # key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/MethodCall.java # key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/MultipleVarDecl.java # key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ObserverEqualityMetaConstruct.java # key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SpecialConstructorCall.java # key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java # key.core/src/main/java/de/uka/ilkd/key/smt/SMTObjTranslator.java # key.core/src/main/java/de/uka/ilkd/key/smt/hierarchy/TypeHierarchy.java # key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/FieldConstantHandler.java # key.core/src/main/java/de/uka/ilkd/key/speclang/ClassAxiomImpl.java # key.core/src/main/java/de/uka/ilkd/key/speclang/ClassWellDefinedness.java # key.core/src/main/java/de/uka/ilkd/key/speclang/ContractAxiom.java # key.core/src/main/java/de/uka/ilkd/key/speclang/MethodWellDefinedness.java # key.core/src/main/java/de/uka/ilkd/key/speclang/RepresentsAxiom.java # key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java # key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java # key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLExpression.java # key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLMethodResolver.java # key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLParameters.java # key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLTranslationException.java # key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/TacletProofObligationInput.java # key.core/src/test/java/de/uka/ilkd/key/java/visitor/TestDeclarationProgramVariableCollector.java # key.core/src/test/java/de/uka/ilkd/key/logic/TestTerm.java # key.core/src/test/java/de/uka/ilkd/key/logic/TestTermFactory.java # key.core/src/test/java/de/uka/ilkd/key/rule/TacletForTests.java # key.core/src/test/java/de/uka/ilkd/key/speclang/njml/ClasslevelTranslatorTest.java # key.core/src/test/java/de/uka/ilkd/key/speclang/njml/ExpressionTranslatorTest.java # key.ui/build.gradle # key.ui/src/main/java/de/uka/ilkd/key/gui/ProofManagementDialog.java
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Labels
This issue was created at git.key-project.org where the discussions are preserved.
When saving the proof statistics as CSV, a comma is used for separating columns, but also as thousands separator, as in
Total rule apps,2,965
It would be advantageous to use, e.g., semicolons instead as columns separator.
Also, the first line in
of class ConsoleUserInterface seems superfluous.
I git-blamed (at)mkirsten for this, at least for ConsoleUserInterface ;) Cheers!
Information:
The text was updated successfully, but these errors were encountered: