Custom query (541 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (201 - 300 of 541)

1 2 3 4 5 6

Status: closed (100 matches)

Ticket Summary Owner Type Priority Component Version
#17102 [anomaly] when pHL => pRHL variant of conseq is used with a bound different from [=1%r] Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17107 Potential mismatch between spec and lemma versions of the "pHL + HL => pHL" variant of [conseq] defect 3 EasyCrypt pre-1.x
#17109 Hoare adversary rule introducess references to non-existent memories in postconditions Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#17110 [anomaly] on using [call] with a lemma referring to the wrong procedure Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17112 `unknown symbol Top.o` when importing a theory including objects referring to `Top.o` Pierre-Yves Strub defect 5 EasyCrypt pre-1.x
#17114 Unsoundness of module system Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#17116 Bad error message for [swap] Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17120 [rnd] allows to prove false Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17122 Clone ignores provided proof Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17123 Bad parsing on call (_: B, I) Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17124 allows to specify timeout only for smt. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17125 Cannot clear variables referring to memory Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17127 Bug in typing of instruction x.[y] = e; Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17128 assert false in rnd. Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17129 bug in alias, the introduced variable has not the good type. Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17132 Unsoundness in definition of "glob M" Pierre-Yves Strub defect 5 EasyCrypt pre-1.x
#17133 seq for phoare do not check the type of the arguments. Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17134 is_lossless F(M).f generate a parse error. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17135 anomaly when intro pattern has wrong form Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17138 "easycrypt -check-all" does not load "Logic" Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17142 Anomaly (related to SMT and memories) Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17143 Anomaly (free type variables in conseq) Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17144 Module type checking: Unclear error message and probably bug Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17145 "choice" reorders its arguments Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17146 Bad error message in combination choice/modules/section Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17147 Parse error in (some) expressions involving memories Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17148 Operators should be subject to section restrictions Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17153 seq does not check type of its arguments Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17154 anomaly: EcPV.MemoryClash defect 3 EasyCrypt pre-1.x
#17155 Fix stdlib w.r.t. why3 import Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17162 Bad interaction between abstract theories and local modules Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17168 Unsoundness: combination of sections, modules, and choice-operators Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17172 Looping on `rewrite !/op` Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17174 Return of the memory explosion defect 3 EasyCrypt pre-1.x
#17177 View application fails non gracely when it cannot instanciate all type variables. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17178 Generalizing over an empty list should generate a sane name Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17180 anomaly: File "src/ecCoreFol.ml", line 1207, characters 19-25: Assertion failed Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17184 parse error involving parameterized module Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17187 anomaly when invalid memory is referenced -- should be proper error message Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17188 Error with smt : lazy defect 3 EasyCrypt pre-1.x
#17190 progress and progress => //. should be equivalent... Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17191 Assert failure Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17193 Obscure failure on lazy smt with higher-order stuff and booleans Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17198 Spurious failure of rewrite Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17199 PG: Default weak-check mode indicator is invalid. Pierre-Yves Strub defect 2 ProofGeneral pre-1.x
#17200 Parse error in required theories are incorrectly located. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17203 Rewrite strangely failling Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17205 New syntax for assignments should be available in immediate definitions Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17206 Missing parens in the pretty printer Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17208 `rewrite ... in ...` Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17211 split causes anomaly when given equality between constructors Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17212 Circular [require] dependencies should be caught instead of blowing up computers Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17213 Retracting/Resetting should cause easycrypt to reload the prelude Pierre-Yves Strub defect 3 ProofGeneral pre-1.x
#17214 Wrong printed for memory Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17216 All test suites should include abstract theory files (*.eca) defect 3 Internals pre-1.x
#17219 operators don't print the way they are declared Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17223 use of ' and ` in operator names causes anomaly rather than error message Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17224 type declarations with bad type variables yield anomalies rather than error messages Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17226 some weirdness with operators of form :+ Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17228 pretty printer uses bad syntax for type constructors Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17229 pretty printer errors with inductive datatypes Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17233 pretty printing issues with _?_:_ and modules Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17235 rewrite ... in ... should allow rewriting in uident not just lident Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17236 error with rewriting occurrence of -1 when only one matching occurrence defect 3 EasyCrypt pre-1.x
#17237 failure of rewrite ... in ... Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17238 anomaly with auto-revert intro pattern Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17241 `clone import` not working when realizing axioms. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17243 Internal error (anomaly) on proof script Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17244 Imprecise "uninitialized local variables" warning Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17252 The `seq` variant documented as pHL is in fact the HL tactic. Alley Stoughton defect 3 Documentation pre-1.x
#17254 print produces misleading results on partially applied functors defect 3 EasyCrypt pre-1.x
#17260 pragma +option should fail gracefully. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17272 Wrong name defect 3 EasyCrypt pre-1.x
#17273 `alias` failures look like uncaught exceptions defect 3 EasyCrypt pre-1.x
#17274 Collision in names, local variables unreachable Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17275 [congr] should apply to iff Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17276 the pretty printer is getting the relative precedences of unary - and %% wrong Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17277 Higher-order pattern-matching with quantifiers Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17278 [eta] reduction is not full on multi-ary functions github <noreply@…> defect 3 EasyCrypt pre-1.x
#17289 Missing dependencies in OPAM package defect 3 EasyCrypt pre-1.x
#17291 `move: x` should keep the body of `x` if any. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17292 anomaly on application of a `<=>` lemma to a `=` goal defect 3 EasyCrypt pre-1.x
#17293 Looping behaviour in reduction/simplification. Probably related to reals. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17294 `Self` (and `Top`) should be allowed in module restrictions Pierre-Yves Strub defect 1 EasyCrypt pre-1.x
#17296 Some program tactics (`rnd`) generate invalid formulas when Distr is not loaded defect 3 EasyCrypt pre-1.x
#17300 Module type checks have wrong variance when dealing with some functor configurations Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17302 fel can generate subgoal with undefined memory Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17303 more fel peculiarities Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17304 Regression on anonymous procedure arguments support Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17306 Operator folding and unfolding not checking type parameters Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17312 cloning can create ill-formed definitions Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17313 module types with multiple occurrences of same procedure should not be accepted Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17315 [print] on notations is not very useful defect 3 EasyCrypt pre-1.x
#17318 clone-time regexp substitution should apply in the specified order Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17320 anomaly when cloning theory with inductive predicate Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17323 |> ip anomaly Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17324 |> ip expands predicates in conclusion Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17326 `+` intro-pattern may reorder assumptions Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17329 EasyCrypt output (goals order e.g.) is not stable Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17330 anomaly on `apply/contra` Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
(more results for this group on next page)
1 2 3 4 5 6
Note: See TracQuery for help on using queries.