|
|
|
@49634
|
12 months |
busenius |
Happy new year
|
|
|
|
@49620
|
12 months |
busenius |
Fixed JavaDco? warnings
|
|
|
|
@49619
|
12 months |
busenius |
Updated eclipse config
|
|
|
|
@49606
|
12 months |
busenius |
Better wording of NEWS
|
|
|
|
@49605
|
12 months |
busenius |
Version bump
|
|
|
|
@49604
|
12 months |
busenius |
Released Expi2Java 1.6
|
|
|
|
@49592
|
12 months |
busenius |
Updated NEWS
|
|
|
|
@46133
|
15 months |
busenius |
Fixed style (for real now)
|
|
|
|
@46132
|
15 months |
busenius |
Fixed style
|
|
|
|
@46131
|
15 months |
busenius |
Fixed style
|
|
|
|
@46129
|
15 months |
busenius |
Fixed TeX errors
|
|
|
|
@41029
|
19 months |
busenius |
Using a hand-made version of Semaphore in symbolic library (compatible to …
|
|
|
|
@32016
|
2 years |
busenius |
Added some CryptoVerif? keywords to Vim highlighting script
|
|
|
|
@26701
|
2 years |
busenius |
Made KeyPair? contravariant again
|
|
|
|
@26700
|
2 years |
busenius |
Switched to invariant SymEnc?, PubEnc?, Signed, Hash and KeyPair? to prevent …
|
|
|
|
@26699
|
2 years |
busenius |
Ignoring unhelpful X <: Top constraints
|
|
|
|
@26698
|
2 years |
busenius |
Improved type inference for invariant types, using a single lower/upper …
|
|
|
|
@26697
|
2 years |
busenius |
Exiting with error code on errors
|
|
|
|
@26696
|
2 years |
busenius |
Improved type inference for invariant types
|
|
|
|
@26612
|
2 years |
busenius |
More debug output
|
|
|
|
@25624
|
3 years |
busenius |
Fixed some stuff
Removed some debug printfs
|
|
|
|
@25623
|
3 years |
busenius |
FIXME--
|
|
|
|
@25622
|
3 years |
busenius |
Added another test case for destructor consistency
|
|
|
|
@25507
|
3 years |
busenius |
Small fix
|
|
|
|
@25506
|
3 years |
busenius |
Added consistency check log for default.exdef
|
|
|
|
@25505
|
3 years |
busenius |
Small fix
|
|
|
|
@25405
|
3 years |
busenius |
Added simple runtime estimation for consistency checking
|
|
|
|
@25404
|
3 years |
busenius |
Added core-consistency.log
|
|
|
|
@25403
|
3 years |
busenius |
Added a log with destructor consistency checking results
|
|
|
|
@25402
|
3 years |
busenius |
Updated destructor consistency testcases
|
|
|
|
@25401
|
3 years |
busenius |
Small fix
|
|
|
|
@25400
|
3 years |
busenius |
Some helper script
|
|
|
|
@25395
|
3 years |
busenius |
Fixed some destructor consistency testcases
|
|
|
|
@25394
|
3 years |
busenius |
Failing consistency check if tuples are encountered (not supported yet)
|
|
|
|
@25393
|
3 years |
busenius |
Also trying to prove negated typing destructor consistent theorem
|
|
|
|
@25392
|
3 years |
busenius |
More robust prover output parsing and THF file handling
|
|
|
|
@25391
|
3 years |
busenius |
Only waiting half of the timeout in case we know that the proof should …
|
|
|
|
@25390
|
3 years |
busenius |
New testcase for failed proving dec consistent with certain constructors
|
|
|
|
@25384
|
3 years |
busenius |
Created a smaller core set of types, constructors and destructors
|
|
|
|
@25383
|
3 years |
busenius |
Fixed addConstructors() for tuples
|
|
|
|
@25334
|
3 years |
busenius |
Added a --timeout switch to specify timeout for the prover in type …
|
|
|
|
@25333
|
3 years |
busenius |
Using --consistency instead of --thf
Added --prover to specify LEO-II …
|
|
|
|
@25332
|
3 years |
busenius |
Removed unneeded THFGenerator class
Added some comments
|
|
|
|
@25331
|
3 years |
busenius |
Better presentation of the type consistency checking
|
|
|
|
@25329
|
3 years |
busenius |
Calling leo and parsing output
|
|
|
|
@25328
|
3 years |
busenius |
Fixed THF generation for closed types
|
|
|
|
@25324
|
3 years |
busenius |
Writing temporary THF files for all checks
|
|
|
|
@25320
|
3 years |
busenius |
Small fix
|
|
|
|
@25319
|
3 years |
busenius |
Fixed duplicated types and functions in THF mode
|
|
|
|
@25318
|
3 years |
busenius |
Implemented collecting dependencies of a destructor
Testing generation of …
|
|
|
|
@25317
|
3 years |
busenius |
Separated THF definitions generation for types and destructors
|
|
|
|
@25316
|
3 years |
busenius |
Fixed the problem with differently configured types and different type …
|
|
|
|
@25292
|
3 years |
busenius |
Testing generation of THF files for consistency checking of a type, fixed …
|
|
|
|
@25291
|
3 years |
busenius |
Implemented collecting dependencies of a constructor/type
Refactored THF …
|
|
|
|
@25290
|
3 years |
busenius |
Some fixes
|
|
|
|
@25289
|
3 years |
busenius |
Unhacked a bit THF constructor definitions generation
|
|
|
|
@25288
|
3 years |
busenius |
Moved generation of THF type definition into ExpiType?
|
|
|
|
@24799
|
3 years |
busenius |
Generating correct destructor consistency theorems for THF mode
|
|
|
|
@24798
|
3 years |
busenius |
Generating destructor definitions for THF mode
|
|
|
|
@24797
|
3 years |
busenius |
Added stubs for generating destructor definitions in THF mode
|
|
|
|
@24794
|
3 years |
busenius |
Nearly correct THF type definitions generation (good enough for default …
|
|
|
|
@24792
|
3 years |
busenius |
Implemented checking argument types in type definitions in THF mode
|
|
|
|
@24753
|
3 years |
busenius |
Generating type definition stub for THF mode
|
|
|
|
@24752
|
3 years |
busenius |
Generating subtyping axioms for all types in THF mode
|
|
|
|
@24751
|
3 years |
busenius |
Some THF fixes
|
|
|
|
@24750
|
3 years |
busenius |
Generating distinctness axioms for all functions in THF mode
|
|
|
|
@24749
|
3 years |
busenius |
Using HOLFunction to produce THF definitions of all functions
|
|
|
|
@24748
|
3 years |
busenius |
Added a helper class for HO functions
|
|
|
|
@24702
|
3 years |
busenius |
Generating THF clauses for constructors and type declarations
|
|
|
|
@24701
|
3 years |
busenius |
Added new --thf option and THFGenerator stub
|
|
|
|
@24700
|
3 years |
busenius |
Some comments
|
|
|
|
@24220
|
3 years |
busenius |
Better doTyping
|
|
|
|
@24219
|
3 years |
busenius |
Removed a very stupid piece of code from Term.doTyping(ExpiType?)
|
|
|
|
@24218
|
3 years |
busenius |
Fixed type annotations in protocols
|
|
|
|
@24217
|
3 years |
busenius |
Fixed isClosed() for function type
|
|
|
|
@24216
|
3 years |
busenius |
Requiring function type annotations in destructors again
|
|
|
|
@24215
|
3 years |
busenius |
NOTE++
|
|
|
|
@24105
|
3 years |
busenius |
FIXME++
|
|
|
|
@24104
|
3 years |
busenius |
Small fix of term typing
|
|
|
|
@24103
|
3 years |
busenius |
More test cases for destructors
|
|
|
|
@24102
|
3 years |
busenius |
Added more test cases for destructor type checking
|
|
|
|
@23986
|
3 years |
busenius |
Some fixes in dtor test cases
|
|
|
|
@23985
|
3 years |
busenius |
Added many test cases for the (not yet implemented) correct destructor …
|
|
|
|
@23984
|
3 years |
busenius |
Small fix
|
|
|
|
@23927
|
3 years |
busenius |
FIXME--
|
|
|
|
@23926
|
3 years |
busenius |
SymLib?: Unhacked hardcoded constructor matching code
|
|
|
|
@23925
|
3 years |
busenius |
Removed deprecated replaceConfig() method from ExpiType?
|
|
|
|
@23922
|
3 years |
busenius |
FIXME++
|
|
|
|
@23921
|
3 years |
busenius |
Updated FIXMEs
|
|
|
|
@23920
|
3 years |
busenius |
Refactored FunctionType?, UnknownType? and TypeVariable?, extracted a common …
|
|
|
|
@23919
|
3 years |
busenius |
Got rid of assert in SymLib?
|
|
|
|
@23918
|
3 years |
busenius |
Updated FIXMEs
|
|
|
|
@23917
|
3 years |
busenius |
SymLib?: Using real type params instead of null in instance()
|
|
|
|
@23892
|
3 years |
busenius |
Added a check that every implementation class implements at most 1 type …
|
|
|
|
@23891
|
3 years |
busenius |
Implemented prf_k* constructors in concrete library
Added PRFState class
|
|
|
|
@23890
|
3 years |
busenius |
Using prf_k* constructors to generate keys in TLS instead of the …
|
|
|
|
@23889
|
3 years |
busenius |
Using openssl.org as the default host for https example again
|
|
|
|
@23888
|
3 years |
busenius |
Removed unnecessary guessing of configs during SymLib? generation
|
|
|
|
@23887
|
3 years |
busenius |
Getting class name and configuration for constructors inside a destructor …
|
|
|
|
@23886
|
3 years |
busenius |
Checking on parsing that all concrete types from ctor have the same config …
|
|
|
|