ada/Http_Cyclone
0
0
Fork 0
mirror of https://github.com/AdaCore/Http_Cyclone.git synced 2026-02-12 13:07:39 -08:00
Code Issues Packages Projects Releases Wiki Activity

Commit Graph

  • 6541402a57 styling changes master Kyriakos Georgiou 2020-11-19 10:18:38 +00:00
  • 88667e8f57 final fixes to enable the build of both udp and tcp Kyriakos Georgiou 2020-11-19 10:16:12 +00:00
  • dc3eedc1dc fixing an array range related bug Kyriakos Georgiou 2020-11-19 10:10:05 +00:00
  • 6b3dacc0e0 enabling only TCP Kyriakos Georgiou 2020-11-17 20:26:21 +00:00
  • ef28f636cb adding needed unsigned type conversion Kyriakos Georgiou 2020-11-17 20:22:41 +00:00
  • 10cea25e6b disabling the warnings for out mode of parameters Kyriakos Georgiou 2020-11-17 17:10:35 +00:00
  • 62305ae2cf removing unecessary files for he Cortex-M4 Kyriakos Georgiou 2020-11-16 13:56:59 +00:00
  • aa450e7ce9 adding the makefile for the cortexM7 board Kyriakos Georgiou 2020-11-16 13:49:57 +00:00
  • eda3fdce48 removing support for Cortex-M4 since we can not test it Kyriakos Georgiou 2020-11-16 13:41:58 +00:00
  • a6bb053f86 adding a note about proving and building configs Kyriakos Georgiou 2020-11-16 13:37:01 +00:00
  • b1593e2c2f making the prove to use gnateD instead of gnatep Kyriakos Georgiou 2020-11-16 13:22:57 +00:00
  • 7e05aab844 making the prove.gpr file generic again Kyriakos Georgiou 2020-11-13 12:47:43 +00:00
  • 683e7b2958 adding a use clause Kyriakos Georgiou 2020-11-12 10:52:24 +00:00
  • 15650b7386 changing the version of SPARK PRO used to 22.0w Kyriakos Georgiou 2020-11-12 10:46:40 +00:00
  • fccef9532f removing an annotate for an issue resolved in SPARK PRO 22.0w Kyriakos Georgiou 2020-11-12 10:44:28 +00:00
  • f974d16ad4 minor styling issues Kyriakos Georgiou 2020-11-10 21:08:30 +00:00
  • aec89f2a9c changing version of the Ada Arm compiler used Kyriakos Georgiou 2020-11-10 21:08:00 +00:00
  • 8b1d0ff2b0 adding the tool's versions and fixing the language Kyriakos Georgiou 2020-11-10 20:55:44 +00:00
  • 47ca580b3b fixing the language usage Kyriakos Georgiou 2020-11-10 20:55:05 +00:00
  • 0cbc716f17 fixing a minor warning about use clause Kyriakos Georgiou 2020-11-10 18:57:34 +00:00
  • 98f25a1c1c fixing styling issues Kyriakos Georgiou 2020-11-10 18:49:10 +00:00
  • 5eabf66ce1 silencing to warnings with reason Kyriakos Georgiou 2020-11-10 18:46:36 +00:00
  • e524f00f43 making access type variables null after calling C freeMemory functions on them Kyriakos Georgiou 2020-11-10 17:19:27 +00:00
  • 707da458e3 fixing styling issues Kyriakos Georgiou 2020-11-09 20:12:08 +00:00
  • 253477b2b0 fixing styling issues Kyriakos Georgiou 2020-11-09 19:52:25 +00:00
  • 855065ef87 fixing styling issues Kyriakos Georgiou 2020-11-09 19:45:43 +00:00
  • 90be776ecc fixing style issues Kyriakos Georgiou 2020-11-09 19:30:32 +00:00
  • c734930330 fixing styling issues Kyriakos Georgiou 2020-11-09 18:55:02 +00:00
  • b341bc2c8f unused file Kyriakos Georgiou 2020-11-09 17:57:03 +00:00
  • e0ca8fe419 fixing a couple of bugs for proving with SPARK Kyriakos Georgiou 2020-11-09 16:58:12 +00:00
  • d667cebf15 silencing warning with reasoning Kyriakos Georgiou 2020-11-09 15:05:09 +00:00
  • 38c6c78003 adding more info to the readme file Kyriakos Georgiou 2020-11-09 11:51:16 +00:00
  • df932024ae adding license headers to Ada files Kyriakos Georgiou 2020-11-06 16:04:20 +00:00
  • 96981dc162 adding GPL v3 license Kyriakos Georgiou 2020-11-06 12:33:12 +00:00
  • 5dd8631bdb fixig bug in Makefile to use Cortex-m4 and 2020-arm-elf Kyriakos Georgiou 2020-11-06 12:25:23 +00:00
  • 4709bec188 Merge pull request #4 from gcluzel/stm32f4xx Kyriakos Georgiou 2020-11-05 19:45:58 +00:00
  • 892db5fd3a Add instructions for the compilation Guillaume 2020-11-05 16:47:13 +01:00
  • f59cb239b3 Add a support for the stm32f407 platform. configure.sh is a script to determine which target must be used for the compilation. Guillaume 2020-11-05 16:23:39 +01:00
  • c275949dfe Improve README.md gcluzel 2020-10-22 12:45:42 +02:00
  • 9c676b2929 rework intro Papier Yannick Moy 2020-09-07 13:01:23 +02:00
  • 880701d79b Last changes Guillaume Cluzel 2020-09-04 16:43:24 +02:00
  • 9cb8e30ae5 Description of the Oryx Library Guillaume Cluzel 2020-09-04 12:17:33 +02:00
  • c20269d8bf Rework section on SPARK inserted in new top-level section for Specification Yannick Moy 2020-09-04 12:12:26 +02:00
  • b0384de7e3 Figure of the Oryx Embedded stack Guillaume Cluzel 2020-09-04 09:41:09 +02:00
  • cd46c8f870 More on the paper Guillaume Cluzel 2020-09-04 09:39:46 +02:00
  • e1b2098946 Typo Guillaume Cluzel 2020-09-03 10:46:32 +02:00
  • 1a106a5732 Continue the explainations Guillaume Cluzel 2020-09-02 15:31:24 +02:00
  • ff7472af36 corrections Guillaume Cluzel 2020-09-01 14:23:17 +02:00
  • 46e9924bad first parts of the paper Guillaume Cluzel 2020-09-01 11:30:31 +02:00
  • c76b060a2f Update proofs for Socket_Send_To and Socket_Receive_Ex if the socket is a UDP socket Guillaume Cluzel 2020-08-31 17:01:03 +02:00
  • d2df6395c5 README.md Guillaume Cluzel 2020-08-28 16:04:45 +02:00
  • 42b57afa2c Merge pull request #1 from gcluzel/constants_preprocessing gcluzel 2020-08-28 15:10:02 +02:00
  • e50ca047f2 Revert a previous changes du to merge of #2 Guillaume Cluzel 2020-08-28 15:06:43 +02:00
  • 0f95b022ce Add a preprocessing option to enable or disable support for UDP Guillaume Cluzel 2020-08-07 14:58:04 +02:00
  • ea17ad063e Add support for all the preprocessed constants of the C code in the SPARK code Guillaume Cluzel 2020-08-04 15:48:13 +02:00
  • f051aa400e Add more TCP constants Guillaume Cluzel 2020-08-04 12:22:44 +02:00
  • 7e7333f0cd Test for preprocessing Guillaume Cluzel 2020-08-03 23:11:28 +02:00
  • 42a4511d95 Merge pull request #2 from AdaCore/bug-correction gcluzel 2020-08-28 14:31:45 +02:00
  • 43098607e9 Correction of the last bugs Guillaume Cluzel 2020-08-26 15:39:35 +02:00
  • 7abad46431 Update README Guillaume Cluzel 2020-08-03 11:16:40 +02:00
  • 4288db5291 Update README Guillaume Cluzel 2020-08-03 09:33:40 +02:00
  • 5e66197a15 Corrections in the Makefile Guillaume Cluzel 2020-07-31 14:32:24 +02:00
  • cfb739930d Correction of object size Guillaume Cluzel 2020-07-31 13:52:41 +02:00
  • 00ce3ca2c5 Update report according to Yannick's comments Guillaume Cluzel 2020-07-27 16:11:25 +02:00
  • 3a04ede1b2 Update README.md gcluzel 2020-07-27 12:27:16 +02:00
  • 984c6bd611 Update report Guillaume Cluzel 2020-07-24 11:57:21 +02:00
  • 15e19dde56 Remove unwanted warning and gnatprove messages Guillaume Cluzel 2020-07-24 11:50:31 +02:00
  • 66bb746e24 Update code and proofs for Tcp_Shutdown Guillaume Cluzel 2020-07-23 12:22:15 +02:00
  • f0bb3e9738 - Update proofs after considering tcp timer that can close the connection when we are in state TIME_WAIT - Adding support brief support for udp Guillaume Cluzel 2020-07-21 14:54:40 +02:00
  • 178ce236e5 Merge pull request #4 from yannickmoy/master gcluzel 2020-07-21 15:50:24 +02:00
  • 7e8c6769ef Typo/English review Yannick Moy 2020-07-21 15:36:38 +02:00
  • bf8404d299 Update report Guillaume Cluzel 2020-07-21 11:53:23 +02:00
  • 4a0f31a71b Finish the work with klee to check the possible states that can be reached when a segment is received Guillaume Cluzel 2020-07-20 10:09:24 +02:00
  • d76feed3ad Continue report Guillaume Cluzel 2020-07-19 22:27:03 +02:00
  • a5a2c4ab53 Improvement in code and proofs Guillaume Cluzel 2020-07-19 19:06:02 +02:00
  • 09727cda40 beginning of the report Guillaume Cluzel 2020-07-17 17:47:44 +02:00
  • fc48d7a8f2 Improve coherence in the code Guillaume Cluzel 2020-07-15 17:36:49 +02:00
  • 95b9a16ec3 Update contracts that model the concurrency and update the proof of tcp_receive accordingly Guillaume Cluzel 2020-07-15 11:53:21 +02:00
  • c004557b12 Update the way the transitive closure is computed. Thus it changes a little the transitive closure and then the underlying proofs Guillaume Cluzel 2020-07-10 18:26:36 +02:00
  • 7ce62a46b0 Some corrections in the contracts Guillaume Cluzel 2020-07-08 17:17:58 +02:00
  • 128ce42904 First steps with klee to confirm the contract for the underlaying functions that receive the messages and process them Guillaume Cluzel 2020-07-07 15:54:04 +02:00
  • 71b542b55f update precondition for server side functions Guillaume Cluzel 2020-07-06 15:00:14 +02:00
  • a1f497c154 Add functions to simplify use in loop invariants Guillaume Cluzel 2020-07-06 13:45:46 +02:00
  • 42fe611cd8 Change Stack size to support all the assignments due to the post-condition Old aspect Guillaume Cluzel 2020-07-03 12:05:39 +02:00
  • 039982c2d1 update compilation options Guillaume Cluzel 2020-07-03 10:45:38 +02:00
  • e8263e821a Code failure examples Guillaume Cluzel 2020-07-03 10:42:30 +02:00
  • 05392657aa Delete old unused files + comment some proofs for dynamic check of assertions & contracts Guillaume Cluzel 2020-07-02 14:40:35 +02:00
  • b8b819449f Improve Ada Style Guillaume Cluzel 2020-07-01 15:55:42 +02:00
  • 962674f33c End of the proof for Tcp_Received and Socket_Received Guillaume Cluzel 2020-06-24 15:28:34 +02:00
  • c1b88dad6c last changes Guillaume Cluzel 2020-06-24 10:33:44 +02:00
  • ea71d57280 Correction des contrats Guillaume Cluzel 2020-06-23 19:45:56 +02:00
  • 3fbe8ccfb6 TCP state for verification Guillaume Cluzel 2020-06-19 23:56:07 +02:00
  • 4dd4c0d41f Add a basic model to represent a socket. It allows to keep information about Socket like its type even when a function fail and we cannot really know the TCP state of the socket (or at least, we are even not interrested in knowing). Guillaume Cluzel 2020-06-04 15:36:49 +02:00
  • 07d2c11026 Improvement of the proofs for TCP_Receive and TCP_Send Guillaume Cluzel 2020-06-04 13:52:32 +02:00
  • a8084a253c Update proof Guillaume Cluzel 2020-05-28 16:04:35 +02:00
  • 3560238e0b correct bug Guillaume Cluzel 2020-05-27 19:43:46 +02:00
  • 3c211f7b8c Update postconditions to have something more precise Guillaume Cluzel 2020-05-27 17:04:16 +02:00
  • a4039ed6a6 Update SPARK proofs Guillaume Cluzel 2020-05-27 16:20:17 +02:00
  • 34a906f5d9 Add Send function. Guillaume Cluzel 2020-05-25 23:17:34 +02:00
  • fd9a87d951 add more concurrency Guillaume Cluzel 2020-05-23 20:53:29 +02:00