ada-libraries
/
jwx
mirror of https://github.com/Componolit/jwx
1
0
Fork 0
Code Issues Releases Wiki Activity
175 Commits 6 Branches 2 Tags 568 KiB
Commit Graph

123 Commits

Author SHA1 Message Date
Alexander Senier 0ac32e393a Store string offset into elements 2020-10-11 01:55:34 +02:00
Alexander Senier 96284aadf8 Implement procedure to iterate object elements 2020-10-07 11:11:11 +02:00
Alexander Senier 8fb08aa6fc Prove absence of overflows for fractional numbers 
Closes #4
 2020-04-25 19:51:10 +02:00
Alexander Senier 1efa73cec7 Correctly model package state 
Ref. #4
 2020-04-24 00:19:54 +02:00
Alexander Senier eaca763d55 Remove redundant initialization 
Ref. #4
 2020-04-23 23:53:07 +02:00
Alexander Senier bdf8ec8392 Do not use packages 2020-04-23 23:51:17 +02:00
Alexander Senier 6e2f0bd5fd Make Context_Size constant 
The variable input Input_Data'Length is not allowed in SPARK

Ref. #4
 2020-04-23 23:49:36 +02:00
Alexander Senier 8262c8871e Fix overflow in negative number handling 
Ref. #4
 2020-04-23 23:47:44 +02:00
Alexander Senier 6c8279d068 Fix array index check 
Ref. #4
 2020-04-23 23:44:19 +02:00
Alexander Senier 9b34ca4bcc Justify constant variable warning 2018-08-18 15:09:16 +02:00
Alexander Senier b5769ff2b1 Limit parser recursion depth 2018-08-18 15:09:16 +02:00
Alexander Senier 199a914c00 Don't use <= comparison for non-negative types 2018-08-18 15:09:16 +02:00
Alexander Senier 9e907b0a0e Remove unused variables 2018-08-18 15:09:16 +02:00
Alexander Senier 113685530f Fix whitspace, parentheses and casing 2018-08-18 15:09:16 +02:00
Alexander Senier f1aa269afe Add missing subprogram specs 2018-08-18 15:09:16 +02:00
Alexander Senier df9ada5aff Remove unused with/use clauses 2018-08-18 15:09:16 +02:00
Alexander Senier b732a7b53c Avoid name hiding 2018-08-18 15:09:16 +02:00
Alexander Senier 78b664b1df Rename LSC package 2018-08-18 15:09:16 +02:00
Alexander Senier 8c6d24d67f Fix whitespace errors 2018-08-18 14:14:41 +02:00
Alexander Senier 67d8569223 Consistently enable SPARK_Mode 2018-08-18 14:14:41 +02:00
Alexander Senier d63b8d0bc1 Add API documentation 2018-08-18 14:14:41 +02:00
Alexander Senier f894d67448 Refactor JWS to use Range_Type 2018-08-18 14:14:41 +02:00
Alexander Senier 71f25db8b2 Refactor JWX 2018-08-18 14:14:41 +02:00
Alexander Senier 8c53a38bb3 Handle optional key elements correctly 2018-08-18 14:14:41 +02:00
Alexander Senier 43c8daab68 WIP: Prove AoRTE 2018-08-18 14:14:41 +02:00
Alexander Senier d761dd6a50 Proof JWT handling 2018-08-18 14:14:41 +02:00
Alexander Senier 7fe9c05f2d Base64: Simplify preconditions for decode operation 2018-08-18 14:14:40 +02:00
Alexander Senier 30380a0fd2 Use fixed-point instead of float numbers 2018-08-18 14:14:40 +02:00
Alexander Senier 5f87d336ec Suppress warning of proof function not checking result 2018-08-18 14:14:40 +02:00
Alexander Senier 4488ac002a WIP: Prove 2018-08-18 14:14:40 +02:00
Alexander Senier aa7b7d311d Fix loop termination for parsing numbers 2018-08-18 14:14:40 +02:00
Alexander Senier b6298842f7 Establish Base64 preconditions 2018-08-18 14:14:40 +02:00
Alexander Senier 113df2f4bb WIP: Prove 2018-08-18 14:14:40 +02:00
Alexander Senier 0345a9235a Change floating point type to Long_Float 2018-08-18 14:14:40 +02:00
Alexander Senier 9d46fce8fc Prove precondition of JWX_Byte_Array_To_LSC_Word32_Array 2018-08-18 14:14:40 +02:00
Alexander Senier a9e7c2ed45 Fix JWX.Stream_Auth instantiation 2018-07-03 21:46:58 +02:00
Alexander Senier d431b075d2 Work around GNAT issue in refined state handling 
Fixes #1
 2018-07-02 21:50:07 +02:00
Alexander Senier ff386a168f Fix end-of-token detection 2018-06-24 23:25:24 +02:00
Alexander Senier f41a0bbda3 Remove unused entities and packages 2018-06-24 22:58:17 +02:00
Alexander Senier fd25ef5939 Add expiration checking support to example proxy 2018-06-24 22:58:17 +02:00
Alexander Senier f4e1d3e341 JWT: Change current time to Long_Integer 2018-06-24 22:58:17 +02:00
Alexander Senier 6451c4b0e0 Refactor authentication proxy example 2018-06-24 22:58:17 +02:00
Alexander Senier 313d38736f Clean up unused entities and packages 2018-06-21 10:39:53 +02:00
Alexander Senier e7a7385902 Implement JWT validation 2018-06-09 00:50:25 +02:00
Alexander Senier 5468b7381d Refactor JWS into generic in preparation of JWT support 2018-06-08 19:46:02 +02:00
Alexander Senier e24d7e3480 Rename proof helper for jwx.stream_auth package 2018-06-08 16:09:43 +02:00
Alexander Senier f598cbdb08 Implement authentication of test streams 2018-06-08 15:27:45 +02:00
Alexander Senier ab53e2bf72 Add HTTP auth test cases 2018-06-07 13:30:26 +02:00
Alexander Senier 98687bad37 Add missing file headers 2018-06-06 21:27:24 +02:00
Alexander Senier 47b5ef37c0 Fix post/pre condition of Valid_Oct 2018-06-03 23:28:09 +02:00