-
Notifications
You must be signed in to change notification settings - Fork 36
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
any/choosein a match arm that mentions a pattern variable fails an assertion in lustreGenNodescomp:frontendLustre parsing, type checking, normalization, desugaring, and translation to transition systemsLustre parsing, type checking, normalization, desugaring, and translation to transition systemsimpact:crashInternal error, assertion failure, exception or segfault instead of a resultInternal error, assertion failure, exception or segfault instead of a resultlang:matchPattern matching: match expressions and patternsPattern matching: match expressions and patternsstatus:triageNew; not yet reviewed by a maintainerNew; not yet reviewed by a maintainerStatus: Open.#1546 In kind2-mc/kind2;An if-then-else checked against an expected type is never compared with it: ill-typed properties and constants are accepted
comp:frontendLustre parsing, type checking, normalization, desugaring, and translation to transition systemsLustre parsing, type checking, normalization, desugaring, and translation to transition systemsimpact:accepts-invalidA malformed program passes a check it should failA malformed program passes a check it should failimpact:crashInternal error, assertion failure, exception or segfault instead of a resultInternal error, assertion failure, exception or segfault instead of a resultimpact:soundnessCan report a property valid when it is notCan report a property valid when it is notstatus:triageNew; not yet reviewed by a maintainerNew; not yet reviewed by a maintainerStatus: Open.#1545 In kind2-mc/kind2;A map literal with an expression list as its value builds a map whose type cannot be written
comp:frontendLustre parsing, type checking, normalization, desugaring, and translation to transition systemsLustre parsing, type checking, normalization, desugaring, and translation to transition systemslang:mapMaps: map types, literals, element updates, and lookupsMaps: map types, literals, element updates, and lookupsneeds:designNeeds a design decision before work can startNeeds a design decision before work can startstatus:triageNew; not yet reviewed by a maintainerNew; not yet reviewed by a maintainerStatus: Open.#1543 In kind2-mc/kind2;Polymorphic recursive function crashes with SIGSEGV; the generic declaration is instantiated twice
comp:frontendLustre parsing, type checking, normalization, desugaring, and translation to transition systemsLustre parsing, type checking, normalization, desugaring, and translation to transition systemsimpact:crashInternal error, assertion failure, exception or segfault instead of a resultInternal error, assertion failure, exception or segfault instead of a resultlang:polymorphismType parameters: polymorphic nodes, functions, contracts, and datatypesType parameters: polymorphic nodes, functions, contracts, and datatypeslang:rec-functionRecursive functions (function rec) and decreases measuresRecursive functions (function rec) and decreases measuresstatus:triageNew; not yet reviewed by a maintainerNew; not yet reviewed by a maintainerStatus: Open.Cycle through an if/when-block condition inside a callee is not detected: node summary drops branch conditions
comp:frontendLustre parsing, type checking, normalization, desugaring, and translation to transition systemsLustre parsing, type checking, normalization, desugaring, and translation to transition systemsimpact:accepts-invalidA malformed program passes a check it should failA malformed program passes a check it should failimpact:soundnessCan report a property valid when it is notCan report a property valid when it is notstatus:triageNew; not yet reviewed by a maintainerNew; not yet reviewed by a maintainerStatus: Open.Match pattern variable shadowing a global constant reads the constant when used under pre
comp:frontendLustre parsing, type checking, normalization, desugaring, and translation to transition systemsLustre parsing, type checking, normalization, desugaring, and translation to transition systemsimpact:soundnessCan report a property valid when it is notCan report a property valid when it is notlang:matchPattern matching: match expressions and patternsPattern matching: match expressions and patternsstatus:triageNew; not yet reviewed by a maintainerNew; not yet reviewed by a maintainerStatus: Open.condact in a when block branch fails an assertion in lustreTransSys
comp:frontendLustre parsing, type checking, normalization, desugaring, and translation to transition systemsLustre parsing, type checking, normalization, desugaring, and translation to transition systemsimpact:crashInternal error, assertion failure, exception or segfault instead of a resultInternal error, assertion failure, exception or segfault instead of a resultlang:clockClocks and clocked constructs: when, merge, current, condact, activate, when-blocksClocks and clocked constructs: when, merge, current, condact, activate, when-blocksstatus:triageNew; not yet reviewed by a maintainerNew; not yet reviewed by a maintainerStatus: Open.Type synonym for a recursive datatype declares the SMT sort twice: "sort already defined"
comp:frontendLustre parsing, type checking, normalization, desugaring, and translation to transition systemsLustre parsing, type checking, normalization, desugaring, and translation to transition systemsimpact:crashInternal error, assertion failure, exception or segfault instead of a resultInternal error, assertion failure, exception or segfault instead of a resultlang:datatypeAlgebraic datatypes (datatype declarations), constructors, testers, selectorsAlgebraic datatypes (datatype declarations), constructors, testers, selectorsstatus:triageNew; not yet reviewed by a maintainerNew; not yet reviewed by a maintainerStatus: Open.Mixing
a[i] = ...anda = ...across branches of an if/when block raises Invalid_argument("Trie.map2")comp:frontendLustre parsing, type checking, normalization, desugaring, and translation to transition systemsLustre parsing, type checking, normalization, desugaring, and translation to transition systemsimpact:crashInternal error, assertion failure, exception or segfault instead of a resultInternal error, assertion failure, exception or segfault instead of a resultlang:arrayArrays: recursive array definitions, element updates, selectsArrays: recursive array definitions, element updates, selectsstatus:triageNew; not yet reviewed by a maintainerNew; not yet reviewed by a maintainerStatus: Open.Temporal match-arm expression is driven by the base clock, not the arm's, when it mentions a pattern variable
comp:frontendLustre parsing, type checking, normalization, desugaring, and translation to transition systemsLustre parsing, type checking, normalization, desugaring, and translation to transition systemsimpact:soundnessCan report a property valid when it is notCan report a property valid when it is notlang:clockClocks and clocked constructs: when, merge, current, condact, activate, when-blocksClocks and clocked constructs: when, merge, current, condact, activate, when-blockslang:matchPattern matching: match expressions and patternsPattern matching: match expressions and patternsstatus:triageNew; not yet reviewed by a maintainerNew; not yet reviewed by a maintainerStatus: Open.Program from --minimize_program valid_lustre does not parse: generated __rand node is opaque without a contract
comp:ivc-mcsInductive validity cores, minimal cut sets, and program minimization (ivcMcs)Inductive validity cores, minimal cut sets, and program minimization (ivcMcs)comp:outputReporting results: text, JSON, and XML output, counterexamples, tracesReporting results: text, JSON, and XML output, counterexamples, tracesimpact:wrong-resultWrong but visible answer: spurious counterexample, wrong trace or valueWrong but visible answer: spurious counterexample, wrong trace or valuestatus:triageNew; not yet reviewed by a maintainerNew; not yet reviewed by a maintainerStatus: Open.Structural
decreasesaccepts only a pattern-bound variable, not a selector applied to onecomp:frontendLustre parsing, type checking, normalization, desugaring, and translation to transition systemsLustre parsing, type checking, normalization, desugaring, and translation to transition systemslang:datatypeAlgebraic datatypes (datatype declarations), constructors, testers, selectorsAlgebraic datatypes (datatype declarations), constructors, testers, selectorslang:rec-functionRecursive functions (function rec) and decreases measuresRecursive functions (function rec) and decreases measuresStatus: Open.