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

175 Commits

Author SHA1 Message Date
Alexander Senier 0ac32e393a Store string offset into elements 2020-10-11 01:55:34 +02:00
Alexander Senier 18e557096f Update build status badge 2020-10-10 12:47:04 +02:00
Alexander Senier c89aaa682b Enable GitHub Actions 2020-10-10 12:34:38 +02:00
Alexander Senier 96284aadf8 Implement procedure to iterate object elements 2020-10-07 11:11:11 +02:00
Alexander Senier 380c57d01b Update to CE 2020 
Ref. #8
 2020-05-22 14:45:16 +02:00
Alexander Senier 7413ab29a4 Fix proofs and example programs 2020-05-21 01:14:37 +02:00
Alexander Senier 10b70ada8f Update toolchain in CI 2020-05-21 01:14:37 +02:00
Alexander Senier 9c0d0e1de7
Merge pull request #6 from Componolit/issue_4 
Issue 4
 2020-04-25 19:54:43 +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 ea388cb7e4 Add version, extend limitiations section 2018-08-18 15:09:16 +02:00
Alexander Senier 9b34ca4bcc Justify constant variable warning 2018-08-18 15:09:16 +02:00
Alexander Senier 1158fb7f75 Fix API doc generation, add static API doc 2018-08-18 15:09:16 +02:00
Alexander Senier f8cdde3e4b Make call graph generation configurable 2018-08-18 15:09:16 +02:00
Alexander Senier 6f93c2d12a Fix typos in README 2018-08-18 15:09:16 +02:00
Alexander Senier 772aeac5f4 Enable CI 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 3d564b220d Allow running stack checker 2018-08-18 15:09:16 +02:00
Alexander Senier 1ab0ca4667 Clean up examples build 2018-08-18 15:09:16 +02:00
Alexander Senier 7cf8b73b29 Enable style checks 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 b87ba2d28d Rename project file 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 fcbbd9f655 Update README 2018-08-18 14:14:41 +02:00
Alexander Senier 9d34b5321a Fix examples 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 734e3de796 Add algorithm type to test keys 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