Commit Graph

  • 13158be915 save before changing everything Guillaume Cluzel 2020-05-18 10:28:58 +02:00
  • 96f8ad7373 Add proof for TCP Connect and Listen Guillaume Cluzel 2020-05-14 23:22:55 +02:00
  • ec04f1586d Resolve all bugs. Let's start the writting of contracts Guillaume Cluzel 2020-05-14 11:36:10 +02:00
  • 8fe1e0130c Correct bugs Guillaume Cluzel 2020-05-14 10:50:52 +02:00
  • 00f7432be1 Add SPARK_Mode for TCP files Guillaume Cluzel 2020-05-12 23:28:33 +02:00
  • 58a694dc99 Improve proofs readability Guillaume Cluzel 2020-05-11 23:44:36 +02:00
  • 5129069299 Add a model for the sockets Guillaume Cluzel 2020-05-11 11:55:04 +02:00
  • 2dea85f03d Use type that fail Guillaume Cluzel 2020-05-09 12:09:37 +02:00
  • 36d33df7e1 * Update proofs * Bind more code Guillaume Cluzel 2020-05-09 00:43:03 +02:00
  • 6bd03814eb Update contracts Guillaume Cluzel 2020-05-07 15:45:28 +02:00
  • 29b8648003 Update not null socket Guillaume Cluzel 2020-05-07 12:22:36 +02:00
  • 25a67a3373 Add Tcp_Abort Guillaume Cluzel 2020-05-07 09:33:05 +02:00
  • 40b0d250a7 clean code Guillaume Cluzel 2020-05-06 19:31:20 +02:00
  • 7f10e7cf8a tmp Guillaume Cluzel 2020-05-06 19:10:45 +02:00
  • 0d200b3a86 Change flags Guillaume Cluzel 2020-05-06 19:09:29 +02:00
  • db11fe02bd Merge pull request #3 from yannickmoy/minor gcluzel 2020-05-07 09:32:36 +02:00
  • a629ebd6bf Minor cleanup Yannick Moy 2020-05-06 23:05:43 +02:00
  • 8f316e9ef2 update code Guillaume Cluzel 2020-05-06 17:09:28 +02:00
  • ecb1dd4d7e Merge pull request #1 from yannickmoy/minor gcluzel 2020-05-06 16:35:33 +02:00
  • 842acd38c7 Merge branch 'master' into minor gcluzel 2020-05-06 16:35:16 +02:00
  • 2cff162258 update styl Guillaume Cluzel 2020-05-06 14:59:01 +02:00
  • c80a276a2c proofs Guillaume Cluzel 2020-05-06 13:27:16 +02:00
  • 945ea292f6 Ménage + ajout de fonctoins Guillaume Cluzel 2020-05-05 22:57:44 +02:00
  • a4ca52cd75 Merge pull request #2 from yannickmoy/style gcluzel 2020-05-06 14:58:29 +02:00
  • 6af1eb3b96 Suggestions for style Yannick Moy 2020-05-06 12:15:18 +02:00
  • 404e7df228 Minor changes and add comments for proof Yannick Moy 2020-05-06 11:48:15 +02:00
  • c8ce43d3c6 update proofs Guillaume Cluzel 2020-05-05 12:02:50 +02:00
  • 5f8a4de83e End of proofs for socket Guillaume Cluzel 2020-05-04 14:29:02 +02:00
  • 48ac365b8f more in the proofs Guillaume Cluzel 2020-04-30 17:53:10 +02:00
  • 4bb3cd8852 reimplementation of sockets Guillaume Cluzel 2020-04-29 22:54:36 +02:00
  • 39fe821524 More rework of the sockets Guillaume Cluzel 2020-04-28 23:11:46 +02:00
  • 0db4b860a8 Replace C functions by Ada functions Guillaume Cluzel 2020-04-28 20:06:39 +02:00
  • fac1ddcc9e update constraints Guillaume Cluzel 2020-04-23 09:23:02 +02:00
  • 4ed0bb5d80 resolve some bugs Guillaume Cluzel 2020-04-20 19:43:56 +02:00
  • ee3e1e3dc3 update SPARK conditions Guillaume Cluzel 2020-04-20 18:51:48 +02:00
  • 7c19e3d6fd socket binding for server functions Guillaume Cluzel 2020-04-16 15:39:13 +02:00
  • 545d55e4f5 add functions Guillaume Cluzel 2020-04-16 09:58:49 +02:00
  • a1a8a5c6fe remove gnatprove errors/warnings Guillaume Cluzel 2020-04-14 17:44:45 +02:00
  • a5f5226df0 Error codes Guillaume Cluzel 2020-04-14 14:43:31 +02:00
  • 70b92090ab improve contracts Guillaume Cluzel 2020-04-09 17:15:40 +02:00
  • 8e01250f34 prove target Guillaume Cluzel 2020-04-08 14:02:43 +02:00
  • 8b83bed44e error Guillaume Cluzel 2020-04-08 11:37:37 +02:00
  • dda471edc5 Error support and first Spark contracts Guillaume Cluzel 2020-04-07 11:40:59 +02:00
  • 0c784d0957 README.md Guillaume Cluzel 2020-04-06 16:53:10 +02:00
  • 7285dcbf99 ada binding Guillaume Cluzel 2020-04-06 09:47:15 +02:00
  • ade629ecdc Ada binding Guillaume Cluzel 2020-04-03 16:07:30 +02:00
  • 8632177f55 Add drivers for STM32 Guillaume Cluzel 2020-04-03 16:06:40 +02:00
  • b75627b9cb socketOpen binding Guillaume Cluzel 2020-03-30 23:29:03 +02:00
  • 3e86e1a8d8 ada sources Guillaume Cluzel 2020-03-30 09:44:09 +02:00
  • 5db82ac74c t_socket.c Guillaume Cluzel 2020-03-29 14:45:19 +02:00
  • 2266b03d87 tis.config Guillaume Cluzel 2020-03-29 14:38:04 +02:00
  • 4c8b36bf3c t_socket.c Guillaume Cluzel 2020-03-29 13:22:15 +02:00
  • 33ee952309 tis.config Guillaume Cluzel 2020-03-29 13:19:31 +02:00
  • f39a60d3dc tis.config Guillaume Cluzel 2020-03-29 13:15:42 +02:00
  • cf189499fe add tests Guillaume Cluzel 2020-03-29 13:13:57 +02:00
  • d29f58b7b6 tis.config Guillaume Cluzel 2020-03-29 13:01:25 +02:00
  • 56952fd5d8 tis.config Guillaume Cluzel 2020-03-29 12:59:18 +02:00
  • 451378635c Change timeout + close socket Guillaume Cluzel 2020-03-25 22:28:22 +01:00
  • 77e8cc7490 typo Guillaume Cluzel 2020-03-25 16:17:51 +01:00
  • 793ba92d85 Update web client Guillaume Cluzel 2020-03-25 16:08:24 +01:00
  • bf848defd5 Initial commit Guillaume Cluzel 2020-03-25 14:21:41 +01:00